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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal

Tactic:
apply le_antisymm
  · intro x hx; obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x; exact ⟨x, hx, rfl⟩
  · rintro _ ⟨x, hx, rfl⟩; exact hx

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ ↑((f.toLinearMap.restrict h) ⟨a * b, ⋯⟩) = ↑(f a • ⟨f b, ⋯⟩)

Tactic:
exact map_mul f a b

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
rcases J.toCotangent_surjective x with ⟨x', hx'⟩

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
x' : ↥J
hx' : J.toCotangent x' = x
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J)) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯).ker

Tactic:
rw [Submodule.map_le_iff_le_comap, ← LinearMap.ker_comp]
    intro x hx
    simp only [LinearMap.mem_ker, LinearMap.comp_apply, Ideal.mapCotangent_toCotangent]
    convert! map_zero I.toCotangent
    exact (Ideal.mem_inf.mp hx).1

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.next i = j

Tactic:
apply c.next_eq _ h
  rw [next]
  rw [dif_pos]
  exact Exists.choose_spec ⟨j, h⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (0 + a✝).app X✝ = a✝.app X✝

Tactic:
simp only [add_app, zero_app, zero_add]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ f x = f' x

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ this

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ x ∈ Set.range ⇑(KaehlerDifferential.D R S), f x = f' x

case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ f 0 = f' 0

case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (x y : Ω[S⁄R]),
    x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) →
      y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f y = f' y → f (x + y) = f' (x + y)

case refine_4
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (a : S), ∀ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)), f x = f' x → f (a • x) = f' (a • x)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (map R R A B).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
by
  rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
    Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
    Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
    bot_sup_eq, Submodule.map_span, ← Set.range_comp]
  convert! bot_sup_eq _
  rw [Submodule.span_eq_bot]; simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ ((prevD j) fun i j ↦ f i j ≫ g.f j) = (prevD j) f ≫ g.f j

Tactic:
dsimp [prevD]
  simp only [assoc, g.comm]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ e.f i =
    (((dNext i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
        (prevD i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
      Hom.f 0 i

Tactic:
by
    dsimp
    simp only [add_zero]
    rw [add_comm]
    refine (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans ?_
    congr
    · cases i
      · dsimp [toPrev, mkCoinductiveAux₂]
      · dsimp [toPrev]
        simp only [CochainComplex.prev_nat_succ, dite_true]
        rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
        dsimp [xPrevIso]
        rw [comp_id]
    · dsimp [fromNext]
      rw [dif_pos (by simp only [CochainComplex.next])]
      simp [xNextIso, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h✝ : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
⊢ F₂.map ((functor r).map f) = F₂.map ((functor r).map g)

Tactic:
Quotient.sound r h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h✝ : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
⊢ F₂.map ((functor r).map g) = F₂.map ((functor r).map g)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
L : C ⥤ D
⊢ ∀ {X Y : Quotient L.homRel}, Function.Injective (Quotient.lift L.homRel L ⋯).map

Tactic:
rintro ⟨_⟩ ⟨_⟩ ⟨_⟩ ⟨_⟩ h
    exact Quotient.sound _ h

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ n.negOnePow • h.hom (i + n) (j + n) = 0

Tactic:
rw [h.zero, smul_zero]

Goal state after:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ ¬(ComplexShape.up ℤ).Rel (j + n) (i + n)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g

Tactic:
by simpa using hg₁.symm

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0

Tactic:
IsIso.comp_right_eq_zero

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ T.mor₂ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h :
  -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ↔ Mono T.mor₁
⊢ T.mor₃ = 0 ↔ (CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0

Tactic:
IsIso.comp_right_eq_zero

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h :
  -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ↔ Mono T.mor₁
⊢ T.mor₃ = 0 ↔ (CategoryTheory.shiftFunctor C (-1)).map T.mor₃ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0

Tactic:
φ'.comm₂_assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ φ'.hom₂ ≫ (productTriangle T).mor₂ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles C
n : ℤ
⊢ (Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ distinguishedTriangles C

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
  exact ⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
p : ℤ
s_g : (σ (p + 1)).s ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
f_r : S.f.f (p + 1) ≫ (σ (p + 1)).r = 𝟙 (S.X₁.X (p + 1))
⊢ (S.f ≫ S.g).f (p + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (p + 1) p ⋯ = 0

Tactic:
S.zero,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
p : ℤ
s_g : (σ (p + 1)).s ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
f_r : S.f.f (p + 1) ≫ (σ (p + 1)).r = 𝟙 (S.X₁.X (p + 1))
⊢ Hom.f 0 (p + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (p + 1) p ⋯ = 0
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : Category.{v_2, u_2} D
inst✝²² : Category.{v_3, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
inst✝¹⁸ : HasZeroObject C
inst✝¹⁷ : HasZeroObject D
inst✝¹⁶ : HasZeroObject E
inst✝¹⁵ : Preadditive C
inst✝¹⁴ : Preadditive D
inst✝¹³ : Preadditive E
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁹ : Pretriangulated C
inst✝⁸ : Pretriangulated D
inst✝⁷ : Pretriangulated E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁶ : F.CommShift ℤ
inst✝⁵ : G.CommShift ℤ
inst✝⁴ : H.CommShift ℤ
inst✝³ : NatTrans.CommShift e.hom ℤ
inst✝² : G.IsTriangulated
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsTriangulated ↔ H.IsTriangulated

Tactic:
← isTriangulated_iff_of_iso e

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : Category.{v_2, u_2} D
inst✝²² : Category.{v_3, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
inst✝¹⁸ : HasZeroObject C
inst✝¹⁷ : HasZeroObject D
inst✝¹⁶ : HasZeroObject E
inst✝¹⁵ : Preadditive C
inst✝¹⁴ : Preadditive D
inst✝¹³ : Preadditive E
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁹ : Pretriangulated C
inst✝⁸ : Pretriangulated D
inst✝⁷ : Pretriangulated E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁶ : F.CommShift ℤ
inst✝⁵ : G.CommShift ℤ
inst✝⁴ : H.CommShift ℤ
inst✝³ : NatTrans.CommShift e.hom ℤ
inst✝² : G.IsTriangulated
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsTriangulated ↔ (F ⋙ G).IsTriangulated
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
h : S.f.f (n + 1) ≫ (σ (n + 1)).r = 𝟙 (S.X₁.X (n + 1))
⊢ (S.f ≫ S.g).f (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ -
      S.f.f (n + 1) ≫ (σ (n + 1)).r ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n =
    -(mappingCone.inr (homOfDegreewiseSplit S σ)).f n

Tactic:
S.zero,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
h : S.f.f (n + 1) ≫ (σ (n + 1)).r = 𝟙 (S.X₁.X (n + 1))
⊢ Hom.f 0 (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ -
      S.f.f (n + 1) ≫ (σ (n + 1)).r ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n =
    -(mappingCone.inr (homOfDegreewiseSplit S σ)).f n
Module: Mathlib.CategoryTheory.Triangulated.Functor

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
⊢ ∀ {u₁₃ : Y₁ ⟶ Y₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : Y₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂}
    (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles), Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
u₁₃

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
⊢ ∀ (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : Y₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂}
    (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles), Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ opcyclesMap (S.f ≫ S.g) i = 0

Tactic:
S.zero,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ opcyclesMap 0 i = 0
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Tactic:
rintro X
    rfl

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

Goal state before:
pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (of V ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rcases φ with ⟨φo, φm⟩

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of V ⋙q (lift { obj := φo, map := φm }).toPrefunctor).map f =
    Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := φo, map := φm }.map f))
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

Tactic:
rintro X
    rfl

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
G : Type u_5
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ (F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)

Tactic:
have hnm' : m + n = 0 := by
    rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
  simp [F.shiftIso_hom_app_comp_shiftMap f n 0 hnm' a' a, shiftIso_zero_hom_app,
    shiftFunctorCompIsoId]

Goal state after: