mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
a : ι → A
v : V
⊢ ∑ i, a i • b i = v ↔ ∑ i, (⇑(algebraMap A R) ∘ a) i • b i = v

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
ε : N →ₗ[R] P
r : R
s : S
⊢ (r • s) • compRight R ε = (RingHom.id R) r • s • compRight R ε

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case zero
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
ε : N →ₗ[R] P
s : S
⊢ (TensorProduct.lift { toFun := fun s ↦ s • compRight R ε, map_add' := ⋯, map_smul' := ⋯ }) (s • 0) =
    s • (TensorProduct.lift { toFun := fun s ↦ s • compRight R ε, map_add' := ⋯, map_smul' := ⋯ }) 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∀ i_1 ∈ univ.erase i, w i_1 = 0
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hshift : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ w j = Pi.single i 1 j

Tactic:
simp [hw j (by simpa using hj), hj]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_2.e_f.h
ι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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    c • Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
rw [smul_comm]

Goal state after:
case refine_2.e_f.h
ι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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
B : Type u_5
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Dual R V
x✝ : V
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry ((baseChange B) ((baseChange A) f))) 1)) 1) x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry ((congr (cancelBaseChange R A B B V)).symm ((baseChange B) f))) 1))
        1)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
r : R
a : A
⊢ (r • a) • ibc.toDual = (RingHom.id R) r • a • ibc.toDual

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
⊢ ∀ (j : Fin n), 0 ≤ w j

Tactic:
intro j

Goal state after:
case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
j : Fin n
⊢ 0 ≤ w j
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: case zero
R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
⊢ (TensorProduct.lift { toFun := fun a ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }).toFun (a • 0) =
    (RingHom.id A) a • (TensorProduct.lift { toFun := fun a ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }).toFun 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ (Finsupp.llift P R S ι).symm
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P := (↑f ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ ↑e'.symm
φ : M →ₗ[R] N
i : ι
⊢ ((AlgebraTensorModule.curry (↑f ∘ₗ linearMapRightBaseChangeHom S M ε)) 1) φ i =
    ((AlgebraTensorModule.curry (↑⋯.equiv ∘ₗ ↑e')) 1) φ i

Tactic:
simp

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ (Finsupp.llift P R S ι).symm
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P := (↑f ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ ↑e'.symm
φ : M →ₗ[R] N
i : ι
⊢ f ((linearMapRightBaseChangeHom S M ε) (1 ⊗ₜ[R] φ)) i = ⋯.equiv (e' (1 ⊗ₜ[R] φ)) i
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_4.e_f.h
ι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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    c • Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
rw [smul_comm]

Goal state after:
case refine_4.e_f.h
ι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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: case zero
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
⊢ (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) 0 =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case zero
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ (j.endHom 1) 0 = 1 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
U : Type u_2
V : Type u_3
inst✝³ : AddCommMonoid U
inst✝² : AddCommMonoid V
inst✝¹ : Module R U
inst✝ : Module R V
e : V ≃ₗ[R] V
f : V →ₗ[R] V
⊢ 0 ∈ {x | f x = x}

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : Semiring R✝
U : Type u_2
V✝ : Type u_3
inst✝⁶ : AddCommMonoid U
inst✝⁵ : AddCommMonoid V✝
inst✝⁴ : Module R✝ U
inst✝³ : Module R✝ V✝
e : V✝ ≃ₗ[R✝] V✝
P : Submodule R✝ U
Q : Submodule R✝ V✝
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
y : V
⊢ (Quotient.equiv W W ↑(u * v) ⋯) (W.mkQ y) = (Quotient.equiv W W ↑u ⋯ * Quotient.equiv W W ↑v ⋯) (W.mkQ y)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: 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
q : P
hq : q ∈ (s.faceOpposite i).closedInterior
hp : (homothety (s.points i) x) q ∉ affineSpan k (Set.range s.points)
⊢ s.points i ∈ Set.range s.points

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: 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
q : P
hq : q ∈ (s.faceOpposite i).closedInterior
hp : (homothety (s.points i) x) q ∉ affineSpan k (Set.range s.points)
⊢ Set.range (s.faceOpposite i).points ⊆ Set.range s.points

Tactic:
simp

Goal state after:
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
hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))
hV : Subsingleton V
⊢ ∀ (g : R), g * 1 = 1 * g

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
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
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := ⋯
x : V
⊢ ∀ x_1 ∈ (b.repr x).support, f ((b.repr x) x_1 • b x_1) = ⟨(b.coord i) (f (b i)), ⋯⟩ • (b.repr x) x_1 • b x_1

Tactic:
intro j

Goal state after:
case inr
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
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
j : ι
⊢ j ∈ (b.repr x).support → f ((b.repr x) j • b j) = ⟨(b.coord i) (f (b i)), ⋯⟩ • (b.repr x) j • b j
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i : ι
⊢ ∀ (i_1 : ι), (b.repr (f (b i))) i_1 = (b.repr ((b.coord i) (f (b i)) • b i)) i_1

Tactic:
intro j

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i j : ι
⊢ (b.repr (f (b i))) j = (b.repr ((b.coord i) (f (b i)) • b i)) j
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
f : Dual R V
v : V
h : f v = 0
r : R
x : V
⊢ (LinearMap.transvection f v) (r • x) = (RingHom.id R) r • (LinearMap.transvection f v) x

Tactic:
simp

Goal state after:
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
⊢ 0 0 = 0

Tactic:
simp

Goal state after:
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
f : Dual R V
v : V
hfv : f v = 0
⊢ ↑(transvection hfv) = LinearMap.transvection f v

Tactic:
simp

Goal state after:
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
f : Dual R V
v : V
h : IsUnit (1 + f v)
r : R
x : V
⊢ (LinearMap.transvection f v) (r • x) = (RingHom.id R) r • (LinearMap.transvection f v) x

Tactic:
simp

Goal state after:
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
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ 1 = (↑1 + f v) * ↑h.unit⁻¹

Tactic:
simp

Goal state after:
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
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * (1 + ↑(-h.unit⁻¹) * (1 + f v)) = 0

Tactic:
simp

Goal state after:
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
f : Dual R V
v : V
h : IsUnit (1 + f v)
⊢ ↑(dilatransvection h) = LinearMap.transvection f v

Tactic:
simp

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
r : R
j : ι
hij : j ≠ i
⊢ r * (b.coord j) ((b.coord i) ((b.coord i) (f (b i)) • b i) • b j) = r * (b.coord i) ((b.coord i) (f (b i)) • b i)

Tactic:
simp

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

Goal state before:
pp: V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : ↑e = LinearMap.transvection f v
⊢ Cardinal.mk ↑{v} ≤ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : QuadraticModuleCat R
i : X ≅ Y
x : ↑X.toModuleCat
⊢ (QuadraticModuleCat.Hom.toIsometry (i.hom ≫ i.inv)) x = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : QuadraticModuleCat R
i : X ≅ Y
x : ↑Y.toModuleCat
⊢ (QuadraticModuleCat.Hom.toIsometry (i.inv ≫ i.hom)) x = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
_M : QuadraticModuleCat R
⊢ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (𝟙 _M))) = 𝟙 (AlgCat.of R (CliffordAlgebra _M.form))

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
_M _N _P : QuadraticModuleCat R
f : _M ⟶ _N
g : _N ⟶ _P
x✝ : ↑_M.toModuleCat
⊢ ((AlgCat.Hom.hom (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))))).toLinearMap ∘ₗ
        CliffordAlgebra.ι _M.form)
      x✝ =
    ((AlgCat.Hom.hom
            (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫
              AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g)))).toLinearMap ∘ₗ
        CliffordAlgebra.ι _M.form)
      x✝

Tactic:
simp

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

Goal state before:
pp: case h₀
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ ∀ (b_1 : Unit), (b.repr (u.rangeRestrict x)) b_1 ≠ 0 → b_1 ≠ default → (b.repr (u.rangeRestrict x)) b_1 • b b_1 = 0

Tactic:
simp

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

Goal state before:
pp: case h₁
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ (b.repr (u.rangeRestrict x)) default = 0 → 0 • b default = 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
⊢ Q₁ 0 = Q₂ 0

Tactic:
simp

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

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry Q₁.polarBilin) 1) x✝¹)) 1) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry Q₂.polarBilin) 1) x✝¹)) 1) x✝

Tactic:
dsimp [polar]

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
x✝¹ x✝ : M₂
⊢ Q₁ (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) - Q₁ (1 ⊗ₜ[R] x✝¹) - Q₁ (1 ⊗ₜ[R] x✝) =
    Q₂ (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) - Q₂ (1 ⊗ₜ[R] x✝¹) - Q₂ (1 ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : e ∈ dilatransvections K V
he' : e.fixedReduce = 1
he_one : e = 1
⊢ 0 0 = 0

Tactic:
simp

Goal state after:
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
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
v w : V
⊢ (1 * 1) ⊗ₜ[R] (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) v w) =
    ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1

Tactic:
QuadraticForm.polarBilin_baseChange,

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
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
v w : V
⊢ (1 * 1) ⊗ₜ[R] (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) v w) =
    ((LinearMap.BilinForm.baseChange A (QuadraticMap.polarBilin Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
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
⊢ (((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

Tactic:
simp

Goal state after: