mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ Disjoint (C' \ K) K ∧ M.Dep (C' \ K ∪ K)

Tactic:
and_iff_right disjoint_sdiff_left

Goal state after:
α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ M.Dep (C' \ K ∪ K)
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]

Goal state after:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' (fun a ↦ ⟨a.1, a.2⟩) '' B)) ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
⊢ IsStronglyConnected (Symmetrify V)

Tactic:
by
  intro a b
  obtain ⟨p⟩ := h a b
  induction p with
  | nil => exact ⟨Path.nil⟩
  | cons q e ih => exact ⟨ih.some.cons (Sum.inl e)⟩

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

Goal state before:
pp: V : Type u_1
inst✝³ : Quiver V
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
w : V → V → R
hw : ∀ (i j : V), 0 ≤ w i j
i j : V
p : Path i j
⊢ 0 ≤ weightOfEPs w p

Tactic:
by
  apply weight_nonneg
  intro i j e
  exact hw _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s

Tactic:
exact And.imp_left (h <| subset_insert _ _)

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

Goal state before:
pp: case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
have h𝒜 : 𝒜.Nonempty := by by_contra! rfl; simp at h𝒜₃

Goal state after:
case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'

Tactic:
mem_shadow_iff_insert_mem

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
⊢ (insert a s).Intersecting

Tactic:
rintro b (rfl | hb) c (rfl | hc)
  · rwa [disjoint_self]
  · exact h _ hc
  · exact fun H => h _ hb H.symm
  · exact hs hb hc

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

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

Tactic:
exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

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

Goal state before:
pp: case mpr.inr.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
⊢ a ∈ t

Tactic:
by_contra

Goal state after:
case mpr.inr.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this✝ : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this : a ∉ t
⊢ False
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
rw [← compress_sdiff_sdiff A B] at hAB hBA

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex (compress (A \ B) (B \ A) B)
sizeA : #B = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
f : ι → V
hf : Pairwise fun i j ↦ G.Adj (f i) (f j)
C : G.Coloring (Fin n)
⊢ Nat.card ι ≤ n

Tactic:
simpa using Nat.card_le_card_of_injective _ (C.injective_comp_of_pairwise_adj f hf)

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

Goal state before:

Tactic:
k.choose (r - i)
    _ = #(powersetCard (r - i) range'k) := by rw [card_powersetCard, card_attachFin, card_range]
    _ = #(∂^[i] 𝒞) := by
      congr!
      ext B
      rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
      constructor
      · rintro ⟨hBk, hB⟩
        have := exists_subsuperset_card_eq hBk (Nat.le_add_left _ i) <| by
          rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
        obtain ⟨C, BsubC, hCrange, hcard⟩ := this
        rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
        refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
        rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
      · rintro ⟨A, Ah, hBA, card_sdiff_i⟩
        rw [mem_powersetCard] at Ah
        refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
        rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
    _ ≤ #(∂^[i] 𝒜) := by
      refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
      · rwa [card_powersetCard, card_attachFin, card_range]
      simp_rw [𝒞, mem_powersetCard]
      rintro A B hA ⟨HB₁, HB₂⟩
      refine ⟨fun t ht ↦ ?_, ‹_›⟩
      rw [mem_attachFin, mem_range]
      have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
      apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
      simp_rw [mem_image]
      rintro _ ⟨a, ha, hab⟩
      simpa [range'k, hab] using hA.1 ha

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
⊢ ¬w.Nil

Tactic:
by rintro ⟨⟩; simp_all

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
s : Finset V
h : G.IsClique ↑s
hc : G.Colorable n
⊢ Pairwise fun i j ↦ G.Adj ↑i ↑j

Tactic:
simpa [Pairwise] using! h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
⊢ Pairwise fun i j ↦ G.Adj ↑i ↑j

Tactic:
simpa [Pairwise] using! h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
⊢ G.CliqueFree m

Tactic:
by
  by_contra h
  simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h
  obtain ⟨s, h, rfl⟩ := h
  exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
simpa [adj_toSubgraph_iff_mem_edges] using! fun _ _ h ↦ p.edges_toPath_subset_edges h

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

Goal state before:
pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
by_contra

Goal state after:
case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
this : ¬2 ≤ G.edist u v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
⊢ G.Preconnected

Tactic:
by
  classical
  rintro a₁ a₂
  obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
  exact ⟨w.ofBoxProdLeft⟩

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

Goal state before:
pp: n : ℕ
v : Fin (n + 3)
⊢ {v - 1, v + 1}.card = 2

Tactic:
Finset.card_pair

Goal state after:
n : ℕ
v : Fin (n + 3)
⊢ 2 = 2

n : ℕ
v : Fin (n + 3)
⊢ v - 1 ≠ v + 1
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_1.refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ (Walk.map h.toHom (cycleGraph.cycle (n - 3))).IsCycle

Tactic:
exact (isCycle_map_iff_of_injective h.injective).mpr cycleGraph.isCycle_cycle

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

Goal state before:
pp: case refine_2.refine_3
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ⋯ }

