mathlib-initiative/mathlib-tactics huggingface dataset:
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))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ x ∈ range (card α + 1), (↑x)⁻¹

Tactic:
simp only [Finset.sum_congr rfl this, mul_eq_mul_left_iff, cast_eq_zero]

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))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
⊢ ∑ x ∈ range (card α + 1), (↑(card α) - ↑x)⁻¹ = ∑ x ∈ range (card α + 1), (↑x)⁻¹ ∨ card α = 0
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
⊢ n ∈ A + B

Tactic:
let sA := {a ∈ Ioc 0 n | a ∈ A}

Goal state after:
case neg
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

Tactic:
refine mem_shadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = 1 ↔ #t = #t✝ + 1
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:
classical
  dsimp [OrderEmbedding.birkhoffFinset]
  simp [birkhoffSet_sup]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ⊆ s
⊢ s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)

Tactic:
simp_rw [mem_coe, mem_nonMemberSubfamily]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ⊆ s
⊢ s ∈ 𝒜 ∧ a ∉ s → t ∈ 𝒜 ∧ a ∉ t
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ compress u v s ∈ ∂ 𝒜

Tactic:
rw [compress]

Goal state after:
case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ (if Disjoint u s ∧ v ⊆ s then (s ⊔ u) \ v else s) ∈ ∂ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜

Tactic:
← Hcomp.eq

Goal state after:
case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ 0

Tactic:
pow_zero

Goal state after:
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 1
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∨ aᶜ ∈ ↑s

Tactic:
by_contra! ha

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ∀ (x : Finset α), (memberSubfamily a 𝒜).Shatters x → (nonMemberSubfamily a 𝒜).Shatters x → a ∉ x

Tactic:
exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)

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

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

Tactic:
sum_range_succ,

Goal state after:
case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    ↑(#(falling (Fintype.card α - (k + 1)) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - (k + 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) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ =
    ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r))⁻¹

Tactic:
sum_fiberwise_of_maps_to'

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) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ = ∑ i ∈ 𝒜, (↑((Fintype.card α).choose #i))⁻¹

case h
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∀ i ∈ 𝒜, #i ∈ range (Fintype.card α + 1)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ (memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]
    rintro s hs t ht
    obtain ⟨u, hu, rfl⟩ := hs ht
    rw [mem_memberSubfamily] at hu
    refine ⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩
    obtain ⟨v, hv, hsv⟩ := hs.exists_inter_eq_singleton ha
    rw [mem_memberSubfamily] at hv
    rw [← singleton_subset_iff (a := a), ← hsv] at hv
    exact hv.2 inter_subset_right

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

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜

Tactic:
have q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q := by grind

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
by
  simp only [subset_iff, mem_shatterer]; exact fun s hs ↦ hs.of_compression

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

Goal state before:
pp: case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ usable
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
rw [mem_filter] at hUV

Goal state after:
case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
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 β
⊢ hs.piecewise f ⁻¹' t = ⋃ i, s i ∩ f i ⁻¹' t

Tactic:
by
  refine ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩
  · rw [mem_preimage, piecewise_apply, ← mem_preimage] at hx
    exact mem_iUnion_of_mem (hs.index x) (mem_inter (hs.mem_index x) hx)
  · rw [← hi, ← (mem_iff_index_eq hs).mp ha.1] at ha
    simp_all [piecewise_apply]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
⊢ range (hs.piecewise f) = ⋃ i, f i '' s i

Tactic:
by
  refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩
  · rintro ⟨x, rfl⟩
    exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩
  · simp only [← hi, mem_image] at ht
    obtain ⟨a, ha1, ha2⟩ := ht
    refine ⟨a, ?_⟩
    simp only [hs.mem_iff_index_eq] at ha1
    simpa [hs.mem_iff_index_eq, ← ha1] using! ha2

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
G : SimpleGraph V
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    (fun v w ↦ ¬(G.deleteEdges {e}).Reachable v w) a₁ a₂ = (fun v w ↦ ¬(G.deleteEdges {e}).Reachable v w) a₂ a₁

Tactic:
by simp [reachable_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
⊢ False

Tactic:
let pwv := (c.takeUntil v hv).dropUntil w hw

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Walk ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
convert! p.induce s _

Goal state after:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ ∀ x ∈ p.support, x ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: 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
⊢ ∃ a, C a = b

Tactic:
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp

Goal state after:
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)
⊢ ∃ a, C a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
⊢ G.CliqueFree n

Tactic:
have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
  obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne
  have := colorable_chromaticNumber hc'
  refine this.cliqueFree ?_
  rw [← ENat.natCast_toNat_eq_self] at hne
  rw [← hne] at hc
  simpa using hc

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
ih :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
⊢ 𝒜 ⊻ ℬ ⊆ (insert a u).powerset

Tactic:
simpa using sups_subset h𝒜 hℬ

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
u : V
hu : u ∈ G'.verts
⊢ u ∈ (G.connectedComponentMk v).supp

Tactic:
exact ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hle.left rfl⟩ |>.map G'.hom

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
e : Sym2 V
he : e ∈ w.edges
hv'e : v' ∈ e
⊢ v' ∈ G'.verts

Tactic:
exact G'.mem_verts_of_mem_edge (hw he) hv'e

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
have huv : u = v := by aesop

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2

Goal state after:
case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
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]
  exact p.toSubgraph_connected.induce_verts

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Tactic:
obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_ofPred_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

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

Goal state before:
pp: case refine_2.refine_2
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
x : ℕ
hx : x < n
⊢ ∀ {b : Fin n}, (cycleGraph n).Adj ⟨x, hx⟩ b → G.Adj p.support[⟨x, hx⟩.succ] p.support[b.succ]

Tactic:
⟨y, hy⟩

Goal state after:
case refine_2.refine_2
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
x : ℕ
hx : x < n
y : ℕ
hy : y < n
⊢ (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩ → G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a

Tactic:
intro h g hg a ha

Goal state after:
case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
h : ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
g : M
hg : g ∈ s
a : M
ha : ¬a * g = a
⊢ G.Adj (a * g) a
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
u v : M
⊢ (mulCayley (s \ {1})).Adj u v ↔ (mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})).Adj u v

Tactic:
simp +contextual [mulCayley_adj']

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
⊢ extremalNumber n H = {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
let e := Fintype.equivFinOfCardEq hc

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
⊢ extremalNumber n H = {G | H.Free G}.sup fun x ↦ #x.edgeFinset