internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof 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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
d : ι →₀ ℕ
x✝ : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : ι, r i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d = 1 ⊗ₜ[R] ((∏ i : ι, r i ^ d i) • ((coeff fun x => m x) f) d)
Tactic:
rw [← TensorProduct.smul_tmul, smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
⊢ f.ground (r • m) = ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
suffices r • m = univ.sum fun i ↦ (const Unit r) i • (const Unit m i) by
  rw [this, ground_image_eq_coeff_sum]
  exact sum_congr rfl (fun i _ => by simp only [univ_unique, const_apply, prod_singleton]; rfl)
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
⊢ r • m = ∑ i : Unit, const Unit r i • const Unit m i
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
⊢ r • m = ∑ i : Unit, const Unit r i • const Unit m i
Tactic:
simp only [univ_unique, const_apply, sum_const, card_singleton, _root_.one_smul]
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ f.ground (r • m) = ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
rw [this, ground_image_eq_coeff_sum]
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ (((coeff fun i => const Unit m i) f).sum fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) =
    ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ (((coeff fun i => const Unit m i) f).sum fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) =
    ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
exact sum_congr rfl (fun i _ => by simp only [univ_unique, const_apply, prod_singleton]; rfl)
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ (fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) i (((coeff fun i => const Unit m i) f) i) =
    (fun k n => r ^ k 0 • n) i (((coeff (const Unit m)) f) i)
Tactic:
simp only [univ_unique, const_apply, prod_singleton]
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ r ^ i default • ((coeff fun i => m) f) i = r ^ i 0 • ((coeff (const Unit m)) f) i
Theorem: PolynomialMap.ground_image_eq_coeff_sum_one
Proof 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ r ^ i default • ((coeff fun i => m) f) i = r ^ i 0 • ((coeff (const Unit m)) f) i
Tactic:
rfl
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum_two
Proof 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 ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ f.ground (r₁ • m₁ + r₂ • m₂) =
    ((coeff ![m₁, m₂]) f).sum fun k n => (∏ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i ^ k i) • n
Tactic:
suffices r₁ • m₁ + r₂ • m₂ = univ.sum fun i ↦ (![r₁, r₂]) i • (![m₁, m₂]) i  by
  rw [this, ground_image_eq_coeff_sum]
Proof 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 ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i
Theorem: PolynomialMap.ground_image_eq_coeff_sum_two
Proof 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 ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i
Tactic:
simp
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum_two
Proof 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 ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
this : r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i
⊢ f.ground (r₁ • m₁ + r₂ • m₂) =
    ((coeff ![m₁, m₂]) f).sum fun k n => (∏ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i ^ k i) • n
Tactic:
rw [this, ground_image_eq_coeff_sum]
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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]
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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)
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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 _
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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] }
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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
Proof 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
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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']
Proof 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
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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]
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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 _
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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 _
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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
Proof 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)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof 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
Proof state after:
no goals