mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
⊢ a ≠ 0

Tactic:
exact fun ha ↦ D'.rep_nonzero (by simp [← hD, ha])

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)

Tactic:
rw [← card_derangements_invariant (card_fin _)]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ↑(numDerangements (n + 1)) = ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n + 1 - k))

Tactic:
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
    -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
    intro x hx
    have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
    rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
exact ⟨And.left, fun h ↦ ⟨h.ne, trivial, trivial⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
K : Type u_3
inst✝ : Field K
b c d : ℙ K (Fin 3 → K)
hbc : b.orthogonal c
hbd : b.orthogonal d
a : Fin 3 → K
ha : a ≠ 0
hac : (Projectivization.mk K a ha).orthogonal c
had : (Projectivization.mk K a ha).orthogonal d
⊢ Projectivization.mk K a ha = b ∨ c = d

Tactic:
induction b with

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * (c + 1)! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
factorial_succ,

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < ([U] ++ ↑p ++ [D]).length
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))

Tactic:
length_append,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < [U].length + (↑p).length + [D].length
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this : count U ↑p = count D ↑p
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail

Tactic:
rw [← cons_tail_dropLast_concat hn.1, count_append, count_cons] at this

Goal state after:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this :
  (count U (↑p).dropLast.tail + if (U == U) = true then 1 else 0) + count U [D] =
    count D (U :: (↑p).dropLast.tail ++ [D])
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
⊢ uniformBell 1 n = 1

Tactic:
simp only [uniformBell_eq, Finset.range_one, Finset.prod_singleton, zero_mul,
    zero_add, choose_self]

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

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (U :: ↑p ++ [D]).length

Tactic:
length_append,

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (U :: ↑p).length + [D].length
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (mud * zeta 𝕜) a b = 1 a b

Tactic:
simp only [mul_boole, one_apply, mul_apply, zeta_apply]

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ([U] ++ ↑p ++ [D]).length ≤ (↑p).length + 1 + 1

Tactic:
length_append,

Goal state after:
p : DyckWord
⊢ [U].length + (↑p).length + [D].length ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z

Tactic:
simp_rw [mul_apply, sum_mul]

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

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)

Tactic:
length_append,

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = List.take (r'.length + (↑p).length - (↑p).length) (r' ++ ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = ↑r

Tactic:
simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']

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

Goal state before:
pp: case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)

Tactic:
exact fun _ _ _ _ _ _ ↦ Commute.mul_mul_mul_comm (by simp : _ = _) _ _

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

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (node () p.insidePart.toTree p.outsidePart.toTree) = p

Tactic:
ofTree

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ pentagonal k = (k * (3 * k - 1) / 2).toNat

Tactic:
by rfl

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G}, A.Nonempty → #A ≤ t → ex A ∈ M
this : (M ∪ {κ + 1}).Nonempty
⊢ False

Tactic:
let k := (M ∪ {κ + 1}).min' this

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G}, A.Nonempty → #A ≤ t → ex A ∈ M
this : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this
⊢ False
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := ⋯
hK : K < 1
ex : Finset G → ℝ := ⋯
κ : ℝ := ⋯
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#((↑H).toFinset * S)) ≤ (2 / ε - 1) * ↑(#(↑H).toFinset)

Tactic:
rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]

Goal state after:
case hab
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ (1 - K) * ↑(#((↑H).toFinset * S)) ≤ (1 - K) * ((2 / ε - 1) * ↑(#(↑H).toFinset))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hA₀ : A.Nonempty
hA₁ : ↑(#(A * A)) ≤ (2 - ε) * ↑(#A)
⊢ #A ≤ #A

Tactic:
by rfl

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm fun x y ↦ e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)

Tactic:
aesop (add simp symm_def)

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
⊢ ↑(↑f ↑x) - #s < Fintype.card ↥sᶜ

Tactic:
by
        have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)
        simp at this ⊢
        omega

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

pp: case h.right
σ : 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
⊢ (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)) ∧
    ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
· simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]
      simp only [smul_mul_assoc, ← smul_eq_iff_eq_inv_smul, Units.smul_isUnit]
      nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]
      rw [mul_comm, smul_eq_C_mul]

Goal state after:
case h.right
σ : 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
⊢ (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)) ∧
    ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
⊢ p.length = 0

Tactic:
have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ p.length = 0
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case neg
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : ¬c ∈ S
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

Tactic:
refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
      simp [comp_toPath_eq_cons]

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
q : Path b a
h : p.comp q = nil
⊢ q.length = 0

Tactic:
have hlen : (p.comp q).length = 0 := by
    simpa using congrArg Path.length h

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
h : p.comp q = nil
hlen : (p.comp q).length = 0
⊢ q.length = 0
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
q : Path b a
x✝ : p.length = 0 ∧ q.length = 0
hp : p.length = 0
hq : q.length = 0
⊢ p.comp q = nil

Tactic:
induction p with
  | nil => simpa using (length_eq_zero_iff q).mp hq
  | cons p' _ ihp => simp at hp

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
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
this : Finsupp.degree (degLex.degree (h i) + degLex.degree (Alon.P (S i) i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
Alon.degree_P,

Goal state after:
case neg
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
this : Finsupp.degree (degLex.degree (h i) + single i #(S i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜

Tactic:
· rw [← erase_insert ha]
    exact erase_mem_compression_of_mem_compression h

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ (↑m)⁻¹ ≤ ↑(#({x ∈ Ioc 0 n | x % m = 1})) / ↑n

Tactic:
le_div_iff₀ (Nat.cast_pos.2 hn),

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ (↑m)⁻¹ * ↑n ≤ ↑(#({x ∈ Ioc 0 n | x % m = 1}))
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑(#({x ∈ Ioc 0 n | x % m = 1}))

Tactic:
apply (Nat.cast_le.2 (card_le_card this)).trans'

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑(#(image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m))))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
h : a ∈ lowerClosure ↑s
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id

Tactic:
obtain ⟨ℬ, hb, h⟩ := h

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
ℬ : α
hb : ℬ ∈ ↑s
h : a ≤ ℬ
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id
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:
by
  simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (t ∈ 𝒜.sup fun s ↦ image (fun a ↦ insert a s) sᶜ) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Tactic:
mem_sup,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ i ∈ 𝒜, t ∈ image (fun a ↦ insert a i) iᶜ) ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c

Tactic:
simp_rw [← inf_eq_left, inf_sup_left]

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
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_inf]

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

Goal state before:
pp: case refine_3
α : 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
⊢ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'

Tactic:
rintro ⟨w, hwB, hw𝒜'⟩

Goal state after:
case refine_3
α : 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) ∈ 𝒜'
⊢ False
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)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ ↑𝒜

Tactic:
h𝒜.empty_mem_iff,

Goal state after:
α : 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 ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬↑𝒜 = {∅}
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

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

Tactic:
rw [z lt]

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
have h := calc
    ∑ s ∈ 𝒜, ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0)⁻¹
    _ ≤ ∑ s ∈ 𝒜, ((Fintype.card α).choose #s : ℚ≥0)⁻¹ := by
      gcongr with s hs
      · exact mod_cast choose_pos s.card_le_univ
      · exact choose_le_middle _ _
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_inv_choose h𝒜

Goal state after:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
h : ∑ s ∈ 𝒜, (↑((Fintype.card α).choose (Fintype.card α / 2)))⁻¹ ≤ 1
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ p, p.IsPath

Tactic:
obtain ⟨W⟩ := hr

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
W : G.Walk u v
⊢ ∃ p, p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

Tactic:
ConnectedComponent.sound (hv'.mono h)

Goal state after:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = 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
x y : α
h : Disjoint (f (hs.index x) '' s (hs.index x)) (f (hs.index y) '' s (hs.index y))
⊢ hs.piecewise f x ≠ hs.piecewise f y

Tactic:
exact h.ne_of_mem (mem_image_of_mem _ (hs.mem_index x)) (mem_image_of_mem _ (hs.mem_index y))

Goal state after: