Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s) = ⊤
Tactic:
rw [_root_.eq_top_iff]
State after:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
⊢ ⊤ ≤ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
⊢ ⊤ ≤ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
intro m h
State after:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
m : S ⊗[R] M
h : m ∈ ⊤
⊢ m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
m : S ⊗[R] M
h : m ∈ ⊤
⊢ m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
induction m using TensorProduct.induction_on with
| zero => exact zero_mem _
| tmul r m =>
    let f : M →ₗ[R] S ⊗[R] M :=
      { toFun     := fun m => (1 : S) ⊗ₜ[R] m
        map_add'  := fun x y => by simp only [TensorProduct.tmul_add]
        map_smul' := fun a x => by simp only [TensorProduct.tmul_smul, RingHom.id_apply] }
    suffices r ⊗ₜ[R] m = r • (1 : S) ⊗ₜ[R] m by
      rw [this]
      apply Submodule.smul_mem _ r _
      apply Submodule.span_le_restrictScalars R
      convert Submodule.apply_mem_span_image_of_mem_span (s := Set.range e) f _
      . conv_rhs => rw [← Set.image_univ, Set.image_image, Set.image_univ]
        rfl
      . rw [hm]; exact Submodule.mem_top
    rw [TensorProduct.smul_tmul']; simp only [Algebra.id.smul_eq_mul, _root_.mul_one]
| add x y hx hy => exact Submodule.add_mem _ (hx Submodule.mem_top) (hy Submodule.mem_top)
State after:
no goals

State before:
case zero
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
h : 0 ∈ ⊤
⊢ 0 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
exact zero_mem _
State after:
no goals

State before:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
⊢ r ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
let f : M →ₗ[R] S ⊗[R] M :=
  { toFun     := fun m => (1 : S) ⊗ₜ[R] m
    map_add'  := fun x y => by simp only [TensorProduct.tmul_add]
    map_smul' := fun a x => by simp only [TensorProduct.tmul_smul, RingHom.id_apply] }
State after:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
suffices r ⊗ₜ[R] m = r • (1 : S) ⊗ₜ[R] m by
  rw [this]
  apply Submodule.smul_mem _ r _
  apply Submodule.span_le_restrictScalars R
  convert Submodule.apply_mem_span_image_of_mem_span (s := Set.range e) f _
  . conv_rhs => rw [← Set.image_univ, Set.image_image, Set.image_univ]
    rfl
  . rw [hm]; exact Submodule.mem_top
State after:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m

State before:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
Tactic:
rw [TensorProduct.smul_tmul']
State after:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m = (r • 1) ⊗ₜ[R] m

State before:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ r ⊗ₜ[R] m = (r • 1) ⊗ₜ[R] m
Tactic:
simp only [Algebra.id.smul_eq_mul, _root_.mul_one]
State after:
no goals

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
x y : M
⊢ (fun m => 1 ⊗ₜ[R] m) (x + y) = (fun m => 1 ⊗ₜ[R] m) x + (fun m => 1 ⊗ₜ[R] m) y
Tactic:
simp only [TensorProduct.tmul_add]
State after:
no goals

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
a : R
x : M
⊢ { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯ }.toFun (a • x) =
    (RingHom.id R) a • { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯ }.toFun x
Tactic:
simp only [TensorProduct.tmul_smul, RingHom.id_apply]
State after:
no goals

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ r ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
rw [this]
State after:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ r • 1 ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ r • 1 ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
apply Submodule.smul_mem _ r _
State after:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] m ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
apply Submodule.span_le_restrictScalars R
State after:
case a
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] m ∈ Submodule.span R (Set.range fun s => 1 ⊗ₜ[R] e s)

State before:
case a
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] m ∈ Submodule.span R (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
convert Submodule.apply_mem_span_image_of_mem_span (s := Set.range e) f _
State after:
case h.e'_5.h.e'_6
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = ⇑f '' Set.range e

case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)

State before:
case h.e'_5.h.e'_6
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = ⇑f '' Set.range e

case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)
Tactic:
. conv_rhs => rw [← Set.image_univ, Set.image_image, Set.image_univ]
  rfl
State after:
case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)

State before:
case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)
Tactic:
. rw [hm]; exact Submodule.mem_top
State after:
no goals

State before:
case h.e'_5.h.e'_6
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = ⇑f '' Set.range e
Tactic:
conv_rhs => rw [← Set.image_univ, Set.image_image, Set.image_univ]
State after:
case h.e'_5.h.e'_6
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = Set.range fun x => f (e x)

State before:
case h.e'_5.h.e'_6
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = Set.range fun x => f (e x)
Tactic:
rfl
State after:
no goals

State before:
case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)
Tactic:
rw [hm]
State after:
case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ ⊤

State before:
case a.convert_2
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ ⊤
Tactic:
exact Submodule.mem_top
State after:
no goals

State before:
case add
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
x y : S ⊗[R] M
hx : x ∈ ⊤ → x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
hy : y ∈ ⊤ → y ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
h : x + y ∈ ⊤
⊢ x + y ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
exact Submodule.add_mem _ (hx Submodule.mem_top) (hy Submodule.mem_top)
State after:
no goals