mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ (b ⊔ c) = a → a ⊓ b = a ∨ a ⊓ c = a

Tactic:
inf_sup_left

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ ≤ infSum 𝒜

Tactic:
calc
    _ = ∑ s ∈ 𝒜, #(truncatedInf 𝒜 s) / (#s * (card α).choose #s : ℚ) := ?_
    _ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ = ∑ s ∈ 𝒜, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬs : ℬ = ∅ ∨ ℬ = {∅}
⊢ #𝒜 * #ℬ ≤ 2 ^ #∅ * #(𝒜 ∩ ℬ)

Tactic:
obtain rfl | rfl := h𝒜s

Goal state after:
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)

case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ {s}, f x = f s + 0

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ ∅, f x = 0 + 0

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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

Goal state before:
pp: case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

pp: case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
· have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
    have := shadow_monotone this
    simp only [subset_empty, shadow_singleton_empty] at this
    simp [this]

Goal state after:
case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
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:
← sum_flip

Goal state after:
𝕜 : 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), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ 1
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (ker f).classes ⊆ Set.range fun y ↦ {x | f x = y}

Tactic:
rintro s ⟨x, rfl⟩
  rw [Set.mem_range]
  exact ⟨f x, rfl⟩

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)

Tactic:
set range'k : Finset (Fin n) :=
    attachFin (range k) fun m ↦ by rw [mem_range]; apply forall_lt_iff_le.2 hkn

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
w : V
⊢ G.Adj v w ↔ w ∈ {w ∈ t | G.Adj v w}

Tactic:
mem_filter,

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
w : V
⊢ G.Adj v w ↔ w ∈ t ∧ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
v : V
⊢ G.Adj v w ↔ v ∈ {v ∈ s | G.Adj v w}

Tactic:
mem_filter,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
v : V
⊢ G.Adj v w ↔ v ∈ s ∧ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w

Tactic:
by
  rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
⊢ (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ

Tactic:
simpa using between_isBipartiteWith disjoint_compl_right

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ

Tactic:
simpa using between_isBipartiteWith disjoint_compl_right

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
h_bipartite : (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ
⊢ #(G.neighborFinset w) ≤ #((between (↑s) (↑s)ᶜ G).neighborFinset w ∪ sᶜ)

Tactic:
exact card_le_card (neighborFinset_subset_between_union_compl hw)

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
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h✝ : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ (s.erase y).erase x | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅

Tactic:
filter_erase,

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h✝ : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce {v_1 | v_1 ∈ p.support} G).Connected

Tactic:
rw [← p.verts_toSubgraph]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
cases h with
    | inl h | inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

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

Goal state before:
pp: n i m : ℕ
hm : m < n + 3
hi : i ≤ ↑⟨m, hm⟩
⊢ ↑((cycleCons n ⟨m, hm⟩).getVert i) = (↑⟨m, hm⟩ - i) % (n + 3)

Tactic:
induction i generalizing m

Goal state after:
case zero
n m : ℕ
hm : m < n + 3
hi : 0 ≤ ↑⟨m, hm⟩
⊢ ↑((cycleCons n ⟨m, hm⟩).getVert 0) = (↑⟨m, hm⟩ - 0) % (n + 3)

case succ
n n✝ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝) = (↑⟨m, hm⟩ - n✝) % (n + 3)
m : ℕ
hm : m < n + 3
hi : n✝ + 1 ≤ ↑⟨m, hm⟩
⊢ ↑((cycleCons n ⟨m, hm⟩).getVert (n✝ + 1)) = (↑⟨m, hm⟩ - (n✝ + 1)) % (n + 3)
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
intro h1
    cases h1 with
      | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
      | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

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

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
mem_filter,

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free (SimpleGraph.map (⇑e) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
mem_filter,

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free (SimpleGraph.map (⇑e) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
⊢ extremalNumber n H = {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
by
  let e := Fintype.equivFinOfCardEq hc
  rw [extremalNumber, le_antisymm_iff]
  and_intros
  on_goal 1 =>
    replace e := e.symm
  all_goals
  rw [Finset.sup_le_iff]
  intro G h
  have h' : G.map e ∈ univ.filter (H.Free ·) := by
    rw [mem_filter, ← free_congr .refl (.map e G)]
    simpa using h
  rw [Iso.card_edgeFinset_eq (.map e G)]
  convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) _ h'

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ⋯.toGraph.Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬G.Adj x✝¹ x✝ → False ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
this : (f x).takeUntil y hy = cons h nil
⊢ False

Tactic:
by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
by
  have := hG.connected.nonempty
  inhabit V
  classical
  have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
    rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
  rw [← this, add_left_inj]
  choose f hf hf' using (hG.existsUnique_path · default)
  refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
  case notNil => exact not_nil_of_ne (by simpa using hw)
  case memEdges => simp
  case inj =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
    rw [dart_edge_eq_iff] at h
    obtain (h | h) := h
    · exact (congrArg (·.fst) h)
    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro x y h
    wlog h' : (f x).length ≤ (f y).length generalizing x y
    · rw [Sym2.eq_swap]
      exact this y x h.symm (le_of_not_ge h')
    refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
    · rintro rfl
      rw [← hf' _ nil IsPath.nil, length_nil,
          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
          length_cons, length_nil] at h'
      simp at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]

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

Goal state before:
pp: V : Type u_1
K : Type u_3
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : Fintype K
⊢ Fintype.card K ^ #⊤.edgeFinset = Fintype.card K ^ (Fintype.card V).choose 2

Tactic:
card_edgeFinset_top_eq_card_choose_two

Goal state after:
V : Type u_1
K : Type u_3
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : Fintype K
⊢ Fintype.card K ^ (Fintype.card V).choose 2 = Fintype.card K ^ (Fintype.card V).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ¬⟦a⟧ = ⟦b⟧ ↔ G.Adj a b

Tactic:
Quotient.eq

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ¬h.setoid a b ↔ G.Adj a b
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 ∈ {x | Odd x.supp.ncard} | x.supp ⊆ c'.supp} ↔
    c ∈ {x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}

Tactic:
mem_filter,

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 ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd #(filter (Membership.mem c.supp) univ)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| extremalNumber n ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
enter [1, 1]

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| n
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := ⋯
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := ⋯
⊢ Injective fun x ↦
    match x with
    | (i, j) => ↑((fₜ (fᵣ i)) j)

Tactic:
intro (i₁, j₁)

Goal state after:
case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
⊢ ∀ ⦃a₂ : Fin r × Fin t⦄,
    (fun x ↦
            match x with
            | (i, j) => ↑((fₜ (fᵣ i)) j))
          (i₁, j₁) =
        (fun x ↦
            match x with
            | (i, j) => ↑((fₜ (fᵣ i)) j))
          a₂ →
      (i₁, j₁) = a₂
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : Even K.supp.ncard
⊢ ?m.31 ∉ G.oddComponents

Tactic:
simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
u : α
⊢ G.eccent u = ⊤

Tactic:
rw [connected_iff_exists_forall_reachable] at h
  push Not at h
  obtain ⟨v, h⟩ := h u
  rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
  exact le_iSup (G.edist u) v

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ⊤.eccent u = 1

Tactic:
apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u
  rw [eccent, iSup_le_iff]
  intro v
  cases eq_or_ne u v <;> simp_all [edist_top_of_ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ ⨆ u, G.eccent u = ⨆ p, G.edist p.1 p.2

Tactic:
eccent_def,

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ ⨆ u, (fun u ↦ ⨆ v, G.edist u v) u = ⨆ p, G.edist p.1 p.2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ p, G.edist p.1 p.2

Tactic:
by
  rw [ediam, eccent_def, iSup_prod]

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| ↑(extremalNumber (n + 1) H) / ↑((n + 1).choose 2)

Tactic:
enter [1, 1]

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| extremalNumber (n + 1) H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ b ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G},
    #b.edgeFinset ≤ {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
mem_filter,

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ∈ univ ∧ b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset