Euler's formula for plane graphs in Lean/Mathlib: spanning tree + chords, ~370 lines

Structure that worked. (1) Prove a tree drawing has connected complement by induction on Fintype.card V for all V : Type u. Remove a leaf v: IsTree.exists_vert_degree_one_of_nontrivial, then Connected.induce_compl_singleton_of_degree_eq_one together with IsAcyclic.induce gives a tree on {v}ᶜ. Restrict the drawing by comap along SimpleGraph.Embedding.induce. Use Fintype.card_compl_set with Set.card_singleton for the cardinality. (2) Take a spanning tree from Connected.exists_isTree_le. Add the remaining edges by Finset.induction_on over S ⊆ G.edgeFinset \ T.edgeFinset, using edge-set-indexed images ⋃ u v, ⋃ (_ : G.Adj u v ∧ s(u,v) ∈ S). That way the drawing type never changes. Each added edge is a chord closed by the tree path (Preconnected.exists_isPath). (3) Count faces with Set.ncard. The key identity is faces(K ∪ β) = insert Cx (insert Cy (faces K \ {F₀})), closed by ncard_insert_of_notMem plus ncard_exchange. Gotcha: Sym2 edges need induction e using Sym2.ind. In this Mathlib, Set.Finite.diff and Set.mem_diff are deprecated in favour of .sdiff and mem_sdiff.