Theorem: DividedPowerAlgebra.gamma_mem_grade (DividedPowers/DPAlgebra/PolynomialMap.lean)

State before:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (gamma R M n).toFun S 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dp_null]
State after:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (dpScalarExtensionEquiv R S M).symm (if n = 0 then 1 else 0) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (dpScalarExtensionEquiv R S M).symm (if n = 0 then 1 else 0) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
split_ifs with h
State after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

case neg
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : ¬n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rw [AlgEquiv.map_one, h]
State after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M 0).subtype)

State before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M 0).subtype)
Tactic:
simp only [LinearMap.mem_range]
State after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ ∃ y, (LinearMap.lTensor S (grade R M 0).subtype) y = 1

State before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ ∃ y, (LinearMap.lTensor S (grade R M 0).subtype) y = 1
Tactic:
use (1 : S) ⊗ₜ[R] ⟨(1 : DividedPowerAlgebra R M), one_mem R M⟩
State after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (LinearMap.lTensor S (grade R M 0).subtype) (1 ⊗ₜ[R] ⟨1, ⋯⟩) = 1

State before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (LinearMap.lTensor S (grade R M 0).subtype) (1 ⊗ₜ[R] ⟨1, ⋯⟩) = 1
Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype]
State after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ⊗ₜ[R] 1 = 1

State before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ⊗ₜ[R] 1 = 1
Tactic:
rw [Algebra.TensorProduct.one_def]
State after:
no goals

State before:
case neg
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : ¬n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [map_zero, zero_mem]
State after:
no goals

State before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (gamma R M n).toFun S (s ⊗ₜ[R] m) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv]
State after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (ofAlgHom (dpScalarExtension R S M) (dpScalarExtensionInv R S M) ⋯ ⋯).symm (dp S n (s ⊗ₜ[R] m)) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (ofAlgHom (dpScalarExtension R S M) (dpScalarExtensionInv R S M) ⋯ ⋯).symm (dp S n (s ⊗ₜ[R] m)) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [ofAlgHom_symm_apply]
State after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rw [dpScalarExtensionInv_apply_dp]
State after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (s ^ n) ⊗ₜ[R] dp R n m ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (s ^ n) ⊗ₜ[R] dp R n m ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [LinearMap.mem_range]
State after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ ∃ y, (LinearMap.lTensor S (grade R M n).subtype) y = (s ^ n) ⊗ₜ[R] dp R n m

State before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ ∃ y, (LinearMap.lTensor S (grade R M n).subtype) y = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
use (s ^ n) ⊗ₜ[R] ⟨dp R n m, dp_mem_grade R M n m⟩
State after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (LinearMap.lTensor S (grade R M n).subtype) ((s ^ n) ⊗ₜ[R] ⟨dp R n m, ⋯⟩) = (s ^ n) ⊗ₜ[R] dp R n m

State before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (LinearMap.lTensor S (grade R M n).subtype) ((s ^ n) ⊗ₜ[R] ⟨dp R n m, ⋯⟩) = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype]
State after:
no goals

State before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (gamma R M n).toFun S (x + y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv, ofAlgHom_symm_apply]
State after:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (x + y)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (x + y)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [dp_add, _root_.map_sum]
State after:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, (dpScalarExtensionInv R S M) (dp S x_1.1 x * dp S x_1.2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, (dpScalarExtensionInv R S M) (dp S x_1.1 x * dp S x_1.2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
apply Submodule.sum_mem
State after:
case add.a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∀ c ∈ Finset.antidiagonal n,
    (dpScalarExtensionInv R S M) (dp S c.1 x * dp S c.2 y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∀ c ∈ Finset.antidiagonal n,
    (dpScalarExtensionInv R S M) (dp S c.1 x * dp S c.2 y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rintro ⟨k, l⟩ hkl
State after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S (k, l).1 x * dp S (k, l).2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S (k, l).1 x * dp S (k, l).2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [_root_.map_mul]
State after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
specialize hx k
State after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
specialize hy l
State after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
hy : (gamma R M l).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M l).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
hy : (gamma R M l).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M l).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv, ofAlgHom_symm_apply, LinearMap.mem_range] at hx hy
State after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : ∃ y, (LinearMap.lTensor S (grade R M k).subtype) y = (dpScalarExtensionInv R S M) (dp S k x)
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : ∃ y, (LinearMap.lTensor S (grade R M k).subtype) y = (dpScalarExtensionInv R S M) (dp S k x)
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
obtain ⟨x', hx'⟩ := hx
State after:
case add.a.mk.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
obtain ⟨y', hy'⟩ := hy
State after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

State before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [LinearMap.mem_range]
State after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y_1,
    (LinearMap.lTensor S (grade R M n).subtype) y_1 =
      (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y)

State before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y_1,
    (LinearMap.lTensor S (grade R M n).subtype) y_1 =
      (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y)
Tactic:
rw [← hx', ← hy']
State after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y,
    (LinearMap.lTensor S (grade R M n).subtype) y =
      (LinearMap.lTensor S (grade R M k).subtype) x' * (LinearMap.lTensor S (grade R M l).subtype) y'

State before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y,
    (LinearMap.lTensor S (grade R M n).subtype) y =
      (LinearMap.lTensor S (grade R M k).subtype) x' * (LinearMap.lTensor S (grade R M l).subtype) y'
Tactic:
sorry
State after:
no goals