mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
⊢ MonoidalCategoryStruct.whiskerRight (h.add { as := m₁ }.as { as := m₂ }.as).symm.hom
        ((Discrete.functor h.F).obj { as := m₃ }) ≫
      (h.add (MonoidalCategoryStruct.tensorObj { as := m₁ } { as := m₂ }).as { as := m₃ }.as).symm.hom ≫
        (Discrete.functor h.F).map (MonoidalCategoryStruct.associator { as := m₁ } { as := m₂ } { as := m₃ }).hom =
    (MonoidalCategoryStruct.associator ((Discrete.functor h.F).obj { as := m₁ })
          ((Discrete.functor h.F).obj { as := m₂ }) ((Discrete.functor h.F).obj { as := m₃ })).hom ≫
      MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := m₁ })
          (h.add { as := m₂ }.as { as := m₃ }.as).symm.hom ≫
        (h.add { as := m₁ }.as (MonoidalCategoryStruct.tensorObj { as := m₂ } { as := m₃ }).as).symm.hom

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (MonoidalCategoryStruct.whiskerRight (h.add { as := m₁ }.as { as := m₂ }.as).symm.hom
            ((Discrete.functor h.F).obj { as := m₃ }) ≫
          (h.add (MonoidalCategoryStruct.tensorObj { as := m₁ } { as := m₂ }).as { as := m₃ }.as).symm.hom ≫
            (Discrete.functor h.F).map
              (MonoidalCategoryStruct.associator { as := m₁ } { as := m₂ } { as := m₃ }).hom).app
      X =
    ((MonoidalCategoryStruct.associator ((Discrete.functor h.F).obj { as := m₁ })
              ((Discrete.functor h.F).obj { as := m₂ }) ((Discrete.functor h.F).obj { as := m₃ })).hom ≫
          MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := m₁ })
              (h.add { as := m₂ }.as { as := m₃ }.as).symm.hom ≫
            (h.add { as := m₁ }.as (MonoidalCategoryStruct.tensorObj { as := m₂ } { as := m₃ }).as).symm.hom).app
      X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
⊢ (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj { as := n })).hom =
    MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj { as := n }) ≫
      (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as { as := n }.as).symm.hom ≫
        (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor { as := n }).hom

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj { as := n })).hom.app X =
    (MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj { as := n }) ≫
          (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as { as := n }.as).symm.hom ≫
            (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor { as := n }).hom).app
      X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
⊢ (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj { as := n })).hom =
    MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := n }) h.zero.symm.hom ≫
      (h.add { as := n }.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
        (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor { as := n }).hom

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj { as := n })).hom.app X =
    (MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := n }) h.zero.symm.hom ≫
          (h.add { as := n }.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
            (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor { as := n }).hom).app
      X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ shiftFunctorAdd' C 0 a a ⋯ =
    (shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).hom.app X =
    ((shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)).hom.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
              (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app
      X =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)).hom.app
      X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd C a₂ a₃)

Tactic:
ext X

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
            isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
              (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app
      X =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd C a₂ a₃)).hom.app
      X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f

Tactic:
Iso.app_hom

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctor C n).map ((shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          (((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          (((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
                (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
m : ℕ
⊢ (P.mkHomAux Q zero one one_zero_comm succ (m + 1)).fst ≫ Q.d (m + 1) m =
    P.d (m + 1) m ≫ (P.mkHomAux Q zero one one_zero_comm succ m).fst

Tactic:
exact (mkHomAux P Q zero one one_zero_comm succ m).2.2

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map
            ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ PreservesLimitsOfShape J (single C c i ⋙ eval C c j)

pp: case neg
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesLimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
· subst h
      exact preservesLimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Goal state after:
case neg
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesLimitsOfShape J (single C c i ⋙ eval C c j)
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
| kerTotal R S

Tactic:
rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
| (kerTotal R S).mkQ.ker
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.inl.inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

Tactic:
simp [LinearMap.mem_ker]

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

Goal state before:
pp: case a.inl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

Tactic:
simp [LinearMap.mem_ker]

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

Goal state before:
pp: case a.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
⊢ (fun x ↦ single ((algebraMap R S) x) 1) x ∈ ↑(linearCombination S ⇑(D R S)).ker

Tactic:
simp [LinearMap.mem_ker]

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
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
          (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
              Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
            Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.restrictScalars A
      (Submodule.span B
        (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
            Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
          Set.range fun x ↦ single ((algebraMap S B) x) 1))

Tactic:
Submodule.restrictScalars_span _ _ h

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
          (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
              Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
            Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A
      (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
          Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
        Set.range fun x ↦ single ((algebraMap S B) x) 1)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j

Tactic:
apply ext_to_X' _ _ hj

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (φ.f j ≫ inrX φ j) ≫ sndX φ j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
apply ext_to_X' _ _ hj

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (inrX φ i ≫ d φ i j) ≫ sndX φ j = (G.d i j ≫ inrX φ j) ≫ sndX φ j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
⊢ (single 0 n).v p' q' hpq' = v 0 p' q' hpq'

Tactic:
by_cases hq : q' = q

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
hq : q' = q
⊢ (single 0 n).v p' q' hpq' = v 0 p' q' hpq'

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n p' q' : ℤ
hpq' : p' + n = q'
hq : ¬q' = q
⊢ (single 0 n).v p' q' hpq' = v 0 p' q' hpq'
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝² : P ⟶ Q
a✝¹ : P.as ⟶ Q.as
b✝ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝ =
    Quot.mk (HomRel.CompClosure r) a✝ + Quot.mk (HomRel.CompClosure r) a✝¹

Tactic:
exact congr_arg (functor r).map (add_comm _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
⊢ ∀ (P Q R : Quotient r) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
rintro _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩
    exact congr_arg (functor r).map (by apply Preadditive.comp_add)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ (functor r).whiskerLeft (LiftCommShift.iso F r hF 0).hom =
    (functor r).whiskerLeft (Functor.CommShift.isoZero (lift r F hF) A).hom

Tactic:
ext X

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ ((functor r).whiskerLeft (LiftCommShift.iso F r hF 0).hom).app X =
    ((functor r).whiskerLeft (Functor.CommShift.isoZero (lift r F hF) A).hom).app X
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
⊢ ((whiskeringLeft C D D).obj F).map
      ((Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)) =
    ((whiskeringLeft C D D).obj F).map
      (eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom)

Tactic:
ext X

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
⊢ (((whiskeringLeft C D D).obj F).map
          ((Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃))).app
      X =
    (((whiskeringLeft C D D).obj F).map
          (eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom)).app
      X