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

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ 1 + m₂✝ 1) * n✝ 2 - (m₁✝ 2 + m₂✝ 2) * n✝ 1, (m₁✝ 2 + m₂✝ 2) * n✝ 0 - (m₁✝ 0 + m₂✝ 0) * n✝ 2,
      (m₁✝ 0 + m₂✝ 0) * n✝ 1 - (m₁✝ 1 + m₂✝ 1) * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1 + (m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1),
      m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2 + (m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2),
      m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0 + (m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0)]

Tactic:
apply vec3_eq <;> ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![c✝ • m✝ 1 * n✝ 2 - c✝ • m✝ 2 * n✝ 1, c✝ • m✝ 2 * n✝ 0 - c✝ • m✝ 0 * n✝ 2, c✝ • m✝ 0 * n✝ 1 - c✝ • m✝ 1 * n✝ 0] =
    ![c✝ • (m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2), c✝ • (m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0)]

Tactic:
smul_sub,

Goal state after:
case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![c✝ • m✝ 1 * n✝ 2 - c✝ • m✝ 2 * n✝ 1, c✝ • m✝ 2 * n✝ 0 - c✝ • m✝ 0 * n✝ 2, c✝ • m✝ 0 * n✝ 1 - c✝ • m✝ 1 * n✝ 0] =
    ![c✝ • (m✝ 1 * n✝ 2) - c✝ • (m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0) - c✝ • (m✝ 0 * n✝ 2),
      c✝ • (m✝ 0 * n✝ 1) - c✝ • (m✝ 1 * n✝ 0)]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ 2 + n₂✝ 2) - m✝ 2 * (n₁✝ 1 + n₂✝ 1), m✝ 2 * (n₁✝ 0 + n₂✝ 0) - m✝ 0 * (n₁✝ 2 + n₂✝ 2),
      m✝ 0 * (n₁✝ 1 + n₂✝ 1) - m✝ 1 * (n₁✝ 0 + n₂✝ 0)] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1 + (m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1),
      m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2 + (m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2),
      m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0 + (m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0)]

Tactic:
apply vec3_eq <;> ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * c✝ • n✝ 2 - m✝ 2 * c✝ • n✝ 1, m✝ 2 * c✝ • n✝ 0 - m✝ 0 * c✝ • n✝ 2, m✝ 0 * c✝ • n✝ 1 - m✝ 1 * c✝ • n✝ 0] =
    ![c✝ • (m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2), c✝ • (m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0)]

Tactic:
smul_sub,

Goal state after:
case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * c✝ • n✝ 2 - m✝ 2 * c✝ • n✝ 1, m✝ 2 * c✝ • n✝ 0 - m✝ 0 * c✝ • n✝ 2, m✝ 0 * c✝ • n✝ 1 - m✝ 1 * c✝ • n✝ 0] =
    ![c✝ • (m✝ 1 * n✝ 2) - c✝ • (m✝ 2 * n✝ 1), c✝ • (m✝ 2 * n✝ 0) - c✝ • (m✝ 0 * n✝ 2),
      c✝ • (m✝ 0 * n✝ 1) - c✝ • (m✝ 1 * n✝ 0)]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h1 : (crossProduct v) w = 0
h2 : LinearIndependent F ![v, w]
⊢ False

Tactic:
simp_rw [cross_apply, cons_eq_zero_iff, zero_empty, and_true, sub_eq_zero] at h1

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
⊢ False
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
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m ↦ m • ↑⟨v, hv⟩) a = ↑⟨u, hu⟩
⊢ (projectivizationSetoid L W) ⟨f ↑⟨u, hu⟩, ⋯⟩ ⟨f ↑⟨v, hv⟩, ⋯⟩

Tactic:
use Units.map σ.toMonoidHom a

Goal state after:
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
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m ↦ m • ↑⟨v, hv⟩) a = ↑⟨u, hu⟩
⊢ (fun m ↦ m • ↑⟨f ↑⟨v, hv⟩, ⋯⟩) ((Units.map ↑σ) a) = ↑⟨f ↑⟨u, hu⟩, ⋯⟩
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬b ≠ m ∨ b ∉ t
⊢ b < a

Tactic:
not_ne_iff

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b = m ∨ b ∉ t
⊢ b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : ¬b ≠ m ∨ b ∉ t
⊢ b < w

Tactic:
not_ne_iff

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b = m ∨ b ∉ t
⊢ b < w
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Tactic:
by
  -- get some basic results about the size of Fin (n+1) plus or minus an element
  have h1 : ∀ a : Fin (n + 1), card ({a}ᶜ : Set (Fin (n + 1))) = card (Fin n) := by
    intro a
    rw [Fintype.card_compl_set]
    simp
  have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by simp only [card_fin, card_option]
  -- rewrite the LHS and substitute in our fintype-level equivalence
  simp only [card_derangements_invariant h2,
    card_congr
      (@derangementsRecursionEquiv (Fin (n + 1))
        _), -- push the cardinality through the Σ and ⊕ so that we can use `card_n`
    card_sigma,
    card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin,
    mul_add, Nat.cast_id]

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

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (n + 1 + 1)) = (↑(n + 1) + 1) * ↑(numDerangements (n + 1)) - (-1) ^ (n + 1)

Tactic:
simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + ↑1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + ↑1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - (-1) ^ n * -1
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l

Tactic:
classical
    obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
    let s : Finset (P × L) := Set.toFinset { i | i.1 ∈ i.2 }
    have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 := by
      rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
      simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
    have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 := by
      rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
      on_goal 1 =>
        rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
        · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
          simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
          change pointCount P l • _ = lineCount L (f l) • _
          rw [hf2]
      all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
    have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
      rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
    rw [← Set.toFinset_compl] at step3
    exact
      ((Finset.sum_eq_sum_iff_of_le fun i hi =>
              HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
          step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a

Tactic:
refine subset_antisymm ?_ ?_

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a

case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p ++ [U]) = count D (take ((↑p).length - 1) ↑p ++ [U])
⊢ False

Tactic:
count_append,

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + count U [U] = count D (take ((↑p).length - 1) ↑p) + count D [U]
⊢ False
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U (List.take i ↑p ++ List.drop i ↑p) = count D (List.take i ↑p ++ List.drop i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)

Tactic:
count_append,

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U (List.take i ↑p) + count U (List.drop i ↑p) = count D (List.take i ↑p ++ List.drop i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
take_append_of_le_length (by rw [singleton_append, length_cons]; lia),

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

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

Tactic:
count_cons_of_ne (by simp),

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) < count U (U :: List.take (i - 1) ↑p)
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 ++ [D]) = count D (U :: (↑p).dropLast.tail ++ [D])
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail

Tactic:
count_append,

Goal state after:
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
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 (List.take j ↑p) ++ List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 (List.take j ↑p) ++ List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
count_append,

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 (List.take j ↑p)) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 (List.take j ↑p) ++ List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 (List.take j ↑p)) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 (List.take j ↑p) ++ List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
count_append,

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 (List.take j ↑p)) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 (List.take j ↑p)) + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ 1 * 1 = 1

Tactic:
one_mul

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ 1 = 1
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 : α
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b ↑x

Tactic:
rw [muFun']

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

Goal state before:
pp: case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
p : (n + 1).Partition
a✝ : p ∈ Finset.univ
⊢ ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell

Tactic:
exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell)

Goal state after:
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
y z : α
hz : z ∈ Ici y
⊢ f z = 1 * f z

Tactic:
one_mul

Goal state after:
𝕜 : 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
y z : α
hz : z ∈ Ici y
⊢ f z = f z
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, (mu 𝕜 * zeta 𝕜) x z * f z = ∑ y ≥ x, ∑ z ≥ y, 1 x z * f z

Tactic:
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]

Goal state after:
𝕜 : 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
⊢ (∑ x_1 > x, if x_1 ≤ x then f x else 0) = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
count_append,

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' + count U ↑p = count D (r' ++ ↑p)
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑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
hq : count U r' + count U ↑p = count D (r' ++ ↑p)
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
count_append,

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

Goal state before:
pp: p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength ≠ q.semilength

Tactic:
contrapose pnq

Goal state after:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p.semilength = q.semilength
⊢ p = q
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ (1 * x_1) * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ i ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
    i ∉ toFinsuppAntidiag '' ↑univ →
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff (i i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1))) =
        0

pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ i ∈ univ,
    (Multiset.toFinsupp i.parts).prod f =
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
        (coeff (i.toFinsuppAntidiag i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1)))

Tactic:
· exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f (by simp) hg (by simpa using hg')

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ i ∈ univ,
    (Multiset.toFinsupp i.parts).prod f =
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
        (coeff (i.toFinsuppAntidiag i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1)))
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder + 4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder

Tactic:
by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia

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]
    simp [Nat.factorial_succ]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ x ∈ Set.range Neg.neg

Tactic:
use -x

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ - -x = x
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.IsLink e = G₂.IsLink f
⊢ G₁.Inc e = G₂.Inc f

Tactic:
· simp [funext_iff, Inc, h]

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

Goal state before:
pp: case e'_3.e'_5
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)

Tactic:
simp [edgeSet_eq_setOfPred_exists_isLink, h]

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case ht.refine_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ (N ∩ {m' | m' * m = m}).Nonempty

Tactic:
← scaling_eq_self

Goal state after:
case ht.refine_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ (fun x ↦ x * m) '' N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ (N ∩ {m' | m' * m = m}).Nonempty