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:
;

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.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₃ (g (f n))) (g (f m))

Tactic:
;

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₃ (g (f n))) (g (f m))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
h : Nonempty ↥s
c : P
⊢ s.shift c 0 = mk' c s.direction

Tactic:
refine ext_of_direction_eq (by simp) ⟨c, ?_⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
h : Nonempty ↥s
c : P
⊢ c ∈ ↑(s.shift c 0) ∩ ↑(mk' c s.direction)
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
x y : S
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (((x + y) • compRight R ε) x✝¹) x✝ = ((x • compRight R ε + y • compRight R ε) x✝¹) x✝

Tactic:
;

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
ε : N →ₗ[R] P
x y : S
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ (((x + y) • compRight R ε) x✝¹) x✝ = ((x • compRight R ε + y • compRight R ε) x✝¹) 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:
;

Goal state after:
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✝
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
Q : Type u_6
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
x✝ : M
⊢ (↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α) x✝ = (β ∘ₗ f) x✝

Tactic:
;

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
Q : Type u_6
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
x✝ : M
⊢ (↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α) x✝ = (β ∘ₗ f) x✝
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
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 α
f : M →ₗ[R] M
x✝ : M
⊢ (↑R (j.endHom f) ∘ₗ α) x✝ = (α ∘ₗ f) x✝

Tactic:
;

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
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 α
f : M →ₗ[R] M
x✝ : M
⊢ (↑R (j.endHom f) ∘ₗ α) x✝ = (α ∘ₗ f) x✝
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_4
inst✝² : Ring R
V : Type u_5
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ f.fixedSubmodule ↔ x✝ ∈ (f - id).ker

Tactic:
;

Goal state after:
R : Type u_4
inst✝² : Ring R
V : Type u_5
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ f.fixedSubmodule ↔ x✝ ∈ (f - id).ker
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
f g : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ f.fixedSubmodule ⊓ g.fixedSubmodule → x✝ ∈ (f ∘ₗ g).fixedSubmodule

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ f.fixedSubmodule ⊓ g.fixedSubmodule → x✝ ∈ (f ∘ₗ g).fixedSubmodule
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
f g : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ (f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule → x✝ ∈ f.fixedSubmodule

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : V →ₗ[R] V
x✝ : V
⊢ x✝ ∈ (f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule → x✝ ∈ f.fixedSubmodule
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case mp
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
x : V
⊢ e.fixedReduce ((↑e).fixedSubmodule.mkQ x) = (↑e).fixedSubmodule.mkQ (a • x)

Tactic:
;

Goal state after:
case mp
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
H : ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
x : V
⊢ e.fixedReduce ((↑e).fixedSubmodule.mkQ x) = (↑e).fixedSubmodule.mkQ (a • x)
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
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
⊢ ∃ x, ∃ (h : ∀ (g : R), g * x = x * g), f = ⟨x, ⋯⟩ • 1

Tactic:
have h_allEq (i j : ι) : b.coord i (f (b i)) = b.coord j (f (b j)) := by
    by_cases hij : j = i
    · simp [hij]
    simpa using congr_arg (b.coord i) (hcomm j i hij 1)

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
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
⊢ ∃ x, ∃ (h : ∀ (g : R), g * x = x * g), f = ⟨x, ⋯⟩ • 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v w : V
hw : f w = 0
x✝ : V
⊢ (transvection f v ∘ₗ transvection f w) x✝ = (transvection f (v + w)) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v w : V
hw : f w = 0
x✝ : V
⊢ (transvection f v ∘ₗ transvection f w) x✝ = (transvection f (v + w)) x✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : Dual R V
v : V
hf : f v = 0
x✝ : V
⊢ (transvection f v ∘ₗ transvection g v) x✝ = (transvection (f + g) v) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : Dual R V
v : V
hf : f v = 0
x✝ : V
⊢ (transvection f v ∘ₗ transvection g v) x✝ = (transvection (f + g) v) x✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r s : R
x : V
⊢ x + (f x • r • v + f x • s • (v + f v • r • v)) = x + f x • (r + (s + s * f v * r)) • v

Tactic:
simp only [smul_add, ← mul_smul, ← add_smul, ← mul_add (f x), mul_assoc]

Goal state after:
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
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, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ ((b.repr x) i * f (b i)) • (b.repr v) i • b i = 0

Tactic:
← mul_smul,

Goal state after:
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
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, ⋯⟩
hfv : f (b i) * (b.repr v) i = 0
this : ∀ (x : V), x = (b.repr x) i • b i
⊢ ((b.repr x) i * f (b i) * (b.repr v) i) • b i = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
W : Type u_3
inst✝¹ : AddCommMonoid W
inst✝ : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
x✝ : W
⊢ (↑e ∘ₗ transvection f v ∘ₗ ↑e.symm) x✝ = ((f ∘ₗ ↑e.symm).transvection (e v)) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
W : Type u_3
inst✝¹ : AddCommMonoid W
inst✝ : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
x✝ : W
⊢ (↑e ∘ₗ transvection f v ∘ₗ ↑e.symm) x✝ = ((f ∘ₗ ↑e.symm).transvection (e v)) x✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
W : Type u_3
inst✝¹ : AddCommMonoid W
inst✝ : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
⊢ ↑e ∘ₗ transvection f v ∘ₗ ↑e.symm = (f ∘ₗ ↑e.symm).transvection (e v)

Tactic:
by
  ext; simp [transvection.apply]

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 w : V
hv : f v = 0
hw : f w = 0
hvw : f (v + w) = 0
x✝ : V
⊢ (transvection hw ≪≫ₗ transvection hv) x✝ = (transvection hvw) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v w : V
hv : f v = 0
hw : f w = 0
hvw : f (v + w) = 0
x✝ : V
⊢ (transvection hw ≪≫ₗ transvection hv) x✝ = (transvection hvw) x✝
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 g : Dual R V
v : V
hf : f v = 0
hg : g v = 0
hfg : (f + g) v = 0
x✝ : V
⊢ (transvection hg ≪≫ₗ transvection hf) x✝ = (transvection hfg) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f g : Dual R V
v : V
hf : f v = 0
hg : g v = 0
hfg : (f + g) v = 0
x✝ : V
⊢ (transvection hg ≪≫ₗ transvection hf) x✝ = (transvection hfg) x✝
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
v : V
hv : 0 v = 0
x✝ : V
⊢ (transvection hv) x✝ = (refl R V) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
v : V
hv : 0 v = 0
x✝ : V
⊢ (transvection hv) x✝ = (refl R V) x✝
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
hf : f 0 = 0
x✝ : V
⊢ (transvection hf) x✝ = (refl R V) x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
hf : f 0 = 0
x✝ : V
⊢ (transvection hf) x✝ = (refl R V) x✝
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
hv : f v = 0
hv' : f (-v) = 0
x✝ : V
⊢ (transvection hv).symm x✝ = (transvection hv') x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hv : f v = 0
hv' : f (-v) = 0
x✝ : V
⊢ (transvection hv).symm x✝ = (transvection hv') x✝
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
hf : f v = 0
hf' : (-f) v = 0
x✝ : V
⊢ (transvection hf).symm x✝ = (transvection hf') x✝

Tactic:
;

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hf : f v = 0
hf' : (-f) v = 0
x✝ : V
⊢ (transvection hf).symm x✝ = (transvection hf') x✝
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
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)))
h2 : t = 0 ∨ r * (b.coord j) (f (b j)) = (b.coord i) (f (b i)) * r
hst : t = 0
⊢ ¬(s = 0 → ¬t = 0)

Tactic:
;

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
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)))
h2 : t = 0 ∨ r * (b.coord j) (f (b j)) = (b.coord i) (f (b i)) * r
hst : t = 0
⊢ ¬(s = 0 → ¬t = 0)
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:
;

Goal state after:
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✝
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
⊢ 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)

Tactic:
;

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
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ (↑(AlgEquiv.toOpposite A A)).toLinearMap)
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)

Tactic:
rw [reverse, AlgEquiv.toAlgHom_toLinearMap, AlgEquiv.toLinearEquiv_toOpposite]

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)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑(opLinearEquiv A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
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
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : Dual R V
v x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (transvection ((Dual.baseChange A) f) (1 ⊗ₜ[R] v))) 1) x✝

Tactic:
;

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : Dual R V
v x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (transvection ((Dual.baseChange A) f) (1 ⊗ₜ[R] v))) 1) x✝
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case pos
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : x = y
⊢ (Finsupp.single y 1) y = 1 y y

Tactic:
;

Goal state after:
case pos
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : x = y
⊢ (Finsupp.single y 1) y = 1 y y
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