mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
⊢ i < i + 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ i < i + 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ (ComplexShape.up ℤ).prev i = i - 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ i - 1 < i

Tactic:
by simp

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

Goal state before:
pp: R : Type t
inst✝⁵ : Ring R
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
⊢ ∀ (m : R) (x : Ext X Y n), homAddEquiv.toFun (m • x) = (RingHom.id R) m • homAddEquiv.toFun x

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext X Y a
⊢ ∀ (x y : Ext Y Z b), α.comp (x + y) h = α.comp x h + α.comp y h

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext X Y a
⊢ ∀ (m : R) (x : Ext Y Z b), α.comp (m • x) h = (RingHom.id R) m • α.comp x h

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
j : ℤ
ι : (singleFunctor C (j + 1)).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE (j + 1)
inst✝ : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I).inv ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I).hom ≫ α
⊢ j < j + 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
S T : Submodule R₁ M₁
⊢ 0 ∈ {y | ∀ x ∈ S, (B x) y = 0}

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Set.range relations.relation

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
g : relations.G
⊢ h.linearEquiv (h.linearEquiv.symm (solution.var g)) = h.linearEquiv (relations.toQuotient (Finsupp.single g 1))

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
⊢ solution.postcomp ((fun s ↦ h.desc s) ((fun f ↦ solution.postcomp f) f)) = solution.postcomp f

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ (fun f ↦ solution.postcomp f) ((fun s ↦ h.desc s) s) = s

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp (h.desc solution' ∘ₗ h'.desc solution) = solution'.postcomp LinearMap.id

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp (h'.desc solution ∘ₗ h.desc solution') = solution.postcomp LinearMap.id

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ ∀ (r : relations.R), relations.toQuotient (relations.relation r) = 0

Tactic:
by simp

Goal state after:
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✝ : Fintype ι
⊢ ∑ i, e.toMatrix v i j • e i = v j

Tactic:
by
  simp_rw [e.toMatrix_apply, e.sum_repr]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: M✝ : Type u_1
inst✝⁶ : MonoidWithZero M✝
inst✝⁵ : Finite M✝
M : Type u_2
inst✝⁴ : MonoidWithZero M
inst✝³ : IsLeftCancelMulZero M
inst✝² : DecidableEq M
inst✝¹ : Fintype M
inst✝ : Nontrivial M
⊢ (if h : 0 = 0 then 0 else bijInv ⋯ 1) = 0

Tactic:
by simp

Goal state after:
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
S : Subgroup Rˣ
inst✝ : Finite ↥S
⊢ ∀ (x y : ↥S), ↑↑(x * y) = ↑↑x * ↑↑y

Tactic:
by simp

Goal state after:
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✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∀ (x : Rˣ), x ∈ image (⇑f.toHomUnits) univ ↔ x ∈ f.toHomUnits.range

Tactic:
by simp

Goal state after:
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✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∀ a ∈ range (orderOf x), x ^ a ∈ univ

Tactic:
by simp

Goal state after:
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✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∀ a ∈ range (orderOf x), ↑↑x ^ a = ↑↑(x ^ a)

Tactic:
by simp

Goal state after:
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 : ℕ
M : Type u_7
inst✝ : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ (fun ζ ↦ ⟨↑↑ζ, ⋯⟩) ((fun ζ ↦ ⟨toUnits ↑ζ, ⋯⟩) ζ) = ζ

Tactic:
simp only [val_toUnits_apply, Subtype.coe_eta]

Goal state after:
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✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
H : ∀ (a : L), f a ∈ S
x✝ : L
⊢ ((fun f ↦ S.subtype.comp f) (f.codRestrict S H)) x✝ = f x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
a b : SpecialLinearGroup n R
⊢ (mapGL S) a = (mapGL S) b → a = b

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
⊢ IsometryEquiv Q (weightedSumSquares K fun i ↦ Q (v i))

Tactic:
let iso := Q.isometryEquivBasisRepr v

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
⊢ IsometryEquiv Q (weightedSumSquares K fun i ↦ Q (v i))
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i
x y : ι → R
⊢ u • (x + y) = u • x + u • y

Tactic:
by simp

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

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i
x : ι → R
⊢ (fun x ↦ u⁻¹ • x) ((fun x ↦ u • x) x) = x

Tactic:
by simp

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

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : Field K
inst✝⁹ : Invertible 2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * ↑(u i) ^ 2 = w i
x : ι → R
⊢ (fun x ↦ u • x) ((fun x ↦ u⁻¹ • x) x) = x

Tactic:
by simp

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
t : TransvectionStruct n R
⊢ t.toMatrix.det = 1

Tactic:
by simp

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
a inv✝ : R
val_inv✝ : a * inv✝ = 1
inv_val✝ : inv✝ * a = 1
ha : { val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ rootsOfUnity (Fintype.card n) R
⊢ ↑↑((fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯)
          ((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) ⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩)) =
    ↑↑⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Tactic:
refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, -v; b, u].det = 1

case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, a; -u, b].det = 1
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
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
by
  rw [det_diagonal, show Finset.univ = insert i₀ ({i | i ≠ i₀} : Finset ι) by grind,
    Finset.prod_insert (by grind), mul_eq_one_iff_eq_inv₀ (by grind),
    ← Finset.prod_inv_distrib] at hD
  ext x
  by_cases hx : x = i₀
  · simpa [hx, hD, -Finset.prod_inv_distrib] using Finset.prod_congr rfl (by grind)
  · simp [hx]

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 ι
D : ι → F
hD : ∏ i, D i = 1
j : ι
h : D j = 0
⊢ False

Tactic:
show Finset.univ = insert j ({i | i ≠ j} : Finset ι) by grind,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : ∏ i ∈ insert j {i | i ≠ j}, D i = 1
h : D j = 0
⊢ False
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_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a + f b) * f b - f a * f a - f b * f b

Tactic:
add_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
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b
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
⊢ -((ι Q) b * (ι Q) a) * x = -((ι Q) b * ((ι Q) a * x))

Tactic:
neg_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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ -((ι Q) b * (ι Q) a * x) = -((ι Q) b * ((ι Q) a * x))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

Tactic:
refine Subtype.ext <| Matrix.ext fun i j ↦ ?_

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
i j : Fin 2
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b)) i j =
    ↑(SpecialLinearGroup.transvection ⋯ c) i j
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
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ l, r j ∈ A (i j)
⊢ (List.map r l).prod ∈ A (List.map i l).sum

Tactic:
by
  match l with
  | [] =>
    rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
    exact one_mem_graded _
  | head::tail =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
    exact
      mul_mem_graded (h _ List.mem_cons_self)
        (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)

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
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c'

Tactic:
refine Subtype.ext <| Matrix.ext fun i j ↦ ?_

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)
i j : Fin 2
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b)) i j =
    ↑(SpecialLinearGroup.transvection ⋯ c') i j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
| (B (l (Pi.single i 1))) (r (Pi.single j 1))

Tactic:
rw [← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
| ((Pi.basisFun R n).repr (l (Pi.single i 1))).sum fun i xi ↦
    ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
      xi •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ (toMatrix₂' R) (((toLinearMap₂' R) M).compl₁₂ (toLin' P) (toLin' Q)) = (toMatrix₂' R) ((toLinearMap₂' R) (Pᵀ * M * Q))

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ i ∈ univ

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ j ∈ univ

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
⊢ x = y

Tactic:
obtain ⟨_, _, xr⟩ := x
    obtain ⟨_, yl, _⟩ := y
    congr
    exact Function.LeftInverse.eq_rightInverse xr yl

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

Goal state before:
pp: 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
x : M
⊢ 2 • Q x = (2 • Q) x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_3
ι : Type u_1
R : Type u_2
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 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A), ↑(((decompose 𝒜) (m * y)) 0) = ↑(((decompose 𝒜) m) 0) * ↑(((decompose 𝒜) y) 0)) →
      (∀ (y : A), ↑(((decompose 𝒜) (m' * y)) 0) = ↑(((decompose 𝒜) m') 0) * ↑(((decompose 𝒜) y) 0)) →
        ∀ (y : A), ↑(((decompose 𝒜) ((m + m') * y)) 0) = ↑(((decompose 𝒜) (m + m')) 0) * ↑(((decompose 𝒜) y) 0)

Tactic:
rintro _ _ ha hb _
      simp only [add_mul, decompose_add, add_apply, AddMemClass.coe_add, ha, hb]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
A✝ : Type u_3
σ : Type u_4
R : Type u_5
inst✝⁵ : CommSemiring R
A : Type u_6
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
ι : Type u_7
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
M : ι → Submodule R A
inst✝ : SetLike.GradedMonoid M
hM : IsInternal M
r : R
⊢ (RingEquiv.ofBijective (coeAlgHom M) hM).toFun ((algebraMap R (⨁ (i : ι), ↥(M i))) r) = (algebraMap R A) r

Tactic:
by simp

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✝¹ : HasAntidiagonal ι
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
x✝ : ι × ι
⊢ x✝ ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = n} → x✝ ∈ antidiagonal n

Tactic:
by simp

Goal state after: