mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ a = 0

Tactic:
add_eq_zero_iff_of_nonneg,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ a = 0

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ a = 0

pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
add_eq_zero_iff_of_nonneg,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
by
  rw [mul_comm]
  exact npow_mul x n m

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (P.coeff P.natDegree • Δ_[1]^[P.natDegree] fun i ↦ i ^ P.natDegree) x = P.leadingCoeff • ↑P.natDegree ! x

pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
fwdDiff_iter_eq_factorial,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (P.coeff P.natDegree • ↑P.natDegree !) x = P.leadingCoeff • ↑P.natDegree ! x

R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.inv
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y c : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
hcy : ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑c = f x
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑c⁻¹ = f x

Tactic:
| inv c hc hcy =>

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

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

Tactic:
Equiv.eq_symm_apply,

Goal state after:
X Y : FintypeCat
f : X ⟶ Y
x : X.obj
⊢ Y.uSwitchEquiv ((ConcreteCategory.hom (uSwitch.map f)) (X.uSwitchEquiv.symm x)) = (ConcreteCategory.hom f) x
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
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
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩

Goal state after:
case mpr
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
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀

Tactic:
rw [← g.op_unop]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
by_cases h' : y₁ < y₂
                · by_contra h''
                  apply not_le.mpr h'
                  convert! f.toOrderHom.monotone (le_of_not_ge h'')
                  all_goals
                    exact (ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm
                · rw [eq_of_le_of_not_lt h h']

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j)) ⟨↑k + (i + 1), ⋯⟩) = ↑⟨↑k + i, ⋯⟩

Tactic:
coe_σ,

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.predAbove ⟨↑k + (i + 1), ⋯⟩) = ↑⟨↑k + i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inl
n : ℕ
⊢ 0 = ↑((ConcreteCategory.hom (σ 0)) 0)

Tactic:
coe_σ,

Goal state after:
case inl
n : ℕ
⊢ 0 = ↑(Fin.predAbove 0 0)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: 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

Tactic:
Fin.castSucc_castPred,

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ ↑k - (i + 1) = ↑((ConcreteCategory.hom (σ 0)) ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

Tactic:
coe_σ,

Goal state after:
case neg
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ ↑k - (i + 1) = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))
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 + 2)
⊢ (opFunctor.obj X).δ i = opObjIso.hom ≫ X.δ i.rev ≫ opObjIso.inv

Tactic:
by
  simp [opObjIso, SimplicialObject.δ]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i = j

Tactic:
← Fin.succAbove_left_inj

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i.succAbove = j.succAbove
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin ((Opposite.unop y).len + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝ =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝

Tactic:
simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin ((Opposite.unop y).len + 1)
⊢ X.left.map (f ≫ (⦋0⦌.const (Opposite.unop y) j✝).op) ≫ Arrow.Hom.left G =
    X.left.map (⦋0⦌.const (Opposite.unop x) ((SimplexCategory.Hom.toOrderHom f.unop) j✝)).op ≫ Arrow.Hom.left G
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
hf : ¬IsIso f
⊢ False

Tactic:
refine hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩

Goal state after:
case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
hf : ¬IsIso f
h : n ≤ m
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X Y : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
obtain ⟨m, hm, g, y, rfl⟩ := hx

Goal state after:
X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) ((ConcreteCategory.hom (X.map g.op)) y) ∈ Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.left e.edge = nerveEquiv x

Tactic:
by
  simp only [← e.src_eq]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i.castSucc.succ = ↑1 + ↑i

Tactic:
simp; grind

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
by
  generalize hm : S.card = m
  obtain _ | m := m
  · obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero]
    rw [face_empty]
    infer_instance
  · rw [← hasDimensionLT_iff_of_iso
      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]
    exact hasDimensionLT_of_le _ (m + 1) _

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
⊢ (↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.σ i.succ =
    (stdSimplex.obj Δ).left.σ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f))

Tactic:
by
    ext φ
    apply objEquiv.injective
    apply SimplexCategory.Hom.ext
    ext j : 2
    dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex, objEquiv, Equiv.ulift,
      uliftFunctor, Function.comp_def]
    cases j using Fin.cases <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L
⊢ toHom (mk (Cocycle.equivHomShift f)) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f

Tactic:
by simp [toHom_mk]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
hq : n + 1 = m
y : Cochain K L n
property✝ : δ n m y ∈ cocycle K L m
⊢ ⟨δ n m y, property✝⟩ ∈ (AddCommGrpCat.Hom.hom s.π).ker

Tactic:
simpa only [zero_comp] using! ConcreteCategory.congr_hom s.condition y

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case e_a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
⊢ (dNext (e.f i)) h.hom =
    (K.extendXIso e ⋯).hom ≫
      ((dNext i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) ≫
        (L.extendXIso e ⋯).inv

Tactic:
by_cases hi : c.Rel i (c.next i)
      · have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
        simp [dNext_eq _ hi, dNext_eq _ hi', K.extend_d_eq _ rfl rfl]
      · rw [dNext_eq_zero _ _ hi]
        by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
        · simp [dNext_eq _ hi', extend_d_from_eq_zero _ _ _ _ _ rfl hi]
        · simp [dNext_eq_zero _ _ hi']

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

Tactic:
rw [fibration_iff, weakEquivalence_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : IsCofibrant X
⊢ Cofibration coprod.inr

Tactic:
rw [isCofibrant_iff] at hX

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : Cofibration (initial.to X)
⊢ Cofibration coprod.inr
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g

Tactic:
have := coprod.inr ≫= sq.fac_left

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : coprod.inr ≫ Q.i ≫ sq.lift = coprod.inr ≫ coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulated
⊢ P.op.trW = P.trW.op

Tactic:
ext X Y f
  exact P.trW_op_iff

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
K L : CochainComplex C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst✝¹ : K.IsStrictlyGE n₁
inst✝ : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
⊢ (mappingCone f).IsStrictlyGE n

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
K L : CochainComplex C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst✝¹ : K.IsStrictlyGE n₁
inst✝ : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero ((mappingCone f).X i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
A : Type u_3
inst✝⁴ : Category.{v_3, u_3} A
inst✝³ : Abelian A
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : HomotopyCategory.Plus C
f : F.mapHomotopyCategoryPlus.obj X✝ ⟶ F.mapHomotopyCategoryPlus.obj Y✝
⊢ F.mapHomotopyCategoryPlus.map (ObjectProperty.homMk ((F.mapHomotopyCategory (ComplexShape.up ℤ)).preimage f.hom)) = f

Tactic:
by
      ext
      exact (F.mapHomotopyCategory _).map_preimage f.hom

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
⊢ ∀ (X : C), t.plus X → ∀ (n : ℤ), t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)

Tactic:
rintro X ⟨a, _⟩ n

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a : ℤ
h✝ : t.IsGE X a
n : ℤ
⊢ t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
⊢ ∀ (X : C), t.minus X → ∀ (n : ℤ), t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)

Tactic:
rintro X ⟨a, _⟩ n

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a : ℤ
h✝ : t.IsLE X a
n : ℤ
⊢ t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h : K.IsStrictlyGE n
⊢ Qh.essImage { obj := X, property := ⋯ }

Tactic:
refine ⟨⟨(HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, ?_⟩,
      ⟨Plus.ι.preimageIso ((quotientCompQhIso C).app _ ≪≫ e.symm)⟩⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h : K.IsStrictlyGE n
⊢ HomotopyCategory.plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
φ : T.obj₂ ⟶ T'.obj₂
a✝ b : ℤ
h₀ : t.IsLE T.obj₁ a✝
h₁' : t.IsGE T'.obj₃ b
h : a✝ < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
⊢ ∃ f, f.hom₂ = φ

Tactic:
obtain ⟨c, comm₂, comm₃⟩ := complete_distinguished_triangle_morphism _ _ hT hT' a φ comm₁

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
φ : T.obj₂ ⟶ T'.obj₂
a✝ b : ℤ
h₀ : t.IsLE T.obj₁ a✝
h₁' : t.IsGE T'.obj₃ b
h : a✝ < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
c : T.obj₃ ⟶ T'.obj₃
comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂
comm₃ : T.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T'.mor₃
⊢ ∃ f, f.hom₂ = φ
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ (I K).IsStrictlyGE n

Tactic:
isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero ((I K).X i)