mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
L : C ⥤ D
W✝ : MorphismProperty C
inst✝ : L.IsLocalization W✝
W : MorphismProperty Cᵒᵖ
h : W.HasRightCalculusOfFractions
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)

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
L : C ⥤ D
W✝ : MorphismProperty C
inst✝ : L.IsLocalization W✝
W : MorphismProperty Cᵒᵖ
h : W.HasRightCalculusOfFractions
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
Y' : Cᵒᵖ
t : Y' ⟶ Opposite.op Y
ht : W t
fac : t ≫ f₁.op = t ≫ f₂.op
⊢ ∃ Y' t, ∃ (_ : W.unop t), f₁ ≫ t = f₂ ≫ t
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.Nonempty
inst✝ : Q.Nonempty
⊢ (P.extensionProduct Q).Nonempty

Tactic:
obtain ⟨Y, f, g, hT⟩ := distinguished_cocone_triangle₂ (0 : Q.arbitrary ⟶ P.arbitrary⟦(1 : ℤ)⟧)

Goal state after:
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.Nonempty
inst✝ : Q.Nonempty
Y : C
f : P.arbitrary ⟶ Y
g : Y ⟶ Q.arbitrary
hT : Triangle.mk f g 0 ∈ distinguishedTriangles
⊢ (P.extensionProduct Q).Nonempty
Module: Mathlib.CategoryTheory.Localization.Composition

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ W₂ ≤ W₃.map L₁

Tactic:
rw [hW₂₃]

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ W✝ : HomologicalComplex C c
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h : RetractArrow f✝ g✝
hg : quasiIso C c g✝
⊢ quasiIso C c f✝

Tactic:
rw [mem_quasiIso_iff] at hg ⊢

Goal state after:
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ W✝ : HomologicalComplex C c
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h : RetractArrow f✝ g✝
hg : QuasiIso g✝
⊢ QuasiIso f✝
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
hf : P.trW f
⊢ Q.trW f

Tactic:
trW_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
hf : ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), Q Z
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
a : ℤ
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C 0 a a ⋯).hom.app K =
    ShortComplex.homologyMap
        ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (HomologicalComplex C (up ℤ)) ℤ).hom.app K)) ≫
      𝟙 (K.homology a)

Tactic:
simp only [ShiftSequence.shiftIso_hom_app, comp_id,
      shiftShortComplexFunctorIso_zero_add_hom_app]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : P Z
e : Triangle.mk T.mor₁ g h ≅ T
h✝ :
  e.hom.hom₁ = Arrow.Hom.left (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom ∧
    e.hom.hom₂ = Arrow.Hom.right (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom
⊢ P T.obj₃

Tactic:
exact P.prop_of_iso (Triangle.π₃.mapIso e) mem

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

Goal state before:
pp: C : Type u_1
inst✝¹⁶ : Category.{v_1, u_1} C
inst✝¹⁵ : HasZeroObject C
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : Pretriangulated C
D : Type u_2
inst✝¹⁰ : Category.{v_2, u_2} D
inst✝⁹ : Preadditive D
inst✝⁸ : HasZeroObject D
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated D
P : ObjectProperty C
F : D ⥤ C
inst✝⁴ : F.CommShift ℤ
inst✝³ : F.IsTriangulated
inst✝² : P.IsClosedUnderIsomorphisms
E : Type u_4
inst✝¹ : Category.{u_5, u_4} E
L : C ⥤ E
inst✝ : L.IsLocalization P.trW
X Y : D
f : X ⟶ Y
hf : (P.inverseImage F).trW f
⊢ P.trW (F.map f)

Tactic:
by simpa only [inverseImage_trW_iff] using hf

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ (∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))) → T ∈ distinguishedTriangles

Tactic:
rintro ⟨X, Y, f, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
X Y : CochainComplex C ℤ
f : X ⟶ Y
e : T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)
⊢ T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt ((opFunctor V c).map φ.op) i

Tactic:
quasiIsoAt_opFunctor_map_iff

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).mapTriangle.map β).hom₂ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (mappingCone.triangle u₂₃)).mor₂ =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₂

Tactic:
by dsimp [β]; simp

Goal state after:
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'
hi : ¬∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
have hi' := e.r_eq_none i' (fun i'' hi'' => hi ⟨i'', hi''⟩)
      dsimp [extend]
      rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi',
        comp_zero, zero_comp]

