mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
by_cases hjk : c.Rel j k

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
⊢ φ ≫ f' = 0 ↔ φ ≫ f'' = 0

Tactic:
by_cases hjk : c.Rel j k

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
⊢ φ ≫ f' = 0 ↔ φ ≫ f'' = 0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
⊢ φ ≫ f' = 0 ↔ φ ≫ f'' = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
by_cases hjk : c.Rel j k

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
⊢ IsLimit (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)

Tactic:
by_cases hjk : c.Rel j k

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : c.Rel j k
⊢ IsLimit (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : ¬c.Rel j k
⊢ IsLimit (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d j k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
by_cases hjk : c.Rel j k

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : c.Rel j k
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d j k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d j k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv
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:
have := K.mono_homologyMap_shortComplexTruncLE_g e i' hi'

Goal state after:
ι : 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'
this : Mono (homologyMap (K.shortComplexTruncLE e).g i')
⊢ IsIso (homologyMap (K.shortComplexTruncLE e).g i')
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : QuasiIso s
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom

Tactic:
singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j =
    ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : QuasiIso s
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a))

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs✝ : IsIso (Q.map s)
hs : QuasiIso s
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
⊢ IsIso (Q.map (CochainComplex.truncLEMap s b))

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs✝ : IsIso (Q.map s)
hs : QuasiIso s
fac : f = Q.map g ≫ inv (Q.map s)
⊢ IsIso (Q.map (CochainComplex.truncLEMap s b))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁸ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁷ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁶ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁵ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝⁴ : L₂.IsLocalization W₂
X Y : C₁
inst✝³ : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst✝² : HasSmallLocalizedHom W₂ X' X'
inst✝¹ : HasSmallLocalizedHom W₂ X' Y'
inst✝ : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
⊢ (SmallHom.equiv W₂ L₂) (Φ.smallHomMap' eX eY f) =
    L₂.map eX.inv ≫ e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁) f) ≫ e.inv.app Y ≫ L₂.map eY.hom

Tactic:
simp [smallHomMap', SmallHom.equiv_comp, Φ.equiv_smallHomMap L₁ L₂ G e]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ R₂.map (homOfLE ⋯ ≫ homOfLE ⋯) = 0

Tactic:
exact hR₂

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i : ℤ
φ : Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ Q.obj L
n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
⊢ φ = 0

Tactic:
obtain ⟨K, _, π, h, g, rfl⟩ := right_fac_of_isStrictlyLE φ i

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
⊢ inv (Q.map π) ≫ Q.map g = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
⊢ IsCyclic G

Tactic:
cases nonempty_fintype G
    apply isCyclic_of_card_pow_eq_one_le
    intro n hn
    exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ (algebraMap R[X] K) f / (algebraMap R[X] K) g =
    (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g) / (algebraMap R[X] K) g

Tactic:
have hg' : algebraMap R[X] K g ≠ 0 :=
      (map_ne_zero_iff _ (IsFractionRing.injective R[X] K)).mpr (Monic.ne_zero hg)

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f / (algebraMap R[X] K) g =
    (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g) / (algebraMap R[X] K) g
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (map (Int.castRingHom R)) g = (map (Int.castRingHom R)) h → g = h

Tactic:
ext_iff,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (∀ (i j : n), ↑((map (Int.castRingHom R)) g) i j = ↑((map (Int.castRingHom R)) h) i j) → ∀ (i j : n), ↑g i j = ↑h i j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q) ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = g

Tactic:
by
  exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
⊢ C a

Tactic:
by
  -- the arguments are enough to construct a subalgebra, and a mapping into it from M
  let s : Subalgebra R (CliffordAlgebra Q) :=
    { carrier := {a | C a}
      mul_mem' := @mul
      add_mem' := @add
      algebraMap_mem' := algebraMap }
  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = Algebra.algebraMap _ _ (Q m) } :=
    ⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι,
      fun m => Subtype.ext <| ι_sq_scalar Q m⟩
  -- the mapping through the subalgebra is the identity
  have of_id : s.val.comp (lift Q of) = AlgHom.id R (CliffordAlgebra Q) := by
    ext x
    simpa [of, -LinearMap.codRestrict_apply]
      -- This `@[simp]` lemma applies to `coeSort s.subModule`, but the goal contains
      -- a plain `coeSort s`. So we remove it from the `simp` arguments, and add it to
      -- the term that `simpa` will simplify before applying.
      using LinearMap.codRestrict_apply s.toSubmodule (CliffordAlgebra.ι Q) x (h := ι)
  -- finding a proof is finding an element of the subalgebra
  rw [← AlgHom.id_apply (R := R) a, ← of_id]
  exact (lift Q of a).prop

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)

Tactic:
map_apply_ι,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((ι Q₂) (g m)) = (map (f.comp g)) ((ι Q₁) m)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((ι Q₂) (g m)) = (map (f.comp g)) ((ι Q₁) m)

Tactic:
map_apply_ι,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (ι Q₃) (f (g m)) = (map (f.comp g)) ((ι Q₁) m)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (ι Q₃) (f (g m)) = (map (f.comp g)) ((ι Q₁) m)

Tactic:
map_apply_ι,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (ι Q₃) (f (g m)) = (ι Q₃) ((f.comp g) m)
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
i j : ι
a : A i
r : R
x : A j
⊢ GradedMonoid.GMul.mul a (r • x) = (RingHom.id R) r • GradedMonoid.GMul.mul a x

Tactic:
injection (smul_comm r (GradedMonoid.mk _ a) (GradedMonoid.mk _ x)).symm

Goal state after: