Theorem: PolynomialMap.coeff_injective (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
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
⊢ f = g
Tactic:
ext S _ _ p
State after:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ f.toFun' S p = g.toFun' S p

State before:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ f.toFun' S p = g.toFun' S p
Tactic:
suffices hp : p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s) by
  simp only [Submodule.mem_span_iff_exists_sum _ p, TensorProduct.smul_tmul'] at hp
  obtain ⟨r, rfl⟩ := hp
  rw [Finsupp.sum_of_support_subset _ (subset_univ _) _ (fun  i _ => by
    rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul])]
  simp only [← toFun_eq_toFun'_apply, image_eq_coeff_sum, h]
State after:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)

State before:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)
Tactic:
rw [PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top ι m hm]
State after:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ ⊤

State before:
case toFun'.h.h.h.h
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ ⊤
Tactic:
exact Submodule.mem_top
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)
⊢ f.toFun' S p = g.toFun' S p
Tactic:
simp only [Submodule.mem_span_iff_exists_sum _ p, TensorProduct.smul_tmul'] at hp
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : ∃ a, (a.sum fun i c => (c • 1) ⊗ₜ[R] m i) = p
⊢ f.toFun' S p = g.toFun' S p

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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : ∃ a, (a.sum fun i c => (c • 1) ⊗ₜ[R] m i) = p
⊢ f.toFun' S p = g.toFun' S p
Tactic:
obtain ⟨r, rfl⟩ := hp
State after:
case intro
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i) = g.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i)

State before:
case intro
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i) = g.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i)
Tactic:
rw [Finsupp.sum_of_support_subset _ (subset_univ _) _ (fun  i _ => by
  rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul])]
State after:
case intro
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x) = g.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x)

State before:
case intro
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x) = g.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x)
Tactic:
simp only [← toFun_eq_toFun'_apply, image_eq_coeff_sum, h]
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✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
r : ι →₀ S
i : ι
x✝ : i ∈ univ
⊢ (0 • 1) ⊗ₜ[R] m i = 0
Tactic:
rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul]
State after:
no goals