Tactic:
have hlen : p.tail.support.length = n := by
        grind [length_tail_add_one, not_nil_iff_lt_length]
      have (m : Fin n) : p.support[m.succ]'(by grind) = p.tail.support[m] := by
        simp [p.support_tail_of_not_nil hp₁.not_nil]
      simp_rw [this]
      have := IsPath.mk' <| (support_tail_of_not_nil _ hp₁.not_nil) ▸ hp₁.support_nodup
      exact hlen ▸ (isPath_iff_injective_get_support _ |>.mp this)

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
this : Nonempty V
inhabited_h : Inhabited V
⊢ Fintype.card V - 1 + 1 = Fintype.card V

Tactic:
Nat.sub_add_cancel Fintype.card_pos

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ Fintype.card V = Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
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
⊢ ¬y = default

pp: case refine_2
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
⊢ ((f y).firstDart ⋯).toProd = (y, x)

Tactic:
· 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'

Goal state after:
case refine_2
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
⊢ ((f y).firstDart ⋯).toProd = (y, x)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
⊢ F.Reachable u v

Tactic:
by_contra

Goal state after:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this : ¬F.Reachable u v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
⊢ Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F

Tactic:
by_contra

Goal state after:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
⊢ ¬z = v

Tactic:
by_contra

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : z = v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: case hf
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
x✝ y✝ : V
he : s(x✝, y✝) ∈ G.edgeSet
⊢ C ⟨s(x✝, y✝), he⟩ = C' ⟨s(x✝, y✝), he⟩

Tactic:
exact h _ _ he

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #z
⊢ False

Tactic:
Finset.card_eq_of_equiv hz.equiv

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t

Tactic:
by
  simp_rw [verts, card_disjiUnion, id_eq, sum_congr rfl fun _ ↦ K.card_mem_parts, sum_const,
    smul_eq_mul, mul_eq_mul_right_iff]
  exact K.card_parts

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x✝¹ : G.ConnectedComponent
x✝ : x✝¹ ∈ C
⊢ x✝¹ ∈ G.connectedComponentMk '' Quot.out '' C

Tactic:
simpa [connectedComponentMk]

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

Goal state before:
pp: case e_a
n r : ℕ
⊢ (((∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0) +
        ∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
simp_rw [ne_comm, ← two_mul]

Goal state after:
case e_a
n r : ℕ
⊢ ((2 * ∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)
⊢ ∀ (v : ↑Kᶜ), β ((induce Kᶜ G).connectedComponentMk v)

Tactic:
exact fun ⟨v, vnK⟩ => f vnK

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

Tactic:
rw [← Fintype.card_fin (n + 1)]

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

Goal state before:
pp: case refine_1
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2).Nonempty

Tactic:
Set.image_nonempty

Goal state after:
case refine_1
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ (Set.Ici 2).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : G.egirth ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Tactic:
egirth,

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ⨅ a, ⨅ w, ⨅ (_ : w.IsCycle), ↑w.length ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ ⨅ a, ⨅ w, ⨅ (_ : w.IsCycle), ↑w.length = ↑w.length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ ↑(t'.choose t ^ r * t) * ↑(t' - t) ≤ ↑(#(filter K t)) * ↑(t' - t)

Tactic:
Nat.cast_sub ht_lt_t'.le

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ ↑(t'.choose t ^ r * t) * (↑t' - ↑t) ≤ ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
n : ℕ
hn : (r + 1) * t ≤ n
G : SimpleGraph (Fin n)
x✝¹ : DecidableRel G.Adj
x✝ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
⊢ (r + 1) * t ≤ n

Tactic:
exact hn

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ ↑t.ncard = Cardinal.mk ↑u

Tactic:
← u.cast_ncard (Set.finite_union.mp hu).2

Goal state after:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ ↑t.ncard = ↑u.ncard
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : CommSemiring R
x : V → R
⊢ x ⬝ᵥ degMatrix R G *ᵥ x = ∑ i, ↑(G.degree i) * x i * x i

Tactic:
simp only [dotProduct, degMatrix, mulVec_diagonal, ← mul_assoc, mul_comm]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
⊢ G.IsMatchingFree

Tactic:
by
  intro x
  by_contra! hc
  apply hmf (x.map (SimpleGraph.Hom.ofLE h))
  refine ⟨hc.1.map_ofLE h, ?_⟩
  intro v
  simp only [Subgraph.map_verts, Hom.coe_ofLE, id_eq, Set.image_id']
  exact hc.2 v

Goal state after: