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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ (mk R M R).compr₂ₛₗ ((mk R M R).flip 1 ∘ₗ lift (LinearMap.lsmul R M).flip) = (mk R M R).compr₂ₛₗ LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
x✝ : M
⊢ (((mk R M R).compr₂ₛₗ ((mk R M R).flip 1 ∘ₗ lift (LinearMap.lsmul R M).flip)) x✝) 1 =
    (((mk R M R).compr₂ₛₗ LinearMap.id) x✝) 1
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (mk R M R).compr₂ₛₗ ↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) =
    (mk R M R).compr₂ₛₗ ↑(TensorProduct.rid R M)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ (((mk R M R).compr₂ₛₗ ↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M)) x✝) 1 =
    (((mk R M R).compr₂ₛₗ ↑(TensorProduct.rid R M)) x✝) 1
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (mk R R M).compr₂ₛₗ ↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) =
    (mk R R M).compr₂ₛₗ ↑(TensorProduct.lid R M)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ (((mk R R M).compr₂ₛₗ ↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M)) 1) x✝ =
    (((mk R R M).compr₂ₛₗ ↑(TensorProduct.lid R M)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
      lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((mk R N P).compr₂ₛₗ
          (((mk R M (N ⊗[R] P)).compr₂ₛₗ
              (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
                lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P))))
            x✝²))
        x✝¹)
      x✝ =
    (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ LinearMap.id) x✝²)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
      lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
                lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ↑(leftComm R M N P) =
    ↑((TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
        TensorProduct.assoc R N M P)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ ↑(leftComm R M N P)) x✝²)) x✝¹) x✝ =
    (((mk R N P).compr₂ₛₗ
          (((mk R M (N ⊗[R] P)).compr₂ₛₗ
              ↑((TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
                  TensorProduct.assoc R N M P))
            x✝²))
        x✝¹)
      x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
⊢ lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝² : M
x✝¹ : P
x✝ : N
⊢ ((((mk R M P).compr₂ₛₗ
            ((mk R (M ⊗[R] P) N).compr₂ₛₗ
              (lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M P).compr₂ₛₗ ((mk R (M ⊗[R] P) N).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
⊢ lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) =
    LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              (lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ↑(rightComm R M N P) =
    ↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
        (TensorProduct.assoc R M P N).symm)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ ↑(rightComm R M N P))) x✝²) x✝¹) x✝ =
    ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              ↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
                  (TensorProduct.assoc R M P N).symm)))
          x✝²)
        x✝¹)
      x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
⊢ (equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x ↦ x • m) ⋯ (𝒞.repr n)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
a✝ : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x ↦ x • m) ⋯ (𝒞.repr n)) a✝
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
⊢ ↑(equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun i ↦ (mk R M N).flip (𝒞 i)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
a✝ : κ
x✝ : M
⊢ (↑(equivFinsuppOfBasisRight 𝒞).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i ↦ (mk R M N).flip (𝒞 i)) ∘ₗ Finsupp.lsingle a✝) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
⊢ ↑(equivFinsuppOfBasisLeft ℬ).symm = (Finsupp.lsum R) fun i ↦ (mk R M N) (ℬ i)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
a✝ : ι
x✝ : N
⊢ (↑(equivFinsuppOfBasisLeft ℬ).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i ↦ (mk R M N) (ℬ i)) ∘ₗ Finsupp.lsingle a✝) x✝
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y : N
⊢ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (x + y)))) =
    mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))) +
      mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm y)))

Tactic:
ext

Goal state after:
R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y a✝ : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (x + y))))) a✝ =
    (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))) +
        mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm y))))
      a✝
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
m : M
n : N
⊢ (finsuppRight R S M N ι) (m ⊗ₜ[R] Finsupp.single i n) = Finsupp.single i (m ⊗ₜ[R] n)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
m : M
n : N
a✝ : ι
⊢ ((finsuppRight R S M N ι) (m ⊗ₜ[R] Finsupp.single i n)) a✝ = (Finsupp.single i (m ⊗ₜ[R] n)) a✝
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
⊢ ↑R (linearCombination S fun x ↦ 1 ⊗ₜ[R] v x) = lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
a✝ : ι
x✝ : S
⊢ (↑R (linearCombination S fun x ↦ 1 ⊗ₜ[R] v x) ∘ₗ lsingle a✝) x✝ =
    ((lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm) ∘ₗ lsingle a✝) x✝
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id =
    LinearMap.id

Tactic:
ext

Goal state after:
case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
x✝ : M
a✝ : N
⊢ ((AlgebraTensorModule.curry
            (AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id))
          x✝ ∘ₗ
        lsingle a✝)
      1 =
    ((AlgebraTensorModule.curry LinearMap.id) x✝ ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
⊢ ↑(directSumRight R R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f =
    (lmap fun x ↦ rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R R M₁' M₁)

Tactic:
ext

Goal state after:
R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
x✝¹ : M₁'
i✝¹ : ι₁
x✝ : M₁ i✝¹
i✝ : ι₁
⊢ (((AlgebraTensorModule.curry (↑(directSumRight R R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f)) x✝¹ ∘ₗ lof R ι₁ M₁ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ((lmap fun x ↦ rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R R M₁' M₁))) x✝¹ ∘ₗ
          lof R ι₁ M₁ i✝¹)
        x✝)
      i✝
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN =
    LinearMap.id

Tactic:
ext

Goal state after:
case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
⊢ (comp I I J J R) 1 = 1

Tactic:
ext

Goal state after:
I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
i✝ j✝ : I × J
⊢ (comp I I J J R) 1 i✝ j✝ = 1 i✝ j✝
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype I
inst✝ : Fintype J
x✝¹ x✝ : Matrix I I (Matrix J J R)
⊢ (compAddEquiv I I J J R).toFun (x✝¹ * x✝) = (compAddEquiv I I J J R).toFun x✝¹ * (compAddEquiv I I J J R).toFun x✝

Tactic:
ext

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype I
inst✝ : Fintype J
x✝¹ x✝ : Matrix I I (Matrix J J R)
i✝ j✝ : I × J
⊢ (compAddEquiv I I J J R).toFun (x✝¹ * x✝) i✝ j✝ =
    ((compAddEquiv I I J J R).toFun x✝¹ * (compAddEquiv I I J J R).toFun x✝) i✝ j✝