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

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hsplit : (count a m)! * rest = ∏ j ∈ m.toFinset.erase 0, (count j m)!
⊢ m.bell * c = m.sum !

Tactic:
simpa [c, hsplit, mul_assoc] using Multiset.bell_mul_eq m

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

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

Tactic:
count_cons

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.DyckWord

Goal state before:
pp: 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

Tactic:
simpa using this

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

Goal state before:
pp: case cons.nil
q : DyckWord
i : ℕ
s : DyckStep
bal : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [s]) ≤ count U (List.take i [s])
hn : { toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

Tactic:
cases s <;> simp at bal

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬findIdx (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0

Tactic:
findIdx_eq,

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[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)

p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
· simp [hn]

Goal state after:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f • (g + h)) a✝¹ b✝ = (f • g + f • h) a✝¹ b✝

Tactic:
exact Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
⊢ f • (g + h) = f • g + f • h

Tactic:
ext; exact Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib

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

Goal state before:
pp: case inl
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
a : α
a✝ : a ≤ a
⊢ ((algebraMap 𝕜 𝕝) (c * d) • 1) a a = ((algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1) a a

pp: case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
a b : α
a✝ : a ≤ b
h : a ≠ b
⊢ ((algebraMap 𝕜 𝕝) (c * d) • 1) a b = ((algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1) a b

Tactic:
· simp only [one_apply, smul_eq_mul, mul_apply, constSMul_apply, map_mul,
            eq_comm, Icc_self]
          simp

Goal state after:
case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
a b : α
a✝ : a ≤ b
h : a ≠ b
⊢ ((algebraMap 𝕜 𝕝) (c * d) • 1) a b = ((algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1) a b
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * mu' 𝕜) a b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]

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

Goal state before:
pp: case inr.intro.calc_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l

Tactic:
have : 0 < #A := by positivity

Goal state after:
case inr.intro.calc_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

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

Tactic:
suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]

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

Goal state before:
pp: p : DyckWord
⊢ (p.nest.take ((↑p).length + 1 + 1) ⋯).denest ⋯ = p

Tactic:
convert! p.denest_nest

Goal state after:
p : DyckWord
⊢ p.nest.take ((↑p).length + 1 + 1) ⋯ = p.nest
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:

Tactic:
∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Tactic:
ext x y; simp [Icc_prod_def, sum_mul_sum, h, sum_product]

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

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

Tactic:
simp_rw [h, ite_false, 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.Partition.Glaisher

Goal state before:
pp: case e'_5
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (fun i ↦ if p (i + 1) then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) = fun i ↦
    1 + ∑' (j : ℕ), (if p (i + 1) then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
ext1 i

Goal state after:
case e'_5
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
⊢ (if p (i + 1) then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) =
    1 + ∑' (j : ℕ), (if p (i + 1) then 1 else 0) • X ^ ((i + 1) * (j + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)) = fun i ↦
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
ext1 i

Goal state after:
case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ j ∈ range m, X ^ ((i + 1) * j) = 1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ x ^ (2 * k + x_1 + 3) - 1) atTop (𝓝 (0 - 1))

pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
· exact (hx.comp (add_right_strictMono.add_monotone monotone_const).tendsto_atTop).sub_const _

Goal state after:
case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
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
⊢ Function.Injective fun i ↦ (↑i + 1) * m - 1

pp: case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

Tactic:
· intro a b h
    rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h
    exact SetCoe.ext h

Goal state after:
case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
← two_mul_smallSchroder_succ,

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ stirlingFirst 0 (n✝ + 1) = 0

Tactic:
by rw [stirlingFirst]

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

Goal state before:
pp: case succ
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1 + 1).stirlingFirst 1 = (n + 1)!

Tactic:
rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]

Goal state after:
case succ
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1) * n ! + 0 = (n + 1)!
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (0 + 1) * (n + 1).stirlingSecond (0 + 1) + (n + 1).stirlingSecond 0 = 1

Tactic:
stirlingSecond_succ_zero,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (0 + 1) * (n + 1).stirlingSecond (0 + 1) + 0 = 1
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (F ∩ E(G)) = G.restrict F

Tactic:
by
  rw [inter_comm, restrict_edgeSet_inter]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.deleteEdges F ≤ G

Tactic:
by
  simp [← restrict_edgeSet_sdiff_eq_deleteEdges]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsLoopAt e x ↔ G.IsLoopAt e x ∧ H.IsLoopAt e x

Tactic:
simp [← isLink_self_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.deleteEdges ∅ = G

Tactic:
by
  simp [← restrict_edgeSet_sdiff_eq_deleteEdges]

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

Goal state before:
pp: case refine_1
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map f G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : f w✝¹ = x✝²
right✝ : f w✝ = x✝¹
⊢ (map g G).IsLink x✝³ x✝² x✝¹

Tactic:
grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

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

Goal state before:
pp: case refine_2
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map g G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : g w✝¹ = x✝²
right✝ : g w✝ = x✝¹
⊢ (map f G).IsLink x✝³ x✝² x✝¹

Tactic:
grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
⊢ ¬∃ s, s.lines.card = Fintype.card κ + 1

Tactic:
rintro ⟨s, sr⟩

Goal state after:
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = Fintype.card κ + 1) ∨ ∃ l, IsMono C l
C : (ι → Option α) → κ
s : ColorFocused C
sr : s.lines.card = Fintype.card κ + 1
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D : Set α
⊢ (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D

Tactic:
restrict_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I D : Set α
⊢ M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ ∅ ＼ D

Tactic:
contract_empty,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ＼ D
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
· apply le_trans degree_mul_le
        simp only [hj, hb0, Finsupp.single_eq_same, zero_add]
        apply le_of_eq
        simp only [EmbeddingLike.apply_eq_iff_eq]
        apply degree_smul_of_isRegular (Units.isRegular _)

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M ／ (X ∪ C)).loops ∪ M.closure (X ∪ C) \ C ∩ X

Tactic:
union_comm X,

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = (M ／ (C ∪ X)).loops ∪ M.closure (C ∪ X) \ C ∩ X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

Tactic:
restrict_indep_iff,

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M ／ C).Indep I ∧ I ⊆ R ↔ ((M ↾ (R ∪ C)) ／ C).Indep I