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

Goal state before:
pp: case h.right.inl
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).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₂ - μ₂ • 1) ^ j * (f₁ - μ₁ • 1) ^ i) m = 0

Tactic:
Module.End.mul_apply,

Goal state after:
case h.right.inl
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).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₂ - μ₂ • 1) ^ j) (((f₁ - μ₁ • 1) ^ i) m) = 0
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: 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, (-1) ^ ↑i * ↑(finrank k (V i)) = 0

Tactic:
simp_rw [← smul_eq_mul]

Goal state after:
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 = ⊤
⊢ ∑ x, (-1) ^ ↑x • ↑(finrank k (V x)) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right.inr
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).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
Module.End.mul_apply,

Goal state after:
case h.right.inr
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).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i) (((f₂ - μ₂ • 1) ^ j) m) = 0
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
b✝ c✝ : List (α × Bool)
a✝ : Relation.ReflTransGen Red.Step (reduce L₁) b✝
H1 : Red.Step b✝ c✝
H2 : reduce L₁ = b✝
⊢ reduce L₁ = c✝

Tactic:
obtain ⟨L4, L5, x, b⟩ := H1
    exact reduce.not H2

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.toWord = invRev x.toWord

Tactic:
by
  rcases x with ⟨L⟩
  rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord <+ x.toWord ++ y.toWord

Tactic:
refine Red.sublist ?_
  have : x * y = FreeGroup.mk (x.toWord ++ y.toWord) := by
    rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
  rw [this]
  exact FreeGroup.reduce.red

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

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty (CommRing α)

Tactic:
classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩

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

Goal state before:
pp: case pos
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
⊢ IsUnit g ∨ IsUnit h

pp: case neg
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
⊢ IsUnit g ∨ IsUnit h

Tactic:
· left; exact hm0 hm

Goal state after:
case neg
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
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a * star a = ↑(a * star a).re

Tactic:
rw [← star_comm_self']

Goal state after:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a * a = ↑(star a * a).re
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
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) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y

Tactic:
congr 1 with k

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

Goal state before:
pp: case e'_3.e_f
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 : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * ((-1) ^ (n - k) * ↑(n.choose k))) f y

Tactic:
Module.End.mul_apply,

Goal state after:
case e'_3.e_f
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 : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k) (((-1) ^ (n - k) * ↑(n.choose k)) f) y
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.one
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑1 = f x

Tactic:
exact ⟨1, by simp, 1, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0 = 0

Tactic:
← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ ((kernelSubobject (X.δ i.succ.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0 =
    0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
x : ↑X.1
⊢ x ∈ ⊤ ∧ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

Tactic:
by tauto

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

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
e : X ⟶ I := ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom f) x, ⋯⟩, monotone' := ⋯ }
⊢ Monotone fun y ↦ ↑y

Tactic:
by tauto

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Monotone fun x ↦ i

Tactic:
by tauto

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 j : Fin (n + 2)
H : i ≤ j
⊢ X.δ j.succ ≫ X.δ i = X.δ i.castSucc ≫ X.δ j

Tactic:
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 : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((sk n).obj X) ((skAdj n).unit.app ((truncation n).obj X))

Tactic:
dsimp [sk, skAdj]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    (((SimplexCategory.Truncated.inclusion n).op.lanAdjunction C).unit.app ((truncation n).obj X))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
this : Y.σ 0 ≫ Y.δ (Fin.castSucc 0) = 𝟙 (Y _⦋n⦌)
⊢ (X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0 = f.app (op ⦋n⦌)

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
this : Y.σ 0 ≫ Y.δ 0 = 𝟙 (Y _⦋n⦌)
⊢ (X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0 = f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
this : Y.σ (Fin.last n) ≫ Y.δ (Fin.last n).succ = 𝟙 (Y _⦋n⦌)
⊢ (X.σ (Fin.last n) ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌)

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
this : Y.σ (Fin.last n) ≫ Y.δ (Fin.last (n + 1)) = 𝟙 (Y _⦋n⦌)
⊢ (X.σ (Fin.last n) ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Op

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ (opFunctor.obj X).σ i = opObjIso.hom ≫ X.σ i.rev ≫ opObjIso.inv

Tactic:
by
  simp [opObjIso, SimplicialObject.σ]

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

Goal state before:
pp: case mp
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
h : { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x }
⊢ IsIso f

Tactic:
obtain rfl := S.dim_eq_of_mk_eq h

Goal state after:
case mp
X : SSet
m : ℕ
x : X _⦋m⦌
f : ⦋m⦌ ⟶ ⦋m⦌
inst✝ : Mono f
h : { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := m, simplex := x }
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝¹ : SimplexCategoryᵒᵖ
x✝ : ⊥.toSSet.obj x✝¹
val✝ : X.obj x✝¹
h : val✝ ∈ ⊥.obj x✝¹
⊢ Y.obj x✝¹

Tactic:
by tauto

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

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

Tactic:
by
  induction n with
  | zero =>
      exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
  | succ n hn =>
      by_cases hx : x ∈ X.nonDegenerate (n + 1)
      · exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
      · simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
        obtain ⟨i, y, rfl⟩ := hx
        obtain ⟨m, f, hf, z, rfl⟩ := hn y
        exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩

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

Goal state before:
pp: X : SSet
x y : X.N
⊢ (∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) →
    ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
by tauto

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
          ((ConcreteCategory.hom (SimplicialObject.δ (nerve X) i.castSucc)) s)).obj
      j =
    s.obj j

Tactic:
nerve.σ_obj,

Goal state after:
case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
⊢ ((ConcreteCategory.hom (SimplicialObject.δ (nerve X) i.castSucc)) s).obj (i.predAbove j) = s.obj j
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ Mono (objEquiv s)

Tactic:
rw [mem_nonDegenerate_iff_strictMono,
    SimplexCategory.mono_iff_injective]

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ⇑s ↔ Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this✝ : Mono (objEquiv x)
this : (unop (op ⦋i⦌)).len ≤ ⦋n⦌.len
⊢ False

Tactic:
dsimp at this

Goal state after:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this✝ : Mono (objEquiv x)
this : i ≤ n
⊢ False
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')),

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ = 0

Tactic:
rw [K.shape _ _ h, zero_f]

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₁₂ (c₁.next i₁, 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₁₂ (c₁.next i₁, i₂) = i₁₂'
⊢ False
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ : I₁
i₂' : I₂
j j' : J
h : c₁.π c₂ c (i₁, i₂') = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂' j h ≫ hom₂ f₁ h₂ F c j j' =
    c₁.ε₂ c₂ c (i₁, c₂.prev i₂') •
      (F.map (f₁.f i₁)).app (K₂.X i₂') ≫
        (F.obj (L₁.X i₁)).map (h₂.hom i₂' (c₂.prev i₂')) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂') j'

Tactic:
simp [hom₂]

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ ((prevD (-n)) h.hom).op = (dNext n) fun p q ↦ (h.hom (-q) (-p)).op

Tactic:
rw [prevD_eq _ (j' := - (n + 1)) (by simp)]
      symm
      exact dNext_eq _ (i' := n + 1) (by simp)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this :
  ((opEquivalence C).functor.map f.op).f n =
    (dNext n) h.hom + (prevD n) h.hom + ((opEquivalence C).functor.map g.op).f n
⊢ (f.f (-n)).op =
    ((((dNext (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
          (prevD (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
        g.f (-n)).op

Tactic:
dsimp at this

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (f.f (-n)).op =
    ((((dNext (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
          (prevD (-n)) fun p q ↦
            (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) +
        g.f (-n)).op
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
intro y₁ y₂ h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₁) =
    SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₂)