mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
⊢ yoneda.map
      ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
        (homologyFunctor C (up ℤ) 0).homologySequenceδ
            (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
              ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
            n₀ n₁ h ≫
          (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁) =
    yoneda.map
      (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))

Tactic:
ext ⟨A⟩ (x : A ⟶ _)

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)
⊢ (ConcreteCategory.hom
          ((yoneda.map
                ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
                  (homologyFunctor C (up ℤ) 0).homologySequenceδ
                      (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                        ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫
                          (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
                      n₀ n₁ h ≫
                    (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
            (Opposite.op A))).toFun
      x =
    (ConcreteCategory.hom
          ((yoneda.map
                (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
                  hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
            (Opposite.op A))).toFun
      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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ a + b = 0

Tactic:
rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]

Goal state after:
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✝ : F.CommShift A
a : A
X✝ : C
⊢ (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      ((shiftFunctor C a).map (adj.unit.app X✝) ≫
        adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
            G.map
                ((shiftFunctor D a).map
                  ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝)))) =
    (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      (adj.unit.app ((shiftFunctor C a).obj X✝) ≫
        G.map ((Functor.commShiftIso F a).hom.app X✝) ≫ 𝟙 (G.obj ((shiftFunctor D a).obj (F.obj X✝))))

Tactic:
simp only [comp_id, homEquiv_counit, Functor.map_comp, assoc, counit_naturality,
    counit_naturality_assoc, left_triangle_components_assoc]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝)))) ≫
        (shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝
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
φ : R →+* CatCenter C
X✝ Y✝ : C
this : (X Y : C) → Module R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
simp only [smulOfRingMorphism_smul_eq, assoc]

Goal state after:
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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
have := covariant_sequence_exact₂' X hS n

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  { X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n), X₃ := AddCommGrpCat.of (Ext X S.X₃ n),
      f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      zero := ⋯ }.Exact
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : J₁' (μ x) • (B x) x = 0
y : J₁' (μ x) = 0
⊢ μ x = 0

Tactic:
by simpa using y

Goal state after:
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Tactic:
pow_mul'

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
⊢ e.toMatrix (update v j x) = (e.toMatrix v).updateCol j ⇑(e.repr x)

Tactic:
ext i' k

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ e.toMatrix (update v j x) i' k = (e.toMatrix v).updateCol j (⇑(e.repr x)) i' k
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

Goal state after:
case intro
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
val✝ : Fintype G
⊢ IsCyclic G
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (↑(-↑g)).det

Tactic:
Units.val_neg,

Goal state after:
n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (-↑↑g).det
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i = 0

Tactic:
· rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]

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
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✝

Tactic:
coe_inv,

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).adjugate 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: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
i✝ j✝ : ι
⊢ ↑(transvection hij 0) i✝ j✝ = ↑1 i✝ j✝

Tactic:
simp [transvection_coe]

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 ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
⊢ i1 ≠ i2 → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 i2

Tactic:
hi12

Goal state after:
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
⊢ Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 i2
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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * (ι Q) a * ((ι Q) b * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
mul_assoc,

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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((ι Q) a * ((ι Q) b * y)) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * ((ι Q) b * (ι Q) a * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
mul_assoc,

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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * ((ι Q) b * ((ι Q) a * y)) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)

Tactic:
mul_assoc,

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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * ((ι Q) a * (ι Q) b) = -(x * (ι Q) b * (ι Q) a)
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 b : M
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (ι Q) a - (ι Q) b * (ι Q) a * (ι Q) a =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
mul_assoc,

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 b : M
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (ι Q) a - (ι Q) b * ((ι Q) a * (ι Q) a) =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = mk (l.dProdIndex fun i ↦ (f i).fst) (l.dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
GradedMonoid.mk_list_dProd,

Goal state after:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = (List.map (fun a ↦ mk (f a).fst (f a).snd) l).prod
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y

Tactic:
simp only [polar, Pi.add_apply]
  abel

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B

Tactic:
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂ b₂) id = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ (algebraMap S R) s ∈ A 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ s • 1 ∈ A 0
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'
⊢ ((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J') ⇑(toLin' A) ⇑(toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
rw [isAdjointPair_iff_comp_eq_compl₂]
  have h :
    ∀ B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R,
      B = B' ↔ LinearMap.toMatrix₂' R B = LinearMap.toMatrix₂' R B' := by
    intro B B'
    constructor <;> intro h
    · rw [h]
    · exact (LinearMap.toMatrix₂' R).injective h
  simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂,
    LinearMap.toMatrix'_toLin', LinearMap.toMatrix'_toLinearMap₂']
  rfl

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finsetSum_apply, AddSubmonoidClass.coe_finsetSum]
  simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]

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

Goal state before:
pp: case e'_1.e'_3
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * P * A₂ = ↑v * y

Tactic:
mul_assoc,

Goal state after:
case e'_1.e'_3
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * (P * A₂) = ↑v * y
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case e'_1.e'_3
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * (P * A₂) = ↑v * y

Tactic:
mul_assoc,

Goal state after:
case e'_1.e'_3
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * (J * (P * A₂)) = ↑v * y
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case e'_2.e'_2
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = ↑v⁻¹ * x

Tactic:
mul_assoc,

Goal state after:
case e'_2.e'_2
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * (Pᵀ * J) = ↑v⁻¹ * x
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case e'_2.e'_2
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * (Pᵀ * J) = ↑v⁻¹ * x

Tactic:
mul_assoc,

Goal state after:
case e'_2.e'_2
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₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * (A₁ᵀ * (Pᵀ * J)) = ↑v⁻¹ * x
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).Nondegenerate ↔ M.Nondegenerate

Tactic:
rw [← nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂,
    nondegenerate_toLinearMap₂'_iff]

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 involute.toLinearMap ((ι Q).range ^ ↑i) = ⨆ j, (ι Q).range ^ ↑j

Tactic:
Submodule.map_pow,

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 involute.toLinearMap (ι Q).range ^ ↑i = ⨆ j, (ι Q).range ^ ↑j
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 : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap (p ^ n)) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap p) ^ n

Tactic:
Submodule.map_pow,

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

Goal state before:
pp: case succ.inr
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
hd : finrank K V = d + 1
hB₁ : B ≠ 0
x : V
hx : (B x) x ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd

Goal state after:
case succ.inr
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
⊢ ∃ v, IsOrthoᵢ B ⇑v