mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (b • f) g = b • map f g

Tactic:
ext

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]

Tactic:
ext i j
  fin_cases i <;> fin_cases j <;> rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
      lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ((curry
          ((curry
              (lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
                lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q))))
            x✝²))
        x✝¹)
      x✝ =
    ((curry ((curry LinearMap.id) x✝²)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
      lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
                lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
⊢ (lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N) = ↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f)

Tactic:
ext

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : Q
x✝ : P
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
⊢ baseChange A (f + g) = baseChange A f + baseChange A g

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ baseChange A 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A 0)) 1) x✝ = ((AlgebraTensorModule.curry 0) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
⊢ baseChange A (r • f) = r • baseChange A f

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (r • f))) 1) x✝ = ((AlgebraTensorModule.curry (r • baseChange A f)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A id = id

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ((AlgebraTensorModule.curry id) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ baseChange A (g ∘ₗ f) = baseChange A g ∘ₗ baseChange A f

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_7
B : Type u_8
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : M →ₗ[R] N
⊢ baseChange B (baseChange A f) = ↑(cancelBaseChange R A B B N).symm ∘ₗ baseChange B f ∘ₗ ↑(cancelBaseChange R A B B M)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_7
B : Type u_8
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (baseChange B (baseChange A f))) 1)) 1) x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              (↑(cancelBaseChange R A B B N).symm ∘ₗ baseChange B f ∘ₗ ↑(cancelBaseChange R A B B M)))
            1))
        1)
      x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
⊢ baseChange A (f * g) = baseChange A f * baseChange A g

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f * g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f * baseChange A g)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : M →ₗ[R] N
⊢ baseChange A (f - g) = baseChange A f - baseChange A g

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f - g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f - baseChange A g)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ baseChange A (-f) = -baseChange A f

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (-f))) 1) x✝ = ((AlgebraTensorModule.curry (-baseChange A f)) 1) x✝
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ (↑sd * ↑sc * sb) • r₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂ ∧
    ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
constructor

Goal state after:
case h.left
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ (↑sd * ↑sc * sb) • r₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂

case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
⊢ f.fieldRange = Subfield.map f ⊤

Tactic:
ext

Goal state after:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x✝ : L
⊢ x✝ ∈ f.fieldRange ↔ x✝ ∈ Subfield.map f ⊤
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ toLinearMapRight' 1 = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
i✝ x✝ : m
⊢ (toLinearMapRight' 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝ =
    (LinearMap.id ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype m
M : Matrix m n R
⊢ Mᵀ.mulVecLin = M.vecMulLinear

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype m
M : Matrix m n R
x✝¹ : m → R
x✝ : n
⊢ Mᵀ.mulVecLin x✝¹ x✝ = M.vecMulLinear x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ Mᵀ.vecMulLinear = M.mulVecLin

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
x✝¹ : n → R
x✝ : m
⊢ Mᵀ.vecMulLinear x✝¹ x✝ = M.mulVecLin x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ mulVecLin 1 = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ (mulVecLin 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝ = (LinearMap.id ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
c : R
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ of (fun i j ↦ (c • f) (Pi.single j 1) i) i j = ((RingHom.id R) c • of fun i j ↦ f (Pi.single j 1) i) i j

Tactic:
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ toMatrix' id = 1

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = 1 i✝ j✝
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ sa * s₁ = ⟨ra * ↑s₂, ⋯⟩

Tactic:
ext

Goal state after:
case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ↑(sa * s₁) = ↑⟨ra * ↑s₂, ⋯⟩
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ sc * (sa * s₁) = ⟨rc * ↑s₃, ⋯⟩

Tactic:
ext

Goal state after:
case e_s
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ↑(sc * (sa * s₁)) = ↑⟨rc * ↑s₃, ⋯⟩