mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : NonUnitalSubalgebra 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)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
hf j k hjk

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra 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)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = ((f k).comp (inclusion hjk)) ⟨x, hxj⟩
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
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
m✝ : M
⊢ (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m✝ = 1 ⊗ₜ[R] m✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
m✝ : M
⊢ (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m✝ = 1 ⊗ₜ[R] m✝
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
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

Tactic:
;

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

Tactic:
;

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
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✝

Tactic:
;

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
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✝

Tactic:
;

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
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✝

Tactic:
;

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

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
⊢ ↑(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)
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
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✝

Tactic:
;

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'
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✝

Tactic:
;

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'
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✝

Tactic:
;

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

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
⊢ ↑(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)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
z : A
⊢ z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)

Tactic:
;

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
z : A
⊢ z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)
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
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✝

Tactic:
;

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.Associator

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ rTensor Q (lTensor P x) ∘ₗ ↑(assoc R P M Q).symm = ↑(assoc R P N Q).symm ∘ₗ lTensor P (rTensor Q x)

Tactic:
simp_rw [rTensor, lTensor, map_map_comp_assoc_symm_eq]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
;

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨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
a✝ : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x ↦ x • m) ⋯ (𝒞.repr n)) a✝

Tactic:
;

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
a✝ : κ
x✝ : M
⊢ (↑(equivFinsuppOfBasisRight 𝒞).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i ↦ (mk R M N).flip (𝒞 i)) ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
;

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
a✝ : ι
x✝ : N
⊢ (↑(equivFinsuppOfBasisLeft ℬ).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i ↦ (mk R M N) (ℬ i)) ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
;

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.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
j : ι₁
n : M₁ j
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') j ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ j) M₂').flip n✝ ∘ₗ component S ι₁ M₁ j) ∘ₗ lof S ι₁ M₁ j) n

Tactic:
;

Goal state after:
case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
j : ι₁
n : M₁ j
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') j ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ j) M₂').flip n✝ ∘ₗ component S ι₁ M₁ j) ∘ₗ lof S ι₁ M₁ j) n
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
a✝ : ι
⊢ ((finsuppRight R S M N ι) (m ⊗ₜ[R] Finsupp.single i n)) a✝ = (Finsupp.single i (m ⊗ₜ[R] n)) a✝

Tactic:
;

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✝