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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ f a b + g a b = 0

Tactic:
apply_eq_zero_of_not_le h,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ 0 + 0 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ -f a b = 0

Tactic:
apply_eq_zero_of_not_le h,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ -0 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ f a b - g a b = 0

Tactic:
apply_eq_zero_of_not_le h,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ 0 - 0 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (mu' 𝕜) a b = -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
rw [mu'_apply, if_neg h]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : BoundedOrder α
⊢ eulerChar 𝕜 αᵒᵈ = eulerChar 𝕜 α

Tactic:
simp [eulerChar, ← mu_toDual 𝕜 (α := α)]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
pq : p < q
⊢ p.semilength < q.semilength

Tactic:
obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq

Goal state after:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength < q.semilength
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = d

Tactic:
obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg
    refine Eq.trans ?_ h1
    suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum]
    apply sum_subset_zero_on_sdiff h2 (by simp)
    exact fun x hx ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) * ∏' (i : ℕ), (1 - X ^ (i + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ ∏' (b : ℕ), (if ¬m ∣ b + 1 then ∑' (j : ℕ), X ^ ((b + 1) * j) else 1) * (1 - X ^ (b + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S A : Finset G
a : G
⊢ expansion K S (a •> A) = expansion K S A

Tactic:
simp [expansion, smul_mul_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

Tactic:
exact (hasSum_pow_pentagonal_sub_pentagonalSeries R).summable

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
⊢ ↑(diagonal α ι) x = fun x_1 ↦ x

Tactic:
by
  ext; simp [diagonal]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

Tactic:
Matroid.delete_isBase_iff

Goal state after:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hι : (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C' l
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
rcases hι with (⟨s, sr⟩ | h)

Goal state after:
case pos.succ.inl
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

case pos.succ.inr
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
h : ∃ l, IsMono C' l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : 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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf✝ : ∃ i, m.degree (b i) ≤ m.degree f
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.reduce ⋯ f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

Tactic:
exact deg_reduce

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

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by
      simpa using (mem_vertices_cons pPrev e).1 hv

Goal state after:
case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
h : φ.obj y₁ = φ.obj u
h' : (φ.mapPath p₁).cons (φ.map e₁) ≍ φ.mapPath Path.nil
⊢ False

Tactic:
← Path.cast_eq_iff_heq rfl h,

Goal state after:
case cons.nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
h : φ.obj y₁ = φ.obj u
h' : Path.cast ⋯ h ((φ.mapPath p₁).cons (φ.map e₁)) = φ.mapPath Path.nil
⊢ False
Module: Mathlib.Combinatorics.Quiver.Covering

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

Tactic:
use ⟨u, Path.nil⟩

Goal state after:
case h
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = ⟨φ.obj u, Path.nil⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1

Tactic:
simp only [Set.not_subset, forall_exists_index, and_imp]

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ∀ x ∈ {0}ᶜ, x ∉ A → schnirelmannDensity A < 1
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
this : ∀ i ∈ range (n + 1), f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
⊢ (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) 0 - (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) (n + 1) = 1

Tactic:
simp [choose_zero_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
⊢ ∀ s ∈ powersetCard n univ,
    ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
s

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
s : Finset α
⊢ s ∈ powersetCard n univ →
    ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [SupIrred, not_and_or]
  push Not
  rw [exists₂_congr]
  simp +contextual [@eq_comm _ _ a]

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ ∅.sup f ↔ ∃ i ∈ ∅, a ≤ f i

Tactic:
simp [ha.ne_bot]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∈ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b).erase a = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∉ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b) = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

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:
by
  simp_rw [mem_coe, mem_nonMemberSubfamily]
  exact And.imp (h hts) (mt <| @hts _)

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
refine card_le_card ?_

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image s.erase s ⊆ bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
q_a q_b : Quotient r
⊢ Quot.lift f f_respects_relation q_a = Quot.lift f f_respects_relation q_b → q_a = q_b

Tactic:
h_eq

Goal state after:
case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
q_a q_b : Quotient r
h_eq : Quot.lift f f_respects_relation q_a = Quot.lift f f_respects_relation q_b
⊢ q_a = q_b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
⊢ u ∈ G.support

Tactic:
by
  let p : G.Walk u v := Classical.choice h
  have hp : ¬p.Nil := Walk.not_nil_of_ne huv
  exact mem_support_of_mem_walk_support p hp p.start_mem_support

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hc : IsPartition c
⊢ (mkClasses c ⋯).classes = c

Tactic:
ext s
  constructor
  · rintro ⟨y, rfl⟩
    obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y
    rwa [← eq_eqv_class_of_mem _ hb hy]
  · exact exists_of_mem_partition hc

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

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } r ≤
      { toFun := fun r ↦ ⟨r.classes, ⋯⟩, invFun := fun C ↦ mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } s ↔
    r ≤ s

Tactic:
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]
    rfl

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

