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

Goal state before:
pp: case h.refine_1
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ I ⊆ univ.sigma Js

pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js

Tactic:
· rw [← univ_sigma_preimage_mk I]
      exact sigma_mono rfl.subset fun i ↦ (hJs i).2

Goal state after:
case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : 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 (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]
        apply bot_le

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ M.closure I

Tactic:
exact hIX.subset_closure

Goal state after:
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'
hdep2 : (M ／ K).Dep (C' \ K)
⊢ C ⊆ C'

Tactic:
← (hC.eq_of_dep_subset hdep2 (sdiff_subset_iff.2 (union_comm _ _ ▸ hC'ss)))

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'
hdep2 : (M ／ K).Dep (C' \ K)
⊢ C' \ K ⊆ C'
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ s ○ t ⊆ s ⊻ t

Tactic:
by
  simp_rw [subset_iff, mem_sups, mem_disjSups]
  exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
⊢ e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)

Tactic:
by
  have : e a ∈ upperClosure (s.map e.toEquiv.toEmbedding) ↔ a ∈ upperClosure s := by simp
  simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]
  congr with h
  simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, inf'_map]

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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
by
  simp only [mem_upperClosure, mem_coe, not_exists, not_and] at ht
  simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    upper_aux.2 (Or.inl hs)]

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∅.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ ∅ → SupIrred b

Tactic:
by simp [ha.eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - 1) ↑(∂ 𝒜)

Tactic:
intro A h
  obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
  rw [card_erase_of_mem hi, h𝒜 hA]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
⊢ s = Iic a ∨ t = Iic a

Tactic:
have := mem_Iic_iff.2 (le_refl a)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : LowerSet α
hst : s ⊔ t = Iic a
this : a ∈ Iic a
⊢ s = Iic a ∨ t = Iic a
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
h : {⊥}.Intersecting
⊢ False

Tactic:
exact intersecting_singleton.1 h rfl

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
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this✝¹ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this✝ : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z

Tactic:
insert_union_comm,

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
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this✝¹ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this✝ : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
⊢ insert z s = ((s ∪ v) \ u ∪ insert w (u.erase w)) \ v.erase z
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = Fintype.card (Finset α)

Tactic:
Fintype.card_finset

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = 2 ^ Fintype.card α
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)

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:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}

Tactic:
mem_sdiff (s := s),

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w, (w ∈ s ∧ w ∉ (s ⊔ U) \ V) ∧ {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₃ (s ∩ t) * f₄ (s ∪ t) + f₃ (insert a s ∩ t) * f₄ (insert a s ∪ t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl
        (insert_union _ _ _), insert_inter_of_notMem ‹_›, ← mul_add]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s

Tactic:
intro hx
    obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
    rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
⊢ c = c'

Tactic:
simp only [mem_supp_iff] at *

Goal state after:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' : G.connectedComponentMk v = c'
⊢ c = c'
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
⊢ Injective (hs.piecewise f)

Tactic:
intro x y h

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
⊢ x = y
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
y : V
hxy : G.Adj x y
⊢ False

Tactic:
refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw <;>
  · rintro ⟨p⟩
    obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
    exact hy₂ <| hx hx₂ hxy

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
⊢ ∃ w, G.Adj u w ∧ G.IsEdgeReachable 2 u w

Tactic:
have : G.Adj u w.snd := Walk.adj_snd (by grind [Walk.not_nil_of_ne])

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
⊢ ∃ w, G.Adj u w ∧ G.IsEdgeReachable 2 u w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Tactic:
use v

Goal state after:
case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ H.verts = (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
by_cases hv : v ∈ s

Goal state after:
case pos
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
⊢ G.edist u w ≤ G.edist u v + G.edist v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: 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 ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅

Tactic:
simp only [← Finset.subset_empty]

Goal state after:
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 ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
simp only [Set.mem_sUnion] at hw

Goal state after:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t ∈ S, w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
h : m + 1 < n + 3
⊢ (cycleCons n ⟨m + 1, h⟩).length = ↑⟨m + 1, h⟩

Tactic:
by
    unfold cycleGraph.cycleCons
    simp only [Walk.length_cons]
    rw [cycleGraph.length_cycle_cons n]

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

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

pp: 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)

Tactic:
· simp [Nat.mod_eq_of_lt hm]

Goal state after:
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 mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s

Tactic:
intro h1
    cases h1 with
      | inl h1 => exact Or.inl h1.left
      | inr h1 => exact Or.inr h1.left

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
⊢ G.IsAcyclic

Tactic:
intro v p hp
  have := hp.three_le_length
  have := Nat.cast_le.mp <| hp.support_nodup.length_le_enatCard.trans h
  rw [List.length_tail, p.length_support] at this
  lia

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 : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.sup_le_iff, mem_filter_univ]
  exact ⟨fun h _ _ h' ↦ by convert! h _ h', fun h _ h' ↦ by convert! h 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
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), G.Adj x y → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
intro x y h

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
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
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
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
this :
  ∀ (x y : V), G.Adj x y → (f x).length ≤ (f y).length → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
⊢ ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
rw [Sym2.eq_swap]
      exact this y x h.symm (le_of_not_ge h')

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
w : G.Walk u✝ u✝
ho : Odd w.length
⊢ False

Tactic:
have := (w.three_le_chromaticNumber_of_odd_loop ho).trans h.chromaticNumber_le

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
w : G.Walk u✝ u✝
ho : Odd w.length
this : 3 ≤ ↑2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v → ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
intro r
    refine r.elim_path fun p => ?_
    refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
    simp [mem_finsetWalkLength_iff]

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

Goal state before:
pp: case a
n r c : ℕ
hr : r > 0
⊢ 1 ≤ #({i ∈ range r | c % r = (n + i) % r})

Tactic:
rw [one_le_card]

Goal state after:
case a
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h
n r c : ℕ
hr : r > 0
⊢ c % r = (n + ((r - 1) * n + c) % r) % r

Tactic:
rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
      Nat.mul_add_mod_self_left]

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

Goal state before:
pp: case inj'.inr
α : 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
i₂ : Fin r
j₂ : Fin t
hne✝ : i₁ = i₂ → j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

Tactic:
· refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
        exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ :
  Tendsto (fun x ↦ 1 / H.turanDensity * (↑(extremalNumber x H) / ↑(x.choose 2))) atTop
    (𝓝 (1 / H.turanDensity * H.turanDensity))
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)

Tactic:
one_div_mul_cancel h,

Goal state after:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun x ↦ 1 / H.turanDensity * (↑(extremalNumber x H) / ↑(x.choose 2))) atTop (𝓝 1)
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)