Goal state after:
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
hjk : c.Rel j k
e : parallelPair ((K.truncGE' e✝).d j k) 0 ≅ parallelPair (K.fromOpcycles j' (e✝.f k)) 0 :=
  parallelPair.ext (K.truncGE'XIsoOpcycles e✝ hj' hj) (K.truncGE'XIso e✝ ⋯ ⋯) ⋯ ⋯
⊢ (Iso.refl (KernelFork.ofι (K.homologyι j') ⋯).pt).hom ≫
      Fork.ι
        ((Cone.postcompose e.hom).obj (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e✝ hj' hj).inv) ⋯)) =
    Fork.ι (KernelFork.ofι (K.homologyι j') ⋯)

Tactic:
by simp [e, Fork.ι]

Goal state after:
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ h.ι ≫
      (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p ⋯) h.hp).desc
        (CokernelCofork.ofπ ((K.extend e).sc' i' j' k').g ⋯) =
    0

Tactic:
by
    dsimp
    rw [← d_comp_desc_eq_zero_iff K e hj' hi hi' hk hk' _ h.hp]
    exact h.wι

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

Goal state before:
pp: case left
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Injective (fromSum e₁ e₂)

Tactic:
rintro (i₁ | i₂) (j₁ | j₂) h
    · obtain rfl := e₁.injective_f h
      rfl
    · exact (ac.disjoint _ _ h).elim
    · exact (ac.disjoint _ _ h.symm).elim
    · obtain rfl := e₂.injective_f h
      rfl

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 : CochainComplex C ℤ
inst✝¹ : HasZeroObject C
inst✝ : ∀ (i : ℤ), HasHomology K i
n q : ℤ
hq : q ≤ n
⊢ QuasiIsoAt (K.ιTruncLE n) q

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hq
  exact HomologicalComplex.quasiIsoAt_ιTruncLE (j := k) _ _ (by simp)

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✝¹ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyLE n'

Tactic:
rw [isStrictlyLE_iff]
  intro i hi
  exact IsZero.of_iso (K.isZero_of_isStrictlyLE n _ (by lia)) (K.shiftFunctorObjXIso a i _ rfl)

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (Y.isZero_of_isStrictlyGE b i (by lia)).eq_of_tgt

Goal state after:
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₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
    (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]

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₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

Tactic:
mem_rootsOfUnity

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: 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✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ↑⟨(Units.map ↑σ) ↑1, ⋯⟩ = ↑1

Tactic:
simp only [OneMemClass.coe_one, map_one]

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

Goal state before:
pp: case inr.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B

Tactic:
· suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this
    simpa only [coe_mul, ← hr] using! (scalar_commute (n := n) r (Commute.all r) B).symm

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Tactic:
have := Matrix.adjugate_fin_two A.1

Goal state after:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
simp_rw [eq_inv_of_mul_eq_one_right had, hg]

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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ g ((algebraMap R (CliffordAlgebra Q)) (Q m)) = (algebraMap R A) (Q m)

Tactic:
AlgHom.commutes

Goal state after:
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
m : M
⊢ (algebraMap R A) (Q m) = (algebraMap R A) (Q m)
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)

Tactic:
rw [pow_succ', succ_nsmul']

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c'

Tactic:
rw [commutatorElement_def, diag2_inv a⁻¹ (inv_ne_zero ha),
      SpecialLinearGroup.transvection_inv one_ne_zero b]

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c'
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : mulLeft₃ = mulRight₃
x y z : R
⊢ x * y * z = x * (y * z)

Tactic:
rw [← mulLeft₃_apply, ← mulRight₃_apply, h]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
hB₁ : B ≠ 0
hB₂ : IsSymm B
⊢ ∃ x, (B x) x ≠ 0

Tactic:
lift B to QuadraticForm R M using hB₂ with Q
  obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁
  exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

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

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
n : ZMod 2
⊢ ⨆ i, Submodule.map reverse ((ι Q).range ^ ↑i) = ⨆ j, (ι Q).range ^ ↑j

Tactic:
submodule_map_pow_reverse,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ ⨆ i, Submodule.map reverse (ι Q).range ^ ↑i = ⨆ j, (ι Q).range ^ ↑j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
m : M
⊢ ((foldl Q f hf) n) ((ι Q) m) = (f m) n

Tactic:
← foldr_reverse,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
m : M
⊢ ((foldr Q f hf) n) (reverse ((ι Q) m)) = (f m) n
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y z : V
hz : z ∈ K ∙ x
⊢ (B z) (y + (-(B x) y / (B x) x) • x) = 0

Tactic:
obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
c : K
hz : c • x ∈ K ∙ x
⊢ (B (c • x)) (y + (-(B x) y / (B x) x) • x) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
r : R
⊢ ((foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n

Tactic:
← foldr_reverse,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
r : R
⊢ ((foldr Q f hf) n) (reverse ((algebraMap R (CliffordAlgebra Q)) r)) = r • n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldl Q f hf) n) 1 = n

Tactic:
← foldr_reverse,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (reverse 1) = n