mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_3
ι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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
⊢ m.domCoprod (n₁ + n₂) = m.domCoprod n₁ + m.domCoprod n₂

Tactic:
ext

Goal state after:
case refine_3
ι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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
⊢ (m.domCoprod (n₁ + n₂)) x✝ = (m.domCoprod n₁ + m.domCoprod 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
⊢ (baseChange B) ((baseChange A) f) = (congr (cancelBaseChange R A B B V)).symm ((baseChange B) f)

Tactic:
ext

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.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_4
ι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₂
⊢ m.domCoprod (c • n) = c • m.domCoprod n

Tactic:
ext

Goal state after:
case refine_4
ι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ᵢ
⊢ (m.domCoprod (c • n)) x✝ = (c • m.domCoprod n) 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
⊢ ↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α = β ∘ₗ f

Tactic:
ext

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
⊢ ↑R (j.endHom f) ∘ₗ α = α ∘ₗ f

Tactic:
ext

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
⊢ f.fixedSubmodule = (f - id).ker

Tactic:
ext

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_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
⊢ (∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x) ↔
    ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)

Tactic:
constructor

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
⊢ (∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x) →
    ∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)

case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
⊢ (∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)) →
    ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • 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 w : V
hw : f w = 0
⊢ transvection f v ∘ₗ transvection f w = transvection f (v + w)

Tactic:
ext

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
⊢ transvection f v ∘ₗ transvection g v = transvection (f + g) v

Tactic:
ext

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
v : V
⊢ transvection 0 v = id

Tactic:
ext

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v x✝ : V
⊢ (transvection 0 v) x✝ = id 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
⊢ transvection f 0 = id

Tactic:
ext

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
x✝ : V
⊢ (transvection f 0) x✝ = id 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:
ext

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✝² : 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
⊢ transvection hw ≪≫ₗ transvection hv = transvection hvw

Tactic:
ext

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
⊢ transvection hg ≪≫ₗ transvection hf = transvection hfg

Tactic:
ext

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
⊢ transvection hv = refl R V

Tactic:
ext

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
⊢ transvection hf = refl R V

Tactic:
ext

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
⊢ (transvection hv).symm = transvection hv'

Tactic:
ext

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
⊢ (transvection hf).symm = transvection hf'

Tactic:
ext

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.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
⊢ e ∈ {e | ∃ f v, ↑e = LinearMap.transvection f v} ↔ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1

Tactic:
constructor

Goal state after:
case mp
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
⊢ e ∈ {e | ∃ f v, ↑e = LinearMap.transvection f v} → Module.rank K ↥(↑e - LinearMap.id).range ≤ 1

case mpr
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
⊢ Module.rank K ↥(↑e - LinearMap.id).range ≤ 1 → e ∈ {e | ∃ f v, ↑e = LinearMap.transvection f v}
Module: Mathlib.LinearAlgebra.TensorProduct.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
⊢ AlgHom.op.symm
      ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))) =
    AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)

Tactic:
ext

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : A
⊢ ((AlgHom.op.symm
            ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
              (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)))).comp
        includeLeft)
      x✝ =
    ((AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)).comp includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : B
⊢ ((AlgHom.restrictScalars R
            (AlgHom.op.symm
              ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
                (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))).comp includeRight) x✝
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) =
    ↑(AlgebraTensorModule.rid R A A).congrRight₂ ((BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂))

Tactic:
← BilinMap.tmul,

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = ↑(AlgebraTensorModule.rid R A A).congrRight₂ ((associated Q₁).tmul (associated Q₂))
Module: Mathlib.LinearAlgebra.TensorProduct.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
⊢ (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯) =
    AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)

Tactic:
ext

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : Aᵐᵒᵖ
⊢ (((AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯)).comp
        includeLeft)
      x✝ =
    ((AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)).comp includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : Bᵐᵒᵖ
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp
              (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ))).comp includeRight) x✝
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
⊢ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))) =
    AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g))

Tactic:
ext

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.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
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
⊢ u x = (b.repr (u.rangeRestrict x)) default • ↑(b default)

Tactic:
by
      rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]
      nth_rewrite 1 [← b.linearCombination_repr (u.rangeRestrict x)]
      rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default] <;> simp

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

Goal state before:
pp: case refine_1
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e ∈ dilatransvections K V ∧ e.fixedReduce = 1

Tactic:
constructor

Goal state after:
case refine_1.left
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e ∈ dilatransvections K V

case refine_1.right
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = 1
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
⊢ Q₁.polarBilin = Q₂.polarBilin

Tactic:
ext

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₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry Q₁.polarBilin) 1) x✝¹)) 1) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry Q₂.polarBilin) 1) x✝¹)) 1) x✝
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
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
hfv : f v = 0
⊢ (↑e).fixedSubmodule ≤ (↑e - LinearMap.transvection f v).ker ∧ e w - (LinearMap.transvection f v) w = 0

Tactic:
constructor

Goal state after:
case h.left
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 : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := ⋯
hfv : f v = 0
⊢ (↑e).fixedSubmodule ≤ (↑e - LinearMap.transvection f v).ker

case h.right
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 : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := ⋯
hfv : f v = 0
⊢ e w - (LinearMap.transvection f v) w = 0