mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a✝ a'✝ : α
b✝ b'✝ : β
c✝ c'✝ : γ
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x✝¹ x✝ : α × β × γ
a : α
b : β
c : γ
a' : α
b' : β
c' : γ
⊢ (fun x ↦ {in₀ x.1, in₁ x.2.1, in₂ x.2.2}) (a, b, c) = (fun x ↦ {in₀ x.1, in₁ x.2.1, in₂ x.2.2}) (a', b', c') →
    (a, b, c) = (a', b', c')

Tactic:
by simpa only [Finset.Subset.antisymm_iff, Finset.subset_iff,
    mem_insert, mem_singleton, forall_eq_or_imp, forall_eq, Prod.mk_inj, or_false, false_or,
    in₀, in₁, in₂, Sum.inl.inj_iff, Sum.inr.inj_iff, reduceCtorEq] using And.left

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
by
  apply (edgeDensity_chunk_aux (hP := hP) hPα hPε hU hV).trans
  have key : (16 : ℝ) ^ #P.parts = #((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts) := by
    rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]; norm_cast
  simp_rw [key]
  convert! sum_div_card_sq_le_sum_sq_div_card (α := ℝ)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
u : V
hu : u ≠ 0
h : (mk K u hu).submodule = v.submodule
⊢ mk K u hu = v

Tactic:
induction v using ind with

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
v : ℙ K V
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v

Tactic:
induction v using ind with

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (w✝ • w✝¹ • (↑x✝³ ⬝ᵥ ↑x✝²) = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
smul_smul,

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ ((w✝ * w✝¹) • (↑x✝³ ⬝ᵥ ↑x✝²) = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : b • a • (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨b • a • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
smul_smul,

Goal state after:
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (b * a) • (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁵ else ⟨(b * a) • (crossProduct ↑x✝⁴) ↑x✝¹, ⋯⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)

Tactic:
Fintype.card_compl_set

Goal state after:
n : ℕ
a : Fin (n + 1)
⊢ card (Fin (n + 1)) - card ↑{a} = card (Fin n)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a •> a⁻¹ •> ↑A = ↑A

Tactic:
smul_inv_smul

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ ↑A = ↑A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))

Tactic:
refine (h₁ _ hc d hd).trans_le ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ ↑(#(c⁻¹ •> A ∩ d •> A)) ≤ ↑(#(A ∩ (c * d) •> A))
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ ∃ p ∈ l₁, p ∈ l₂
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case inl
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i = 0
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U])

Tactic:
simp [hi]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
⊢ f = g

Tactic:
refine DFunLike.coe_injective (funext₂ fun a b ↦ ?_)
  by_cases hab : a ≤ b
  · exact h _ _ hab
  · rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]

Goal state after:
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✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ((f • g) • h) a b = (f • g • h) a b

Tactic:
simp only [smul_apply, sum_smul, smul_sum, sum_sigma']

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ (Icc a b).sigma (Icc a), (f a x.snd • g x.snd x.fst) • h x.fst b =
    ∑ x ∈ (Icc a b).sigma fun a ↦ Icc a b, f a x.fst • g x.fst x.snd • h x.snd b
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

Tactic:
← p.cons_tail_dropLast_concat h

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide
          (count U (List.take (0 + 1) (U :: (↑p).dropLast.tail ++ [D])) =
            count D (List.take (0 + 1) (U :: (↑p).dropLast.tail ++ [D]))) =
        true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U
                (List.take ((range (U :: (↑p).dropLast.tail ++ [D]).length)[j] + 1) (U :: (↑p).dropLast.tail ++ [D])) =
              count D
                (List.take ((range (U :: (↑p).dropLast.tail ++ [D]).length)[j] + 1) (U :: (↑p).dropLast.tail ++ [D]))) =
          false)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a b : α
hba : b ≠ a
⊢ l.idxFun i = some a ↔ m.idxFun i = some a

Tactic:
simp only [funext_iff] at hlm ⊢

Goal state after:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l✝ : Line α ι
i✝ : ι
a x : α
l : Line α ι
x✝ : Unit
i : ι
hi : l.idxFun i = none
⊢ (l.idxFun i).elim (Sum.inr ()) Sum.inl = Sum.inr x✝

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l✝ : Line α ι
i✝ : ι
a x : α
l : Line (η → α) ι
e : η
i : ι
hi : l.idxFun i = none
⊢ ((l.idxFun (i, e).1).elim (Sum.inr (i, e).2) fun f ↦ Sum.inl (f (i, e).2)) = Sum.inr e

Tactic:
simp [hi]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
⊢ (M ↾ M.E \ D).IsBase B ↔ M.IsBasis B (M.E \ D)

Tactic:
isBase_restrict_iff

Goal state after:
α : Type u_1
M : Matroid α
B D : Set α
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBasis B (M.E \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

Tactic:
← indep_singleton,

Goal state after:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ M.Indep (K \ I ∪ I)

Tactic:
by simpa [sdiff_union_of_subset hKJ.2]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : 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
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) (Finsupp.single i (⋯.unit⁻¹ • f)) + 0

Tactic:
simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]

Goal state after:
case h.left
σ : 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
⊢ f = ⋯.unit⁻¹ • f * b i
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ (M.sum N).IsBasis I X ↔ M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

Tactic:
simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm,
    Equiv.sumCongr_apply, Equiv.symm_symm, sigma_isBasis_iff, Bool.forall_bool,
    Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]

Goal state after:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ M.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ∧
      N.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ↔
    M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices ≠ []

Tactic:
simp [← length_pos_iff_ne_nil]

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.dropLast ++ [b] = p.vertices

Tactic:
by
  simp_rw [← p.vertices_getLast p.vertices_ne_nil, dropLast_concat_getLast]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := ⟨s, ⋯⟩
h : ι ↑(φ.map e) • φ.obj v = φ.obj (ι s • v)
⊢ φ.obj (ι s • v) = ι s • φ.obj v

Tactic:
have label_eq : (φ.map e).val = s := by
    -- `φm` says `φ ⋙q labelling = labelling`
    -- So `(φ ⋙q labelling).map e = labelling.map e`
    have : (φ ⋙q labelling W ι).map e = (labelling V ι).map e := by
      rw [φm]
    simp only [Prefunctor.comp_map, labelling_map] at this
    exact this

Goal state after:
V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := ⟨s, ⋯⟩
h : ι ↑(φ.map e) • φ.obj v = φ.obj (ι s • v)
label_eq : ↑(φ.map e) = s
⊢ φ.obj (ι s • v) = ι s • φ.obj v
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : h i = 0
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: 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}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ #(image f (sA.disjSum sB)) ≤ #(Ioo 0 n)

Tactic:
by gcongr; grind [mem_disjSum]

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

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

Tactic:
simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (({b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}).inf' ⋯ fun x ↦ id x) =
    ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2
Module: Mathlib.Order.Irreducible

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

Tactic:
classical
  apply WellFoundedLT.induction a _
  clear a
  rintro a ih
  by_cases ha : SupIrred a
  · exact ⟨{a}, by simp [ha]⟩
  rw [not_supIrred] at ha
  obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
  · exact ⟨∅, by simp [ha.eq_bot]⟩
  obtain ⟨s, rfl, hs⟩ := ih _ hb
  obtain ⟨t, rfl, ht⟩ := ih _ hc
  exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1 - supSum 𝒜ᶜˢ = 1

Tactic:
supSum_of_univ_notMem h𝒜₁.compls,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1 - ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ = 1

α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ univ ∉ 𝒜ᶜˢ
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : 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)
⊢ #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Tactic:
refine card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun s hs => ?_)

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 ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

case refine_2
α : 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 ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
grind [falling, mem_sup]

Goal state after:
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)
⊢ ↑((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) ⊆ {s | a ∉ s}

Tactic:
simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_ofPred_eq, and_imp,
      mem_shatterer]

Goal state after:
α : 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
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_2
α : 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)
s : Finset α
hs : s ∈ (memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer
t : Finset α
ht : t ⊆ insert a s
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
simp only [mem_inter, mem_shatterer] at hs

Goal state after:
case refine_3.refine_2
α : 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)
s t : Finset α
ht : t ⊆ insert a s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
⊢ 𝒜.Shatters s

Tactic:
intro t ht

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
⊢ ¬⊥.Connected

Tactic:
simp [not_preconnected_bot, connected_iff]

Goal state after: