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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
hn : ∃ i, e.f i = i'
⊢ IsIso ((K.πTruncGE e).f i')

Tactic:
obtain ⟨i, hi⟩ := hn

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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((K.πTruncGE e).f 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
i : ι
⊢ ((single C c j).obj A).HasHomology i

Tactic:
by
  apply ShortComplex.hasHomology_of_zeros

Goal state after:
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
this : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso := e.symm }
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) G' G e'.symm
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
have : e = e' ≪≫ Functor.isoWhiskerLeft _ α := by
    ext
    simp [α, this]

Goal state after:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
e' : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso Φ.functor L₁ L₂ G'
this✝ : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := { iso := e.symm }
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) G' G e'.symm
this : e = e' ≪≫ L₁.isoWhiskerLeft α
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y
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 B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j = (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
← cancel_mono (iCycles _ _)

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 B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).iCycles j =
    ((singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv) ≫ ((single C c j).obj B).iCycles j
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Ext X Y n)

Tactic:
simp only [hasExt_iff, small_congr Ext.homEquiv]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) ↔
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)

Tactic:
rw [← cancel_mono (e₂.hom.app _)]

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y ≫ e₂.hom.app Y =
    ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)) ≫
      e₂.hom.app Y
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 ((iso adj a).hom.app X✝) ≫ (Functor.commShiftIso G a).hom.app (F.obj X✝)

Tactic:
LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_cancel a)

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✝) =
    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✝)
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
⊢ adj.CommShift A

Tactic:
let := adj.leftAdjointCommShift A
  refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩
  ext X
  dsimp
  simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
    Functor.commShiftIso_comp_hom_app] using! LeftAdjointCommShift.compatibilityUnit_iso adj a X

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X =
    CatCenter.app { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } X ≫
      CatCenter.app { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } X

Tactic:
Linear.smul_comp,

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X =
    a • 𝟙 X ≫ CatCenter.app { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } X
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ (r • 𝟙 ((L ⋙ G).obj (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
Linear.smul_comp,

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ (r • 𝟙 ((L ⋙ G).obj (L.objPreimage X)) ≫ G.map e.hom) = r • 𝟙 (G.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
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
      X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C
  have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₃ _
    (op_distinguished _ hS.singleTriangle_distinguished) n₀ n₁ (by lia)
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)
  · ext; apply singleFunctor_map_comp_hom (C := C)
  · ext; dsimp; apply preadditiveYoneda_homologySequenceδ_singleTriangle_apply

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
j : Fin 2
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Tactic:
obtain ⟨u, v, h⟩ := hab
  refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩ <;>
  · rw [Matrix.det_fin_two_of, ← h]
    ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
t : Fin 2
⊢ v t = ↑g 0 t

Tactic:
{

Goal state after:
R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
t : Fin 2
⊢ v t = ↑g 0 t
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
⊢ (if i2 = i₀ then if i1 = i₀ then 1 else diagonal fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1
      else
        if i1 = i₀ then diagonal fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1
        else
          diagonal fun i ↦
            if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
            else
              if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else if i = i₀ then (D i1)⁻¹ * (D i2)⁻¹ else (D i2)⁻¹
              else if i = i1 then D i1 else if i = i₀ then (D i1)⁻¹ else 1)
      i j =
    (if i1 = i₀ then if i2 = i₀ then 1 else diagonal fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1
      else
        if i2 = i₀ then diagonal fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1
        else
          diagonal fun i ↦
            if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
            else
              if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else if i = i₀ then (D i2)⁻¹ * (D i1)⁻¹ else (D i1)⁻¹
              else if i = i2 then D i2 else if i = i₀ then (D i2)⁻¹ else 1)
      i j

Tactic:
split_ifs <;> simp [diagonal_apply]

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : ¬i1 = i₀
⊢ (if i = j then
      if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
      else if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else (D i1)⁻¹ * (D i2)⁻¹ else if i = i1 then D i1 else 1
    else 0) =
    if i = j then
      if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
      else if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else (D i2)⁻¹ * (D i1)⁻¹ else if i = i2 then D i2 else 1
    else 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
⊢ LeftInverse ⇑(map g) ⇑(map f)

Tactic:
by
  intro x
  replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h
  rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]

Goal state after:
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
⊢ r ^ 0 ∈ A (0 • i)

Tactic:
pow_zero,

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
⊢ 1 ∈ A (0 • i)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) (a ^ 0) = (of A 0) a ^ 0

Tactic:
pow_zero,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) 1 = (of A 0) a ^ 0
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) 1 = (of A 0) a ^ 0

Tactic:
pow_zero,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) 1 = 1
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) i) b) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0

Tactic:
coe_mul_of_apply

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ (if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
suffices x * u = v * y ↔ v⁻¹ * x = y * u⁻¹ by
    dsimp only [Matrix.IsAdjointPair]
    simp only [Matrix.transpose_mul]
    simp only [← mul_assoc, P.transpose_nonsing_inv]
    convert! this using 2
    · rw [mul_assoc, mul_assoc, ← mul_assoc J]
      rfl
    · rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
      rfl

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
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
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap (p * q)) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap q) *
      Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap p)

Tactic:
Submodule.map_mul,

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
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm)
      (Submodule.map reverseOp.toLinearMap p * Submodule.map reverseOp.toLinearMap q) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap q) *
      Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap p)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_1
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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
⊢ j ≠ 0 → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j 0

Tactic:
refine Fin.cases ?_ (fun j => ?_) j

Goal state after:
case succ.inr.refine_1.refine_1
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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
⊢ 0 ≠ 0 → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) 0 0

case succ.inr.refine_1.refine_2
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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i : Fin (d + 1)
j : Fin d
⊢ j.succ ≠ 0 → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j.succ 0