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

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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv ≫ (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
by
  have : ((K.restriction e).sc' i j k).HasHomology := by subst hi hk; assumption
  have : (K.sc' i' j' k').HasHomology := by subst hi'' hk''; assumption
  dsimp [restrictionHomologyIso, homologyIsoSc']
  rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp, assoc,
    ← cancel_epi (K.sc j').homologyπ]
  apply (ShortComplex.π_homologyMap_ι _).trans
  dsimp
  rw [comp_id, id_comp]
  refine ((ShortComplex.homology_π_ι_assoc _ _).trans ?_).symm
  congr 1
  apply pOpcycles_restrictionOpcyclesIso_inv

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_5
i j k : ι
hij : i = j
hjk : j = k
x : X i
⊢ (aux X j k hjk) ((aux X i j hij) x) = (aux X i k ⋯) x

Tactic:
subst hij hjk

Goal state after:
ι : Type u_1
X : ι → Type u_5
i : ι
x : X i
⊢ (aux X i i ⋯) ((aux X i i ⋯) x) = (aux X i i ⋯) x
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)

Tactic:
exact K.isZero_of_isStrictlyGE n i hi

Goal state after:
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
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃

Tactic:
by
  apply comp_assoc
  lia

Goal state after:
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
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂

Tactic:
by
  apply comp_assoc
  lia

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
A : C
i : ι
γ : A ⟶ K.homology i
j : ι
hj : c.next i = j
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ K.d i j = 0), π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i

Tactic:
by
  subst hj
  exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₁ ≫ (e.app S.X₂).hom = (e.app S.X₁).hom ≫ (triangleOfSES ⋯).mor₁

Tactic:
cat_disch

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₂ ≫ (e.app S.X₃).hom = (e.app S.X₂).hom ≫ (triangleOfSES ⋯).mor₂

Tactic:
cat_disch

Goal state after:
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
⊢ HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Ext X Y n)

Tactic:
by
  let := HasDerivedCategory.standard C
  simp only [hasExt_iff, small_congr Ext.homEquiv]
  constructor
  · intro h X Y n
    exact h X Y n (by simp)
  · intro h X Y n hn
    lift n to ℕ using hn
    exact h X Y n

Goal state after:
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 φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝¹ x✝ : A
⊢ isoWhiskerRight (pullbackShiftIso C φ (x✝¹ + x✝) (φ (x✝¹ + x✝)) ⋯) F ≪≫
      commShiftIso F (φ (x✝¹ + x✝)) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ (x✝¹ + x✝) (φ (x✝¹ + x✝)) ⋯).symm =
    CommShift.isoAdd
      (isoWhiskerRight (pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯) F ≪≫
        commShiftIso F (φ x✝¹) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).symm)
      (isoWhiskerRight (pullbackShiftIso C φ x✝ (φ x✝) ⋯) F ≪≫
        commShiftIso F (φ x✝) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝ (φ x✝) ⋯).symm)

Tactic:
ext
    simp only [PullbackShift.functor, comp_obj, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, NatTrans.comp_app, whiskerRight_app, whiskerLeft_app,
      CommShift.isoAdd_hom_app, map_comp, assoc]
    rw [F.commShiftIso_add' (φ.map_add _ _).symm,
      ← shiftFunctorAdd'_eq_shiftFunctorAdd, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
      pullbackShiftFunctorAdd'_hom_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl,
      pullbackShiftFunctorAdd'_inv_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl]
    simp only [CommShift.isoAdd'_hom_app, assoc, map_comp, NatTrans.naturality_assoc,
      Iso.inv_hom_id_app_assoc]
    slice_rhs 9 10 => rw [← map_comp, Iso.inv_hom_id_app, map_id]
    simp only [comp_obj, id_comp]
    rw [← Functor.comp_map F (shiftFunctor D _), ← (F.commShiftIso _).hom.naturality_assoc]
    slice_rhs 4 5 => rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]
    slice_rhs 3 4 => rw [← map_comp, Iso.inv_hom_id_app, map_id]
    simp only [comp_obj, id_comp, comp_map, assoc]
    slice_rhs 3 4 => rw [← map_comp, ← map_comp, Iso.inv_hom_id_app, map_id, map_id]
    rw [id_comp, assoc, assoc]
    rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map (φ.hom₃ ≫ T₂.mor₃).unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁

