mathlib-initiative/mathlib-tactics huggingface dataset:
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
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
⊢ False

Tactic:
rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ False
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
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
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (a • ad) = (↑fe).1 a * (lift fe) ad

Tactic:
← inl_mul_eq_smul,

Goal state after:
R : Type u_1
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
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (inl a * ad) = (↑fe).1 a * (lift fe) ad
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) y + (g ^ l) z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k

Tactic:
hl,

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ 0 + (g ^ l) z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
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 ^ l • ((f - μ • 1) ^ l) m = 0

Tactic:
hl,

Goal state after:
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 ^ l • 0 = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
⊢ ((l₁ + l₂).choose (i, j).1 • ((f₁ - μ₁ • 1) ^ (i, j).1 * (f₂ - μ₂ • 1) ^ (i, j).2)) m = 0

Tactic:
suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
    rw [LinearMap.smul_apply, this, smul_zero]

Goal state after:
case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_3
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 = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥⊤)

Tactic:
finrank_top,

Goal state after:
case refine_3
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 = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k (V (Fin.last n).succ))
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 : ℕ
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f

Tactic:
uIcc_of_le (le_add_of_nonneg_right hc.le),

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' Icc a (a + c) = range f
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))

Tactic:
dsimp
    revert ih
    generalize htl : reduce tl1 = TL
    intro ih
    cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

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

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

Tactic:
obtain ⟨x⟩ := nonempty_fintype α
    have : NeZero (Fintype.card α) := ⟨by simp⟩
    classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (∑ i ∈ insert a✝ s✝, f i).den ∣ (insert a✝ s✝).lcm fun i ↦ (f i).den

Tactic:
Finset.sum_insert has,

Goal state after:
case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (f a✝ + ∑ x ∈ s✝, f x).den ∣ (insert a✝ s✝).lcm fun i ↦ (f i).den
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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
← mul_sum,

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
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -((algebraMap R S) p * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
z : A
⊢ ∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a

Tactic:
by
  obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq M z
  obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
  use x', y', hu
  rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
  convert! IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
  grind

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✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x =
    x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s

Tactic:
ext <;> simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + (a * star b).re + ((b * star a).re + normSq b) = normSq a + normSq b + ((a * star b).re + (b * star a).re)

Tactic:
abel

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
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : M → G
y : M
⊢ f (y + h) • g (y + h) - f y • g y =
    f (y + h) • g y - f y • g y + (f y • g (y + h) - f y • g y) +
      (f (y + h) • g (y + h) - f y • g (y + h) - (f (y + h) • g y - f y • g y))

Tactic:
abel

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

Goal state before:
pp: case e'_2
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 = shiftₗ M G h + -1

pp: case e'_3
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)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ m ∈ range (n + 1), shiftₗ M G h ^ m * (-1) ^ (n - m) * ↑(n.choose m)) f y

Tactic:
· simp only [sub_eq_add_neg]

Goal state after:
case e'_3
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)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ m ∈ range (n + 1), shiftₗ M G h ^ m * (-1) ^ (n - m) * ↑(n.choose m)) f y
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case inr.inl
m : ℕ
⊢ Δ_[1]^[m] (fun x ↦ ↑(x.choose m)) 0 = if m = m then 1 else 0

Tactic:
simp only [if_true, add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, cast_one]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by
  obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx
  exact ⟨a, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ (castAddHom A).range ↔ a ∈ zmultiples 1

Tactic:
simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i, f i ^ a i

Tactic:
by
  obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx
  exact ⟨a, by simp⟩

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
⊢ IsSplitEpi f

Tactic:
let φ : Y → X := fun y => (H y).some.1

Goal state after:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
⊢ IsSplitEpi f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ (Fork.ofι i ⋯).pt
hm : m ≫ (Fork.ofι i ⋯).ι = s.ι
⊢ m = s.ι ≫ e

Tactic:
rw [Fork.ι_ofι] at hm

Goal state after:
case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ (Fork.ofι i ⋯).pt
hm : m ≫ i = s.ι
⊢ m = s.ι ≫ e
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ p ≫ 𝟙 X = p ≫ p

Tactic:
rw [hp, comp_id]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)

Tactic:
by
  dsimp [δ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_gt H]

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
obtain rfl | hj := hj.eq_or_lt

Goal state after:
case inl
n m : ℕ
j : Fin (m + 1)
hi : n + ↑j = m
hj : ↑j ≤ ↑j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (↑j) hi)) j) = 0

case inr
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj✝ : ↑j ≤ i
hj : ↑j < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin ((rev.obj { len := n }).len + 1)
⊢ (Hom.toOrderHom (rev.map (δ i))) j = (Hom.toOrderHom (δ i.rev)) j

Tactic:
simp [δ, Fin.succAbove_rev_right, Fin.rev_rev, rev_map_apply]

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

Goal state before:
pp: Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'

Tactic:
let e := image.isoStrongEpiMono e i fac

Goal state after:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
reassoc_of% hj _ i'.succ (by lia) (by lia) (by grind),

Goal state after:
case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ σ₀Iter j ⋯ ≫ δ i'.succ ≫ σ 0 = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
hk' : j.castSucc < k
⊢ ↑(j.predAbove k) ≤ i

Tactic:
· grind [Fin.predAbove]

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

Goal state before:
pp: case succ
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
| succ n hn =>

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

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy

Tactic:
exact (N.ext_iff (N.mk x hx) (N.mk y hy)).symm

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case right
n : ℕ
i j : Fin (n + 2)
hj✝ : j ∈ {i}ᶜ
hj : ¬j = i
⊢ ∃ a, (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩

Tactic:
obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i

Goal state after:
case right.inl
n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ ∃ a, (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) a = ⟨j, hj✝⟩

case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite ((stdSimplex.obj n).obj d)

Tactic:
rw [objEquiv.finite_iff]
  infer_instance

Goal state after:
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₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
⊢ ((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
      { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (Y₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } =
    { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } ≫
      ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ

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

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂

Tactic:
apply mul_right_cancel (b := ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂))
    rw [mul_assoc]
    nth_rw 2 [mul_comm]
    rw [← mul_assoc, ComplexShape.σ_ε₁ c₂ c₁₂ h₁ i₂, mul_comm, ← mul_assoc,
      Int.units_mul_self, one_mul, mul_comm, ← mul_assoc, Int.units_mul_self, one_mul]

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₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) ≠ i₁₂'

Tactic:
intro 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₁₂
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₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ False