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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
⊢ (map (↑f) M).mulMap (map (↑f) N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N) = ↑f ∘ₗ M.mulMap N

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
x✝¹ : ↥M
x✝ : ↥N
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((map (↑f) M).mulMap (map (↑f) N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (↑f ∘ₗ M.mulMap N)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N) 1 = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
x✝ : ↥N
⊢ ↑((N.lTensorOne' ∘ₗ (TensorProduct.mk R ↥⊥ ↥N) 1) x✝) = ↑(LinearMap.id x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ M.rTensorOne' ∘ₗ ↑(TensorProduct.comm R ↥⊥ ↥M) ∘ₗ (TensorProduct.mk R ↥⊥ ↥M) 1 = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
x✝ : ↥M
⊢ ↑((M.rTensorOne' ∘ₗ ↑(TensorProduct.comm R ↥⊥ ↥M) ∘ₗ (TensorProduct.mk R ↥⊥ ↥M) 1) x✝) = ↑(LinearMap.id x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
⊢ mulLeftMap N m =
    M.mulMap N ∘ₗ
      LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
a✝ : ι
x✝ : ↥N
⊢ (mulLeftMap N m ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
⊢ M.mulRightMap n =
    M.mulMap N ∘ₗ
      LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
a✝ : ι
x✝ : ↥M
⊢ (M.mulRightMap n ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
            ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective ⇑i
⊢ i = M'.mulMap N

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)
hi : Function.Injective ⇑i
x✝¹ : ↥M'
x✝ : ↥N
⊢ ((TensorProduct.AlgebraTensorModule.curry i) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (M'.mulMap N)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective ⇑i
⊢ i = M.mulMap N'

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)
hi : Function.Injective ⇑i
x✝¹ : ↥M
x✝ : ↥N'
⊢ ((TensorProduct.AlgebraTensorModule.curry i) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (M.mulMap N')) x✝¹) x✝
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case e'_4
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ⇑((TensorProduct.mk R k M) 1) ∘ (v + fun x ↦ c x • v ↑n) =
    ⇑((TensorProduct.mk R k M) 1) ∘ v + fun x ↦ (⇑(Ideal.Quotient.mk 𝔪) ∘ c) x • (⇑((TensorProduct.mk R k M) 1) ∘ v) ↑n

Tactic:
ext

Goal state after:
case e'_4
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
x✝ : ι
⊢ (⇑((TensorProduct.mk R k M) 1) ∘ (v + fun x ↦ c x • v ↑n)) x✝ =
    (⇑((TensorProduct.mk R k M) 1) ∘ v + fun x ↦
        (⇑(Ideal.Quotient.mk 𝔪) ∘ c) x • (⇑((TensorProduct.mk R k M) 1) ∘ v) ↑n)
      x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : MultilinearMap R s E
⊢ (let __src := liftAux (φ₁ + φ₂);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    (let __src := liftAux φ₁;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) +
      let __src := liftAux φ₂;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ((let __src := liftAux (φ₁ + φ₂);
          { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      x✝ =
    (((let __src := liftAux φ₁;
            { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) +
            let __src := liftAux φ₂;
            { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
r : R
φ₂ : MultilinearMap R s E
⊢ (let __src := liftAux (r • φ₂);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    (RingHom.id R) r •
      let __src := liftAux φ₂;
      { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
r : R
φ₂ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ((let __src := liftAux (r • φ₂);
          { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      x✝ =
    (((RingHom.id R) r •
            let __src := liftAux φ₂;
            { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ (fun φ' ↦ φ'.compMultilinearMap (tprod R))
      ((fun φ ↦
          let __src := liftAux φ;
          { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
        φ) =
    φ

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ((fun φ' ↦ φ'.compMultilinearMap (tprod R))
        ((fun φ ↦
            let __src := liftAux φ;
            { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
          φ))
      x✝ =
    φ x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : (⨂[R] (i : ι), s i) →ₗ[R] E
⊢ (fun φ ↦
        let __src := liftAux φ;
        { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
      ((fun φ' ↦ φ'.compMultilinearMap (tprod R)) φ) =
    φ

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : (⨂[R] (i : ι), s i) →ₗ[R] E
x✝ : (i : ι) → s i
⊢ (((fun φ ↦
              let __src := liftAux φ;
              { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
            ((fun φ' ↦ φ'.compMultilinearMap (tprod R)) φ)).compMultilinearMap
        (tprod R))
      x✝ =
    (φ.compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this :
  GradedMonoid.GMul.mul (algebraMap₀ r) x.snd =
    (cast R M ⋯) ((cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r)))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd

Tactic:
cast_cast

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this : GradedMonoid.GMul.mul (algebraMap₀ r) x.snd = (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
⊢ (map fun i ↦ g i ∘ₗ f i) = map g ∘ₗ map f

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((map fun i ↦ g i ∘ₗ f i).compMultilinearMap (tprod R)) x✝ = ((map g ∘ₗ map f).compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
⊢ lift h ∘ₗ map f = lift (h.compLinearMap f)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
x✝ : (i : ι) → s i
⊢ ((lift h ∘ₗ map f).compMultilinearMap (tprod R)) x✝ = ((lift (h.compLinearMap f)).compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ (map fun i ↦ LinearMap.id) = LinearMap.id

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ ((map fun i ↦ LinearMap.id).compMultilinearMap (tprod R)) x✝ = (LinearMap.id.compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ piTensorHomMap ((tprod R) f) = map f

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((piTensorHomMap ((tprod R) f)).compMultilinearMap (tprod R)) x✝ = ((map f).compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f✝ : (i : ι) → s i →ₗ[R] t i
f : (i : ι) → s i ≃ₗ[R] t i
⊢ ((map fun i ↦ ↑(f i)) ∘ₗ map fun i ↦ ↑(f i).symm) = LinearMap.id

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f✝ : (i : ι) → s i →ₗ[R] t i
f : (i : ι) → s i ≃ₗ[R] t i
x✝ : (i : ι) → t i
⊢ (((map fun i ↦ ↑(f i)) ∘ₗ map fun i ↦ ↑(f i).symm).compMultilinearMap (tprod R)) x✝ =
    (LinearMap.id.compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f✝ : (i : ι) → s i →ₗ[R] t i
f : (i : ι) → s i ≃ₗ[R] t i
⊢ ((map fun i ↦ ↑(f i).symm) ∘ₗ map fun i ↦ ↑(f i)) = LinearMap.id

Tactic:
ext

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f✝ : (i : ι) → s i →ₗ[R] t i
f : (i : ι) → s i ≃ₗ[R] t i
x✝ : (i : ι) → s i
⊢ (((map fun i ↦ ↑(f i).symm) ∘ₗ map fun i ↦ ↑(f i)).compMultilinearMap (tprod R)) x✝ =
    (LinearMap.id.compMultilinearMap (tprod R)) x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ))) =
    lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
      lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
                  lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))).compMultilinearMap
              (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
r : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ))) =
    r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
r : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