mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ (fst φ).f p ≫ (inl φ).v p p ⋯ + (snd φ).v p q hpq ≫ (↑(inr φ)).v q p ⋯ = 𝟙 ((mappingCocone φ).X p)

Tactic:
obtain rfl : q = p + -1 := by lia
  simp [fst, inl, snd, inr, mappingCocone,
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ hpq,
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Int.negOnePow_even 2 ⟨1, rfl⟩,
    mappingCone.id_X φ (p + -1) p (by lia)]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
hi : i = none
⊢ IsZero (X K i)

Tactic:
by
  subst hi
  exact Limits.isZero_zero _

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ c'.prev (e.f j) = e.f j

Tactic:
apply c'.prev_eq_self

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ ¬c'.Rel (c'.prev (e.f j)) (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j') = extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j')

Tactic:
extend.d_none_eq_zero' _ _ _ hj',

Goal state after:
case neg
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ 0 = extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ 0 = extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j')

Tactic:
extend.d_none_eq_zero' _ _ _ hj',

Goal state after:
case neg
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ 0 = 0 ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0

Tactic:
rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
⊢ ⋯.δ i' j' hij' = 0

Tactic:
by
  by_cases hj : ∃ j, e.f j = j'
  · obtain ⟨j, rfl⟩ := hj
    rw [← cancel_mono (homologyMap (K.ιTruncLE e) (e.f j)), zero_comp]
    exact (K.shortComplexTruncLE_shortExact e).δ_comp i' _ hij'
  · apply ((K.truncLE e).exactAt_of_isSupported e j'
      (by simpa using hj)).isZero_homology.eq_of_tgt

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsIso (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
by
  have := K.mono_homologyMap_shortComplexTruncLE_g e i' hi'
  apply isIso_of_mono_of_epi

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ QuasiIso (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i

Tactic:
rw [HomologicalComplex.quasiIso_truncLEMap_iff]
  constructor
  · intro h i hi
    obtain ⟨k, rfl⟩ := Int.le.dest hi
    exact h k _ (by dsimp; lia)
  · rintro h i i' rfl
    exact h _ (by dsimp; lia)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁

Tactic:
apply HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ ∀
    (a_1 b_1 :
      (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))),
    a_1 = b_1

Tactic:
intro x

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ ∀
    (b_1 :
      (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
        (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))),
    x = b_1
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
        𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h

Tactic:
erw [comp_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) = Q.map f.τ₃ ≫ (triangleOfSES h₂).mor₃

Tactic:
by
    dsimp [triangleOfSES, triangleOfSESδ]
    rw [assoc, assoc, IsIso.inv_comp_eq, ← Functor.map_comp_assoc,
      ← CochainComplex.mappingCone.map_descShortComplex,
      Functor.map_comp_assoc, IsIso.hom_inv_id_assoc,
      ← Functor.commShiftIso_hom_naturality,
      ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]
    congr 2
    exact (CochainComplex.mappingCone.triangleMap S₁.f S₂.f f.τ₁ f.τ₂ f.comm₁₂.symm).comm₃

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ ((Ext.mk₀ S.g).comp hS.extClass comp_extClass_assoc._proof_1_1).comp γ ⋯ = 0

Tactic:
comp_extClass,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ Ext.comp 0 γ ⋯ = 0
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ =
    (shiftFunctorZero C B).inv.app X ≫ eqToHom ⋯ ≫ 𝟙 ((shiftFunctor (PullbackShift C φ) 0).obj X)

Tactic:
erw [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' (OppositeShift C ℤ) b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)

Tactic:
rw [oppositeShiftFunctorAdd'_hom_app]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op

Tactic:
shiftFunctorCompIsoId_add'_hom_app _ _ _ _ _ _
    (neg_add_cancel m) (neg_add_cancel n) (neg_add_cancel p) h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)) ≫
        (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
          (shiftFunctor C n).map
              ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
            (shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ a + b = 0

Tactic:
eq_neg_of_add_eq_zero_left h,

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ a + -a = 0
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫
      G.map
          (F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
            F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) ⋯).inv.app (F.obj X✝)))) ≫
              F.map
                  ((shiftFunctor C a).map ((Functor.commShiftIso G (-a)).hom.app ((shiftFunctor D a).obj (F.obj X✝)))) ≫
                F.map ((shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝)))) ≫
                  adj.counit.app ((shiftFunctor D a).obj (F.obj X✝))) ≫
        (Functor.commShiftIso G a).hom.app (F.obj X✝)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.map_shiftFunctorCompIsoId_inv_app,
    Functor.map_comp, assoc, unit_naturality_assoc, right_triangle_components_assoc]

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctor C a).map ((shiftFunctorCompIsoId C a (-a) ⋯).inv.app (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((Functor.commShiftIso G a).inv.app (F.obj X✝))) ≫
          (shiftFunctor C a).map ((Functor.commShiftIso G (-a)).inv.app ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (shiftFunctor C a).map ((Functor.commShiftIso G (-a)).hom.app ((shiftFunctor D a).obj (F.obj X✝))) ≫
              (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
                (Functor.commShiftIso G a).hom.app (F.obj X✝)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ ∀ x ∈ ((mk₀ f).postcomp L ⋯).ker, x = 0

Tactic:
intro x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
x : Ext L M 0
⊢ x ∈ ((mk₀ f).postcomp L ⋯).ker → x = 0
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
x : relations.R →₀ A
⊢ solution.π (relations.map x) = 0

Tactic:
by
  change solution.π.comp relations.map x = 0
  rw [π_comp_map, LinearMap.zero_apply]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.fromQuotient.ker ≤ ⊥

Tactic:
intro x

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.Quotient
⊢ x ∈ solution.fromQuotient.ker → x ∈ ⊥
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : Fintype ι
⊢ ∑ i, e.toMatrix v i j • e i = v j

Tactic:
simp_rw [e.toMatrix_apply, e.sum_repr]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ (b.repr (x * w j✝)) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Tactic:
← Algebra.leftMulMatrix_mulVec_repr

Goal state after:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ ((Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr (w j✝))) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = f

Tactic:
toLin_mul b' c' c,

Goal state after:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ (toLin c' c) (c.toMatrix ⇑c') ∘ₗ (toLin b' c') ((toMatrix b' c') f) = f
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1

Tactic:
rw [← hxy]

Goal state after:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ∀ x ∈ ((mk₀ g).precomp L ⋯).ker, x = 0

Tactic:
intro x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
x : Ext N L 0
⊢ x ∈ ((mk₀ g).precomp L ⋯).ker → x = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ nthRoots k 1
⊢ ↑⟨x, hx⟩ * ↑⟨x, hx⟩ ^ (k - 1) = 1

Tactic:
mem_nthRoots <| NeZero.pos k

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ * ↑⟨x, hx✝⟩ ^ (k - 1) = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ nthRoots k 1
⊢ ↑⟨x, hx⟩ ^ (k - 1) * ↑⟨x, hx⟩ = 1

Tactic:
mem_nthRoots <| NeZero.pos k

Goal state after:
case refine_2
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ ^ (k - 1) * ↑⟨x, hx✝⟩ = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_3
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ nthRoots k 1
⊢ { val := ↑⟨x, hx⟩, inv := ↑⟨x, hx⟩ ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R

Tactic:
mem_nthRoots <| NeZero.pos k

Goal state after:
case refine_3
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ { val := ↑⟨x, hx✝⟩, inv := ↑⟨x, hx✝⟩ ^ (k - 1), val_inv := ⋯, inv_val := ⋯ } ∈ rootsOfUnity k R