mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
⊢ (fun x ↦
        match x with
        | (g, g') =>
          ⟨{ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
              invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
              left_inv := ⋯, right_inv := ⋯ },
            ⋯⟩)
      ((fun f ↦
          ({ toFun := fun x ↦ ⟨↑(↑f ↑x), ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ },
            { toFun := fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩, invFun := fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩, left_inv := ⋯,
              right_inv := ⋯ }))
        f) =
    f

Tactic:
ext x
    by_cases hx : x ∈ s
    · simp [hx]
    · rw [mem_prefixed.1 f.2, not_lt] at hx
      simp [hx]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (⋯.unit⁻¹ • f)) ≤ m.toSyn (m.degree f)

Tactic:
apply le_of_eq

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (⋯.unit⁻¹ • f)) = m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
⊢ (M ／ C).Dep (K \ C)

Tactic:
have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (Matroid.sum' M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)

Tactic:
simp only [Matroid.sum', mapEquiv_isBase_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBase_iff]
  convert! Iff.rfl
  ext
  simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
⊢ Injective fun f ↦ φ.map f

Tactic:
rintro f g he
  have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
  simpa using (hφ.star_bijective u).left this

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices.length = p'.length + 1
⊢ (p'.cons e).vertices.length = (p'.cons e).length + 1

Tactic:
simp [vertices_cons, length_cons, ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
ih : ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨b✝, p'⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
| cons p' ev ih =>

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
· rintro ⟨s, ⟨hs, -⟩, rfl⟩
    exact ⟨hs, mem_insert_self _ _⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ x ∈ range (card α + 1), ↑(card α) * (↑((card α).choose x) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
← mul_sum,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
⊢ Set.InjOn (compress u v) ↑({a ∈ s | compress u v a ∉ s})

Tactic:
by
  intro a ha b hb hab
  rw [mem_coe, mem_filter] at ha hb
  rw [compress] at ha hab
  split_ifs at ha hab with has
  · rw [compress] at hb hab
    split_ifs at hb hab with hbs
    · exact sup_sdiff_injOn u v has hbs hab
    · exact (hb.2 hb.1).elim
  · exact (ha.2 ha.1).elim

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
⊢ ∃ a, Iic a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal (coe_nonempty.2 hs.ne_bot)

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
a : α
ha : a ∈ ↑s
has : ∀ ⦃y : α⦄, (fun x ↦ x ∈ ↑s) y → a ≤ y → y ≤ a
⊢ ∃ a, Iic a = s
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]
  simp [birkhoffSet_inf]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α),

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ supSum {s} = ∑ s, ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) - 1
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s

Tactic:
h (Insert.insert b s) _ (subset_insert _ _)

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).Intersecting
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ image (fun t ↦ s ∩ t) 𝒜 = s.powerset

Tactic:
ext t; rw [mem_image, mem_powerset, h.subset_iff]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
⊢ a ∉ t

Tactic:
obtain ⟨u, hu, htu⟩ := ht.exists_superset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
⊢ a ∉ t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer

Tactic:
intro a 𝒜 ih₀ ih₁

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
⊢ #𝒜 ≤ #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α + 1), ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r) ≤ 1

Tactic:
rw [← sum_flip]
    refine (le_card_falling_div_choose le_rfl h𝒜).trans ?_
    rw [div_le_iff₀] <;> norm_cast
    · simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using
        Set.Sized.card_le (sized_falling 0 𝒜)
    · rw [tsub_self, choose_zero_right]
      exact zero_lt_one

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ¬Disjoint (id b₁) (id b₂)

Tactic:
simp only [Set.not_disjoint_iff]

Goal state after:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ∃ x ∈ id b₁, x ∈ id b₂
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i ↦ t i) i j

Tactic:
exact ht.disjoint hij

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
s : Set V
x✝ : ∃ C, C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun x ↦ (induce x G).Connected) s

Tactic:
· exact h ▸ maximal_connected_induce_supp _

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = r