Tactic:
← φ.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map (T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
f : T₁ ⟶ T₂
⊢ ((𝟭 (Triangle C)ᵒᵖ).map f ≫
        ((Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).isoMk
              (Opposite.unop T₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom).unop =
    (((Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).isoMk
              (Opposite.unop T₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom ≫
        (functor C ⋙ inverse C).map f).unop

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
⊢ ∀ {X Y : Triangle Cᵒᵖ} (f : X ⟶ Y),
    (inverse C ⋙ functor C).map f ≫
        (((inverse C ⋙ functor C).obj Y).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj Y)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₁) (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₂)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((inverse C ⋙ functor C).obj X).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj X) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₁)
            (Iso.refl ((inverse C ⋙ functor C).obj X).obj₂) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (𝟭 (Triangle Cᵒᵖ)).map f

Tactic:
cat_disch

Goal state after:
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 φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F✝ : C ⥤ D
inst✝ : F✝.CommShift B
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift C φ
⊢ (functor φ F).map
        (((NatTrans.PullbackShift.natIsoId C φ).hom ≫
              natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
          x✝) ≫
      ((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
            natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
        ((functor φ F).obj x✝) =
    𝟙 ((functor φ F).obj x✝)

Tactic:
by
    simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

Goal state after:
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 φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F✝ : C ⥤ D
inst✝ : F✝.CommShift B
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift D φ
⊢ ((NatTrans.PullbackShift.natIsoId C φ).hom ≫ natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
        ((functor φ G).obj x✝) ≫
      (functor φ G).map
        (((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
              natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
          x✝) =
    𝟙 ((functor φ G).obj x✝)

Tactic:
by
    simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

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
⊢ { app := fun X ↦ 1 • 𝟙 X, naturality := ⋯ } = 1

Tactic:
cat_disch

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
⊢ { app := fun X ↦ 0 • 𝟙 X, naturality := ⋯ } = 0

Tactic:
cat_disch

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (v : n → R), (∀ (w : m → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → v = 0) ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
dotProduct_transpose_mulVec

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (w : m → R), (∀ (v : n → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → w = 0) ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
dotProduct_transpose_mulVec

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
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
⊢ C a

Tactic:
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 := ι)

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
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
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
of_id : s.val.comp ((lift Q) of) = AlgHom.id R (CliffordAlgebra Q)
⊢ C a
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₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map g) ((map f) x) = x

Tactic:
rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
D : ι → F
hD : (diagonal D).det = 1
i : ι
hi : i ∈ {i | i ≠ i₀}
⊢ P (if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)

Tactic:
simp [(Finset.mem_filter.1 hi).2, hdiag]

Goal state after:
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
i j : Fin 2
h : i ≠ j
c : F
⊢ SpecialLinearGroup.transvection h c ∈ commutator SL(2, F)

Tactic:
by
  fin_cases i
  · obtain rfl : j = 1 := by fin_cases j <;> tauto
    exact transvection_mem_commutator₀ ha hasq c
  · obtain rfl : j = 0 := by fin_cases j <;> tauto
    exact transvection_mem_commutator₁ ha hasq c

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

Goal state before:
pp: R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ (RingHom.id S₂) (y x✝¹) •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
RingHom.id_apply,

Goal state after:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ y x✝¹ •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ y x✝¹ •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
RingHom.id_apply,

Goal state after:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ y x✝¹ •> x x✝³ •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x y : M
⊢ polar (⇑Q) x (a • y) = a • polar (⇑Q) x y

Tactic:
rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ (RingHom.id R) a • f x * g (a • x) = (a * a) • (f x * g x)

Tactic:
RingHom.id_apply,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • f x * g (a • x) = (a * a) • (f x * g x)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • f x * (RingHom.id R) a • g x = (a * a) • (f x * g x)

Tactic:
RingHom.id_apply,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • f x * a • g x = (a * a) • (f x * g x)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
⊢ (toMatrix₂' R) ((toLinearMap₂' R) J' ∘ₗ toLin' A) = (toMatrix₂' R) (((toLinearMap₂' R) J).compl₂ (toLin' A')) ↔
    J.IsAdjointPair J' A A'

Tactic:
LinearMap.toMatrix₂'_comp,

Goal state after:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
⊢ (toMatrix' (toLin' A))ᵀ * (toMatrix₂' R) ((toLinearMap₂' R) J') =
      (toMatrix₂' R) (((toLinearMap₂' R) J).compl₂ (toLin' A')) ↔
    J.IsAdjointPair J' A A'