Goal state before:
pp: case mpr
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 ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = r

Tactic:
← Ah.2,

Goal state after:
case mpr
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 ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = #A
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n✝ : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst✝ : Fintype α
n : ℕ
hc : G.Colorable n
hn : card (Fin n) ≤ card α
⊢ G.Coloring α

Tactic:
exact G.recolorOfCardLE hn hc.some

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' | G.Colorable n'})
⊢ G.Colorable n

Tactic:
exact this.mono h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑l

Tactic:
grw [← hkl]

Goal state after:
V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑k
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 ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length

Tactic:
exact edist_le _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ p.toSubgraph.neighborSet v
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [h.neighborSet_toSubgraph_endpoint] at this

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ {p.snd, p.penultimate}
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : 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
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y ≤ ↑w_app.length

Tactic:
exact edist_le _

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝¹ : (hasse α).Adj a b
this✝ : (hasse α).Adj b c
this : (hasse α).Adj a c
⊢ False

Tactic:
grind [hasse_adj, CovBy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1) ∨ y.1 ⋖ x.1 ∧ x.2 = y.2 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1 ↔
    (x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ y.1 ⋖ x.1 ∧ x.2 = y.2) ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 ∨ y.2 ⋖ x.2 ∧ x.1 = y.1

Tactic:
or_or_or_comm

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
h : A.compl = B.compl
i j : V
⊢ A i j = B i j

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
    as we are relying on seeing through the definition of `Matrix`, and `of`.
    The original proof was: `grind [of, congr($h i j), compl, IsAdjMatrix]` -/
    simp [compl] at h; grind [congr($h i j), IsAdjMatrix]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
h : ∃ a b c, ¬G.Adj a b ∧ ¬G.Adj b c ∧ G.Adj a c
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
obtain ⟨_, _, _, h1, h2, h3⟩ := h

Goal state after:
α : Type u
G : SimpleGraph α
w✝² w✝¹ w✝ : α
h1 : ¬G.Adj w✝² w✝¹
h2 : ¬G.Adj w✝¹ w✝
h3 : G.Adj w✝² w✝
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := ⋯
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ #G.edgeFinset < #(G ⊔ edge x y).edgeFinset

Tactic:
convert! Nat.lt_add_one #G.edgeFinset

Goal state after:
case e'_4
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ #(G ⊔ edge x y).edgeFinset = #G.edgeFinset + 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph (n + r) r).edgeFinset = #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2

Tactic:
rw [← mul_right_inj' two_ne_zero]
  simp_rw [mul_add, ← sum_degrees_eq_twice_card_edges,
    degree, neighborFinset_eq_filter, turanGraph, card_filter]
  conv_lhs =>
    enter [2, v]
    rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]
  rw [sum_add_distrib,
    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range n, if v % r ≠ w % r then 1 else 0,
    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range r, if v % r ≠ (n + w) % r then 1 else 0,
    sum_range_add, sum_range_add, add_assoc, add_assoc]
  congr 1; · simp [← Fin.sum_univ_eq_sum_range]
  rw [← add_assoc, sum_comm]; simp_rw [ne_comm, ← two_mul]; congr
  · conv_rhs => rw [← card_range n, ← smul_eq_mul, ← sum_const]
    congr!; exact sum_ne_add_mod_eq_sub_one
  · rw [mul_comm 2, Nat.choose_two_right, Nat.div_two_mul_two_of_even (Nat.even_mul_pred_self r)]
    conv_rhs => enter [1]; rw [← card_range r]
    rw [← smul_eq_mul, ← sum_const]
    congr!; exact sum_ne_add_mod_eq_sub_one

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
p : G.Walk v u
x y : V
xy : G.Adj (x, y).1 (x, y).2
xC : { fst := x, snd := y, adj := xy }.toProd.1 ∈ ↑C
ynC : { fst := x, snd := y, adj := xy }.toProd.2 ∉ ↑C
⊢ False

Tactic:
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)

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 (Fintype.card (Fin (n + 1))) H) / ↑((n + 1).choose 2) ≤ ↑(extremalNumber n H) / ↑(n.choose 2)

Tactic:
div_le_iff₀ (mod_cast Nat.choose_pos (by linarith)),

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
⊢ ↑(extremalNumber (Fintype.card (Fin (n + 1))) H) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)