Tactic:
exact h₂ HA

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
he : G.IsBridge s(u, u)
⊢ False

Tactic:
simp [IsBridge] at he

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n

Tactic:
· rintro hc
    have C : G.Coloring (Fin n) := hc.toColoring (by simp)
    let f := Embedding.completeGraph (@Fin.valEmbedding n)
    use f.toHom.comp C
    intro v
    exact Fin.is_lt (C.1 v)

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w

Tactic:
simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
  conv_lhs =>
    rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]
  conv_rhs =>
    rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
  simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),
    sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
  exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : ¬G.Reachable u w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable, Reachable.trans, Adj.reachable]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case hc
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (x, b).1 ((G.boxProdLeft H b).toHom y).1 ∧ (x, b).2 = ((G.boxProdLeft H b).toHom y).2

Tactic:
· exact ⟨h, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case hc
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1

Tactic:
· exact ⟨h, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h✝ : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
suffices {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x} by simpa [Finset.subset_iff] using this

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h✝ : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1

Tactic:
refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
      · exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)
      · exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)
      · rw [mem_coe, mem_toRight] at hi
        rw [mem_coe, mem_toLeft] at hj
        simpa using h hi hj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj u w
hsupp : w ∈ p.support
⊢ w = p.snd

Tactic:
have := h.subsingleton_path u w |>.elim ⟨_, hp.takeUntil hsupp⟩ <| .singleton hadj

Goal state after:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v w : V
p : G.Walk u v
hp : p.IsPath
hadj : G.Adj u w
hsupp : w ∈ p.support
this : ⟨p.takeUntil w hsupp, ⋯⟩ = Path.singleton hadj
⊢ w = p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ q.support

Tactic:
← Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨p₀, hp₀⟩ ⟨q, hq⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ p₀.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
⊢ q = p.concat hadj

Tactic:
have hw : w ∉ p.support := hG.ne_mem_support_of_support_of_adj_of_isPath hq hp hadj.symm hv
  exact Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨q, hq⟩ ⟨_, hp.concat hw hadj⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ m < #G.edgeFinset

Tactic:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.lt_sup_iff, mem_filter_univ]

Goal state after:
V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ (∃ b, H.Free b ∧ m < #b.edgeFinset) ↔ ∃ G x, H.Free G ∧ m < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable

Tactic:
obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
  grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (C.labelGraph k).Adj x y → G.Adj x y

Tactic:
grind [labelGraph_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ j✝ : K
h : i✝ ≠ j✝
⊢ ∀ (x y : V), (C.labelGraph i✝).Adj x y → ¬(C.labelGraph j✝).Adj x y

Tactic:
grind [labelGraph_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ c ∈ {x ∈ G.oddComponents.toFinset | x.supp ⊆ c'.supp} ↔
    c ∈ {x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}

Tactic:
Set.toFinset_ofPred,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ c ∈ {x ∈ {x | Odd x.supp.ncard} | x.supp ⊆ c'.supp} ↔
    c ∈ {x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)

Tactic:
simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
    ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd #(univ.biUnion fun x ↦ x.supp.toFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : G.ediam = 1
u : α
⊢ 0 < G.eccent u

Tactic:
pos_iff_ne_zero

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : G.ediam = 1
u : α
⊢ G.eccent u ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint (↑K ∪ ↑Cfin.toFinset) ↑D
⊢ False

Tactic:
Set.Finite.coe_toFinset,

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint (↑K ∪ C.supp) ↑D
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (atTop.limUnder fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)))

Tactic:
h_tendsto.limUnder_eq

Goal state after:
W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
hlg : ↑w.length < G.egirth
w' : G.Walk a a := w.cycleBypass
hwc' : w'.IsCycle
hwlg' : ↑w'.length < G.egirth
⊢ False

Tactic:
exact not_le_of_gt hwlg' (SimpleGraph.egirth_le_length hwc')

Goal state after: