mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x✝ s✝) S).join.destruct (cons a ((cons x✝ s✝).append S.join)).destruct

Tactic:
simpa only [BisimO, join_cons_cons, destruct_cons, cons_append, true_and] using
          Or.inr ⟨_, _, S, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
Hp,

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ (of v).s.get? (n + 1) = some { a := 1, b := ↑p'.b }
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
n : ℕ
hb : b.drop n ≠ nil
⊢ motive (a.drop n) (b.drop n)

Tactic:
induction n with
    | zero => simpa
    | succ m ih =>
      simp only [drop] at hb ⊢
      generalize b.drop m = tb at *
      cases tb with
      | nil => simp at hb
      | cons tb_hd tb_tl =>
        simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
        obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
        simpa [ha]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = (fib 0).gcd (fib n✝)

Tactic:
| H0 =>

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      n =
    (↑f).coeff n

Tactic:
· rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
      simpa using hn

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1

Tactic:
by
  simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    x ^ n * (1 - x) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
← Commute.mul_pow,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x * (1 - x)) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

Tactic:
by
  classical
  simp_rw [DFinsupp.sumAddHom_apply]
  exact c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ (∃ a, ∃ (_ : ↑a ≤ k), ((f - μ • 1) ^ a) x = 0) ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0

Tactic:
exists_prop

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i : Fin 2), IsIdempotentElem (o i)

pp: case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

pp: case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0

Tactic:
· intro i
    fin_cases i <;> simpa [o]

Goal state after:
case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson = matrix n I.jacobson

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson

case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

Tactic:
apply le_antisymm

Goal state after:
case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n

case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V)
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Tactic:
replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)

Tactic:
#adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
      ```
      -/

Goal state after:
case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let W₀ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₀
  let W₁ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₁
  let W₂ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₂
  let W₃ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₃
  let W₄ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₄
  let W₅ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₅
  let g₀ : W₀ →ₗ[k] W₁ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₀ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₁ : W₁ →ₗ[k] W₂ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₁ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₂ : W₂ →ₗ[k] W₃ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₂ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₃ : W₃ →ₗ[k] W₄ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₃ ∘ₗ ULift.moduleEquiv.toLinearMap
  let g₄ : W₄ →ₗ[k] W₅ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₄ ∘ₗ ULift.moduleEquiv.toLinearMap
  have := sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux g₀ g₁ g₂ g₃ g₄
    (inj := by simpa [g₀]) (surj := by simpa [g₄])
  simp only [W₀, W₁, W₂, W₃, W₄, W₅, finrank_ulift] at this
  apply this <;>
  simpa only [g₀, g₁, g₂, g₃, g₄, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) = max #α ℵ₀

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) ≤ max #α ℵ₀

case a
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

Tactic:
rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]

Goal state after:
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ #(FreeAlgebra R X) = 1

Tactic:
rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, mk_eq_one]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
⊢ Function.Injective ⇑toFreeMonoid

Tactic:
by
  rintro ⟨x, xs⟩ ⟨y, ys⟩ h
  simp only [toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq] at h
  simpa using h

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ R[x]
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
simp_rw [← coe_subset]
  push_cast
  exact Set.subset_smul_set_iff

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
Module: Mathlib.Algebra.Group.Pointwise.Set.Small

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑(-s)

Tactic:
rw [← Set.image_neg_eq_neg]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x✝ x y : M
hx : x ∈ closure (Set.range f)
hy : y ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2
hy' : ∃ a, y = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, x * y = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'

Goal state after:
case mul
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, ((v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x✝ x y : M
hx : x ∈ closure (Set.range f)
hy : y ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2
hy' : ∃ a, y = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, x * y = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'

Goal state after:
case mul
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, ((v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ closure {a, b} = zmultiples ↑(a.gcd b)

Tactic:
apply le_antisymm

Goal state after:
case a
a b : ℤ
⊢ closure {a, b} ≤ zmultiples ↑(a.gcd b)

case a
a b : ℤ
⊢ zmultiples ↑(a.gcd b) ≤ closure {a, b}
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hj' : v j ∈ closure (v '' t)
hk' : v k ∈ closure (v '' t)
hjk : v i ∈ closure (v '' t)
⊢ False

Tactic:
exact hi₁ hjk

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        i)

Tactic:
match i with | 0 | 1 => simp <;> lia

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op

Tactic:
rw [← op_comp, hp]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ¬↑j' ≤ ↑i'
⊢ ∃ a, ∃ (ha : a ∈ S), φ a ha = (i', j')

Tactic:
not_le

Goal state after:
case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ ∃ a, ∃ (ha : a ∈ S), φ a ha = (i', j')
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑(φ (i, j) hij).1 * (-1) ^ ↑(φ (i, j) hij).2)

pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
· simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
      apply mul_comm

Goal state after:
case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ Function.Surjective (Hom.toOrderHom f).toFun

Tactic:
dsimp; rwa [← epi_iff_surjective]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + (i + 1) = m
hj' : ↑j = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
obtain _ | m := m

Goal state after:
case succ.zero
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
j : Fin (0 + 1)
hi' : n + (i + 1) = 0
hj' : ↑j = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : ↑j = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc = (Hom.toOrderHom θ) (x.castPred ⋯).succ

Tactic:
apply le_antisymm

Goal state after:
case h.a
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc ≤ (Hom.toOrderHom θ) (x.castPred ⋯).succ

case a
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc