mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n
    apply_fun MulOpposite.unop at hk
    have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
    rw [this, mul_assoc]
    rcases n with - | n
    · simp at hn
    rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ e₁ = e₂

Tactic:
have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
    clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]

Goal state after:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ e₁ = e₂
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
hi : i ≠ i'
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')

Tactic:
simpa [hi] using c.refl 0

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)

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

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 m : ℕ∞
hm : k ≤ m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
unfold HasUnifEigenvalue at *
  contrapose hk
  rw [← le_bot_iff, ← hk]
  exact (f.genEigenspace _).monotone hm

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 1 * (↑fg).1 a = (↑fg).1 a * (↑fg).2 1

Tactic:
← fg.prop.2.1,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 1 * (↑fg).1 a = (↑fg).2 (a • 1)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).1 x * (↑fg).2 1 = (↑fg).2 x

Tactic:
← fg.prop.2.1,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).2 (x • 1) = (↑fg).2 x
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - (t * μ) • 1) ^ l) m = 0

Tactic:
rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x ^ n.succ)⁻¹ = (x ^ n.succ)⁻¹ * x

Tactic:
rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]

Goal state after:
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ a⁻¹

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

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
hR : Infinite α
⊢ Nonempty (CommRing α)

Tactic:
· have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
    exact ⟨e.commRing⟩

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑↑(n + 1)

Tactic:
Int.cast_negSucc,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C (map (algebraMap R K) q ^ m * C a).leadingCoeff = C a

Tactic:
leadingCoeff_mul,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C ((map (algebraMap R K) q ^ m).leadingCoeff * (C a).leadingCoeff) = C a
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P ^ 2

Tactic:
pow_two

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
⊢ IsDecompOn g (f '' A) S⁻¹

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩
  rcases hf a ha with ⟨γ, γ_mem, hγ⟩
  use γ⁻¹, Finset.inv_mem_inv γ_mem
  rw [hγ, inv_smul_smul, ← hγ, h ha]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
← pairwiseDisjoint_coe,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun i ↦ ↑(i • t)) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ x ^ 0 = 1

Tactic:
npow_zero

Goal state after:
case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: j : ℕ
⊢ (Δ_[1] fun x ↦ ↑(x.choose (j + 1))) = fun x ↦ ↑(x.choose j)

Tactic:
by
  ext n
  simp only [fwdDiff, choose_succ_succ' n j, cast_add, add_sub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ ↑(Iic a * Iic b) ⊆ ↑(Iic (a * b))

Tactic:
by simpa using Set.Iic_mul_Iic_subset' _ _

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
⊢ v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}

Tactic:
simp [f']

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
← pairwiseDisjoint_coe,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (s.PairwiseDisjoint fun i ↦ ↑(i • t)) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
x : X.obj
⊢ Y.uSwitchEquiv ((ConcreteCategory.hom (uSwitch.map f)) (X.uSwitchEquiv.symm x)) = (ConcreteCategory.hom f) x

Tactic:
← uSwitchEquiv_naturality f,

Goal state after:
X Y : FintypeCat
f : X ⟶ Y
x : X.obj
⊢ (ConcreteCategory.hom f) (X.uSwitchEquiv (X.uSwitchEquiv.symm x)) = (ConcreteCategory.hom f) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else ↑((if j < i then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯)) =
    j

Tactic:
split_ifs

Goal state after:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j

Tactic:
split_ifs

Goal state after:
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.pred ⋯) = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.pred ⋯) = j

case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
Fin.val_one,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + (-1) ^ 1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F.augmentedCechConerve ⟶ X
⊢ G.left ≫ X.hom.app ⦋0⦌ = F.hom ≫ WidePushout.ι (fun x ↦ F.hom) 0 ≫ G.right.app ⦋0⦌

Tactic:
rw [WidePushout.arrow_ι_assoc (fun (_ : Fin 1) => F.hom)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F.augmentedCechConerve ⟶ X
⊢ G.left ≫ X.hom.app ⦋0⦌ = (WidePushout.head fun x ↦ F.hom) ≫ G.right.app ⦋0⦌
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
⊢ X.Finite

Tactic:
obtain ⟨d, _⟩ := Y.hasDimensionLT_of_finite

Goal state after:
X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h✝ : Y.HasDimensionLT d
⊢ X.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (Y.map g.op)) ((ConcreteCategory.hom (f.app (op ⦋m⦌))) y) =
    (ConcreteCategory.hom (f.app (op ⦋n⦌))) ((ConcreteCategory.hom (X.map g.op)) y)

Tactic:
by rw [NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ ψ ≫ ψ = 0

Tactic:
· exact False.elim <| hj <| by simp_all [Nat.odd_add]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n i : ℕ
x✝² x✝¹ : Δ[n] _⦋i⦌
h : (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝² = (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝¹
x✝ : Fin ((unop (op ⦋i⦌)).len + 1)
⊢ (Hom.toOrderHom (objEquiv x✝²)) x✝ = (Hom.toOrderHom (objEquiv x✝¹)) x✝

Tactic:
apply congr_fun h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ j.succAbove ((i.castPred ⋯).succAbove k) ∈ {i, j}ᶜ

pp: case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝

pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩

Tactic:
· grind [compl_insert, mem_compl, Fin.succAbove, Fin.castPred]

Goal state after:
case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝

case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
⊢ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ = 𝟙 (mapTrifunctor F' I₁ I₂ I₃)

Tactic:
ext X₁ X₂ X₃ ⟨i₁, i₂, i₃⟩
    dsimp
    simp only [← NatTrans.comp_app, e.inv_hom_id, NatTrans.id_app]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂

Tactic:
by
  obtain rfl := c₁.next_eq' h
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
· rw [K.D₁_shape c₁₂ _ _ h₂, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂'')

Tactic:
have h₅ : ComplexShape.π c₁ c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂' := by
            rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄]

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂'')
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)

Tactic:
by
  apply (HomologicalComplex.forget _ _).map_injective
  apply GradedObject.mapMap_id

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₁'
inst✝⁵ : Category.{v_3, u_3} C₂
inst✝⁴ : Category.{v_4, u_4} C₂'
inst✝³ : Category.{v_5, u_5} D
inst✝² : Preadditive D
inst✝¹ : HasShift D ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
x✝² x✝¹ x✝ : ℤ × ℤ
⊢ (-1) ^ ((x✝².1 + x✝¹.1) * x✝.2 + x✝².1 * x✝¹.2) = (-1) ^ (x✝².1 * (x✝¹.2 + x✝.2)) * (-1) ^ (x✝¹.1 * x✝.2)

Tactic:
← zpow_add

Goal state after:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₁'
inst✝⁵ : Category.{v_3, u_3} C₂
inst✝⁴ : Category.{v_4, u_4} C₂'
inst✝³ : Category.{v_5, u_5} D
inst✝² : Preadditive D
inst✝¹ : HasShift D ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
x✝² x✝¹ x✝ : ℤ × ℤ
⊢ (-1) ^ ((x✝².1 + x✝¹.1) * x✝.2 + x✝².1 * x✝¹.2) = (-1) ^ (x✝².1 * (x✝¹.2 + x✝.2) + x✝¹.1 * x✝.2)