mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
⊢ ∀ (n m : M₁),
    (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
      (B₁ n) m

Tactic:
intro n m

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = (B₁ n) m
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
i : ι
⊢ ibc.equiv
      ((TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl S S) b.repr).symm
        (⋯.equiv.symm (Finsupp.single i 1))) =
    ε (b i)

Tactic:
generalize_proofs _ _ _ _ ibcRA

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
i : ι
pf✝³ : RingHomInvPair (RingHom.id S) (RingHom.id S)
pf✝² : SMulCommClass R S S
pf✝¹ : IsScalarTower R S S
pf✝ : IsScalarTower R S (ι →₀ S)
ibcRA : IsBaseChange S (Finsupp.mapRange.linearMap (Algebra.linearMap R S))
⊢ ibc.equiv
      ((TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl S S) b.repr).symm
        (ibcRA.equiv.symm (Finsupp.single i 1))) =
    ε (b i)
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb) (sl, sr) = σ₁⁻¹ * σ₂
⊢ Perm.sign σ₁ • MultilinearMap.domDomCongr σ₁ ((↑a).domCoprod ↑b) =
    Perm.sign σ₂ • MultilinearMap.domDomCongr σ₂ ((↑a).domCoprod ↑b)

Tactic:
ext v

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb) (sl, sr) = σ₁⁻¹ * σ₂
v : ιa ⊕ ιb → Mᵢ
⊢ (Perm.sign σ₁ • MultilinearMap.domDomCongr σ₁ ((↑a).domCoprod ↑b)) v =
    (Perm.sign σ₂ • MultilinearMap.domDomCongr σ₂ ((↑a).domCoprod ↑b)) v
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) ↔
    (affineCombination k univ s.points) w ∈ ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
Set.mem_inter_iff,

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (affineCombination k univ s.points) w ∈ s.closedInterior ∧
      (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) ↔
    (affineCombination k univ s.points) w ∈ ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : e ∈ fixingSubgroup (V ≃ₗ[R] V) W.carrier
⊢ map (↑e) W = W

Tactic:
ext v

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : e ∈ fixingSubgroup (V ≃ₗ[R] V) W.carrier
v : V
⊢ v ∈ map (↑e) W ↔ v ∈ W
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
i j : ι
hij : i ≠ j
r : R
this : f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
⊢ r • f (b j) = (b.coord i) (f (b i)) • r • b j

Tactic:
rw [LinearMap.ext_iff] at this

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → f * (b.coord i).transvection (r • b j) = (b.coord i).transvection (r • b j) * f
i j : ι
hij : i ≠ j
r : R
this : ∀ (x : V), (f * (b.coord i).transvection (r • b j)) x = ((b.coord i).transvection (r • b j) * f) x
⊢ r • f (b j) = (b.coord i) (f (b i)) • r • b j
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ f x • v = 0

Tactic:
by
      rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
      rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s + t * (b.coord i) (f (b i)) = 0
this : s * r + t * (r * (b.repr (f (b j))) j) = -(t * (b.repr (f (b i))) j)
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s + t * (b.coord i) (f (b i)) = 0
this : s * r + t * r * (b.repr (f (b j))) j = -(t * (b.repr (f (b i))) j)
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
⊢ e.symm ∈ dilatransvections R V ↔ e ∈ dilatransvections R V

Tactic:
suffices ∀ e ∈ dilatransvections R V, e.symm ∈ dilatransvections R V from
    ⟨by simpa using this e.symm, this e⟩
  rintro e ⟨f, v, he⟩
  use f, - e.symm v
  ext x
  suffices x = e x - f x • v by
    simpa [LinearMap.transvection.apply, ← sub_eq_add_neg, symm_apply_eq]
  rw [eq_comm, sub_eq_iff_eq_add, ← coe_coe, he, LinearMap.transvection.apply]

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

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (polarBilin Q)

Tactic:
QuadraticForm.baseChange,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.baseChange A (polarBilin Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (toBaseChange A Q).comp involute = (Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)

Tactic:
ext v

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((toBaseChange A Q).comp involute).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ -1 ⊗ₜ[R] (ι Q) v = 1 ⊗ₜ[R] (-(ι Q) v)

Tactic:
TensorProduct.tmul_neg

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ -1 ⊗ₜ[R] (ι Q) v = -1 ⊗ₜ[R] (ι Q) v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (AlgHom.op (toBaseChange A Q)).comp reverseOp =
    (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))

Tactic:
ext v

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((AlgHom.op (toBaseChange A Q)).comp reverseOp).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
                ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp
                  (toBaseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
this :
  ((AlgHom.op (toBaseChange A Q)).comp reverseOp) x =
    ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
        ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q)))
      x
⊢ (toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)

Tactic:
refine (congr_arg unop this).trans ?_

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
this :
  ((AlgHom.op (toBaseChange A Q)).comp reverseOp) x =
    ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
        ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q)))
      x
⊢ unop
      (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
          ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q)))
        x) =
    (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id A (A ⊗[R] CliffordAlgebra Q)

Tactic:
ext v

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (((AlgHom.restrictScalars R ((toBaseChange A Q).comp (ofBaseChange A Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v =
    (((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] CliffordAlgebra Q))).comp
            Algebra.TensorProduct.includeRight).toLinearMap ∘ₗ
        ι Q)
      v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ * x₂ = y * (x₁ * x₂)

Tactic:
← mul_assoc

Goal state after:
case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ * x₂ = y * x₁ * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ reverse ((ι 0) x) = (ι 0) x

Tactic:
ι_eq_zero,

Goal state after:
case ι
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ reverse (0 x) = 0 x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ((Algebra.ofId R (CliffordAlgebra 0)).comp ((lift 0) ⟨0, ⋯⟩)).toLinearMap ∘ₗ ι 0 =
    (AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0

Tactic:
ι_eq_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ ((Algebra.ofId R (CliffordAlgebra 0)).comp ((lift 0) ⟨0, ⋯⟩)).toLinearMap ∘ₗ 0 =
    (AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) (x✝² • x✝), ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
simp only [map_smul, mul_smul_comm]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
m : M
inst✝ : Invertible (Q m)
⊢ (ι Q) (⅟(Q m) • m) * (ι Q) m = 1

Tactic:
rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (gradedCommAux R 𝒜 ℬ) ((lof R (ι × ι) (fun i ↦ 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b)) =
    (-1) ^ (j * i) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)

Tactic:
rw [gradedCommAux]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (DirectSum.toModule R (ι × ι) (⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) fun i ↦
        have o := lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (i.2, i.1);
        have s := (-1) ^ (i.1 * i.2);
        (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)))
      ((lof R (ι × ι) (fun i ↦ 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b)) =
    (-1) ^ (j * i) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
⊢ ∀ (x y : A), (x + y) ᵍ⊗ₜ[R] 1 = x ᵍ⊗ₜ[R] 1 + y ᵍ⊗ₜ[R] 1

Tactic:
by simp [tmul, TensorProduct.add_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ toTensorAlgebra (GradedMonoid.GMul.mul a b) = toTensorAlgebra a * toTensorAlgebra b

Tactic:
TensorPower.gMul_eq_coe_linearMap,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ toTensorAlgebra ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv) a) b) =
    toTensorAlgebra a * toTensorAlgebra b
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (DirectSum.coeAlgHom fun i ↦ ⋀[R]^i M).comp (GradedAlgebra.liftι R M) = AlgHom.id R (ExteriorAlgebra R M)

Tactic:
by
      ext m
      dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply,
        AlgHom.id_apply, GradedAlgebra.liftι]
      rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case e'_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
⊢ (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯,
            right_inv := ⋯ }).graph.toAddSubgroup =
    e.toAddMonoidHom.graph

Tactic:
ext v

Goal state after:
case e'_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
v : (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd
⊢ v ∈
      (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯,
              right_inv := ⋯ }).graph.toAddSubgroup ↔
    v ∈ e.toAddMonoidHom.graph
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ∀ (j : Fin (n + 1)), j ≠ i₀ → ∑ i, Mᵀ i j = 0

Tactic:
by simpa using hv

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (↑S * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))

Tactic:
S

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (!![0, -1; 1, 0] * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: ⊢ reps 0 = ∅

Tactic:
rw [reps, Set.eq_empty_iff_forall_notMem]
  rintro A ⟨h₁, h₂, -, h₄⟩
  suffices |A.1 0 1| < 0 by linarith [abs_nonneg (A.1 0 1)]
  have := A_c_eq_zero h₁
  simp_all [h₂.ne']

Goal state after: