[GOAL]
⊢ StableUnderComposition @Finite
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Finite f
hg : Finite g
⊢ Finite (comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ RespectsIso @Finite
[PROOFSTEP]
apply finite_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Finite (RingEquiv.toRingHom e)
[PROOFSTEP]
intros
[GOAL]
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ Finite (RingEquiv.toRingHom e✝)
[PROOFSTEP]
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective
[GOAL]
⊢ StableUnderBaseChange @Finite
[PROOFSTEP]
refine StableUnderBaseChange.mk _ finite_respectsIso ?_
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Finite (algebraMap R T) → Finite includeLeftRingHom
[PROOFSTEP]
classical
introv h
replace h : Module.Finite R T := by rw [RingHom.Finite] at h ; convert h; ext; intros; simp_rw [Algebra.smul_def]; rfl
suffices Module.Finite S (S ⊗[R] T) by rw [RingHom.Finite]; convert this; congr; ext; intros;
  simp_rw [Algebra.smul_def]; rfl
exact inferInstance
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Finite (algebraMap R T) → Finite includeLeftRingHom
[PROOFSTEP]
introv h
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Finite (algebraMap R T)
⊢ Finite includeLeftRingHom
[PROOFSTEP]
replace h : Module.Finite R T := by rw [RingHom.Finite] at h ; convert h; ext; intros; simp_rw [Algebra.smul_def]; rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Finite (algebraMap R T)
⊢ Module.Finite R T
[PROOFSTEP]
rw [RingHom.Finite] at h
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Module.Finite R T
[PROOFSTEP]
convert h
[GOAL]
case h.e'_5.h.e'_5
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ inst✝ = toAlgebra (algebraMap R T)
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
intros
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ ↑(algebraMap R T) r✝ * x✝ = r✝ • x✝
[PROOFSTEP]
rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Finite includeLeftRingHom
[PROOFSTEP]
suffices Module.Finite S (S ⊗[R] T) by rw [RingHom.Finite]; convert this; congr; ext; intros;
  simp_rw [Algebra.smul_def]; rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
⊢ Finite includeLeftRingHom
[PROOFSTEP]
rw [RingHom.Finite]
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
⊢ Module.Finite S (S ⊗[R] T)
[PROOFSTEP]
convert this
[GOAL]
case h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
⊢ Algebra.toModule = leftModule
[PROOFSTEP]
congr
[GOAL]
case h.e'_5.h.h.e_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
⊢ toAlgebra includeLeftRingHom = leftAlgebra
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := toAlgebra includeLeftRingHom;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
intros
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := toAlgebra includeLeftRingHom;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ r✝ • x✝ = ↑(algebraMap S (S ⊗[R] T)) r✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Module.Finite S (S ⊗[R] T)
[PROOFSTEP]
exact inferInstance


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
⊢ ↑(aeval x) (↑(map (algebraMap R A)) p) = ↑(aeval x) p
[PROOFSTEP]
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = ↑(algebraMap A B) (↑(aeval x) p)
[PROOFSTEP]
rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ← IsScalarTower.algebraMap_eq]
  -- Porting note: added
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R B) (↑(algebraMap A B) ∘ x)) p =
    ↑(eval₂Hom (algebraMap R B) fun i => ↑(algebraMap A B) (x i)) p
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero, iff_false_intro (one_ne_zero' B),
  or_false_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ↑(algebraMap A B)
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : σ → { x // x ∈ S }
p : MvPolynomial σ R
⊢ ↑(aeval fun i => ↑(x i)) p = ↑(↑(aeval x) p)
[PROOFSTEP]
convert aeval_algebraMap_apply A x p


[GOAL]
⊢ StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective ↑f
hg : Function.Surjective ↑g
⊢ Function.Surjective ↑(comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
apply surjective_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective ↑(RingEquiv.toRingHom e)
[PROOFSTEP]
intros _ _ _ _ e
[GOAL]
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ Function.Surjective ↑(RingEquiv.toRingHom e)
[PROOFSTEP]
exact e.surjective
[GOAL]
⊢ StableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
refine' StableUnderBaseChange.mk _ surjective_respectsIso _
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ↑(algebraMap R T) → Function.Surjective ↑includeLeftRingHom
[PROOFSTEP]
classical
introv h x
skip
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ↑(algebraMap R T) → Function.Surjective ↑includeLeftRingHom
[PROOFSTEP]
introv h x
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
skip
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
case zero
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
⊢ ∃ a, ↑includeLeftRingHom a = 0
[PROOFSTEP]

| zero => exact ⟨0, map_zero _⟩
[GOAL]
case zero
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
⊢ ∃ a, ↑includeLeftRingHom a = 0
[PROOFSTEP]
exact ⟨0, map_zero _⟩
[GOAL]
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : T
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] y
[PROOFSTEP]

| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
[GOAL]
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : T
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] y
[PROOFSTEP]
obtain ⟨y, rfl⟩ := h y
[GOAL]
case tmul.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
use y • x
[GOAL]
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ ↑includeLeftRingHom (y • x) = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
dsimp
[GOAL]
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
[GOAL]
case add
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S ⊗[R] T
ex : ∃ a, ↑includeLeftRingHom a = x
ey : ∃ a, ↑includeLeftRingHom a = y
⊢ ∃ a, ↑includeLeftRingHom a = x + y
[PROOFSTEP]

| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
case add
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S ⊗[R] T
ex : ∃ a, ↑includeLeftRingHom a = x
ey : ∃ a, ↑includeLeftRingHom a = y
⊢ ∃ a, ↑includeLeftRingHom a = x + y
[PROOFSTEP]
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey
[GOAL]
case add.intro.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S
⊢ ∃ a, ↑includeLeftRingHom a = ↑includeLeftRingHom x + ↑includeLeftRingHom y
[PROOFSTEP]
exact ⟨x + y, map_add _ x y⟩
[GOAL]
⊢ OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
introv R hs H
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ↑f
[PROOFSTEP]
skip
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ↑f
[PROOFSTEP]
letI := f.toAlgebra
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ Function.Surjective ↑f
[PROOFSTEP]
show Function.Surjective (Algebra.ofId R S)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ Function.Surjective ↑(Algebra.ofId R S)
[PROOFSTEP]
rw [← Algebra.range_top_iff_surjective, eq_top_iff]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ ⊤ ≤ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
rintro x -
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_total R s 1).mp (show _ ∈ Ideal.span s by rw [hs]; trivial)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ 1 ∈ Ideal.span s
[PROOFSTEP]
rw [hs]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
fapply Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem _ l.support (fun x : s => f x) fun x : s => f (l x)
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∑ i in l.support, ↑f (↑l i) * ↑f ↑i = 1
[PROOFSTEP]
dsimp only
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∑ i in l.support, ↑f (↑l i) * ↑f ↑i = 1
[PROOFSTEP]
simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one]
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ↑f (∑ x in l.support, ↑l x * ↑x) = ↑f 1
[PROOFSTEP]
exact f.congr_arg hl
[GOAL]
case intro.hs
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ↑f ↑i ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact fun _ => Set.mem_range_self _
[GOAL]
case intro.hl
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ↑f (↑l i) ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact fun _ => Set.mem_range_self _
[GOAL]
case intro.H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ∃ n, ↑f ↑i ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
intro r
[GOAL]
case intro.H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨y, hy⟩ := H r (IsLocalization.mk' _ x (1 : Submonoid.powers (f r)))
[GOAL]
case intro.H.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
y : Localization.Away ↑r
hy : ↑(Localization.awayMap f ↑r) y = IsLocalization.mk' (Localization.Away (↑f ↑r)) x 1
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨z, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) y
[GOAL]
case intro.H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n : ℕ
hy :
  ↑(Localization.awayMap f ↑r)
      (IsLocalization.mk' (Localization.Away ↑r) z
        { val := (fun x x_1 => x ^ x_1) (↑r) n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) }) =
    IsLocalization.mk' (Localization.Away (↑f ↑r)) x 1
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
erw [IsLocalization.map_mk', IsLocalization.eq] at hy
[GOAL]
case intro.H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n : ℕ
hy :
  ∃ c,
    ↑c * (↑1 * ↑f z) =
      ↑c *
        (↑{
              val :=
                ↑f
                  ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
              property :=
                (_ :
                  ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                        property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                    Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
          x)
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨⟨_, m, rfl⟩, hm⟩ := hy
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑1 * ↑f z) =
    ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑{
            val :=
              ↑f
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                    property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
            property :=
              (_ :
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                  Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
        x)
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
refine' ⟨m + n, _⟩
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑1 * ↑f z) =
    ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑{
            val :=
              ↑f
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                    property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
            property :=
              (_ :
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                  Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
        x)
⊢ ↑f ↑r ^ (m + n) • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
dsimp at hm ⊢
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm : ↑f ↑r ^ m * (1 * ↑f z) = ↑f ↑r ^ m * (↑f (↑r ^ n) * x)
⊢ ↑f ↑r ^ (m + n) * x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
simp_rw [_root_.one_mul, ← _root_.mul_assoc, ← map_pow, ← f.map_mul, ← pow_add, map_pow] at hm
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm : ↑f (↑r ^ m * z) = ↑f ↑r ^ (m + n) * x
⊢ ↑f ↑r ^ (m + n) * x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact ⟨_, hm⟩


[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c (a + b) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
rw [coeff_add] at hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
obtain h | h : coeff c a ≠ 0 ∨ coeff c b ≠ 0 := by
  contrapose! hc
  simp only [hc, add_zero]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
⊢ coeff c a ≠ 0 ∨ coeff c b ≠ 0
[PROOFSTEP]
contrapose! hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c a = 0 ∧ coeff c b = 0
⊢ coeff c a + coeff c b = 0
[PROOFSTEP]
simp only [hc, add_zero]
[GOAL]
case inl
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c a ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
exact ha h
[GOAL]
case inr
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : a ∈ {x | IsHomogeneous x n}
hb : b ∈ {x | IsHomogeneous x n}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
exact hb h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : coeff c (r • a) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
rw [coeff_smul] at hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
apply ha
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
⊢ coeff c a ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
⊢ False
[PROOFSTEP]
apply hc
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
⊢ r • coeff c a = 0
[PROOFSTEP]
rw [h]
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha :
  a ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | IsHomogeneous x n},
              add_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ {x | IsHomogeneous x n} →
                      b ∈ {x | IsHomogeneous x n} → ∀ (c : σ →₀ ℕ), coeff c (a + b) ≠ 0 → ∑ i in c.support, ↑c i = n) },
          zero_mem' := (_ : ∀ (d : σ →₀ ℕ), coeff d 0 ≠ 0 → ∑ i in d.support, ↑d i = n) }.toAddSubsemigroup.carrier
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
h : coeff c a = 0
⊢ r • 0 = 0
[PROOFSTEP]
exact smul_zero r
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = Finsupp.supported R R {d | ∑ i in d.support, ↑d i = n}
[PROOFSTEP]
ext
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ x✝ ∈ Finsupp.supported R R {d | ∑ i in d.support, ↑d i = n}
[PROOFSTEP]
rw [Finsupp.mem_supported, Set.subset_def]
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), x ∈ ↑x✝.support → x ∈ {d | ∑ i in d.support, ↑d i = n}
[PROOFSTEP]
simp only [Finsupp.mem_support_iff, Finset.mem_coe]
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), ↑x✝ x ≠ 0 → x ∈ {d | ∑ x in d.support, ↑d x = n}
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
⊢ homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n)
[PROOFSTEP]
rw [Submodule.mul_le]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
⊢ ∀ (m_1 : MvPolynomial σ R),
    m_1 ∈ homogeneousSubmodule σ R m →
      ∀ (n_1 : MvPolynomial σ R), n_1 ∈ homogeneousSubmodule σ R n → m_1 * n_1 ∈ homogeneousSubmodule σ R (m + n)
[PROOFSTEP]
intro φ hφ ψ hψ c hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
classical
rw [coeff_mul] at hc
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
  contrapose! H
  by_cases h : coeff d φ = 0 <;> simp_all only [Ne.def, not_false_iff, zero_mul, mul_zero]
specialize hφ aux.1
specialize hψ aux.2
rw [Finsupp.mem_antidiagonal] at hde
classical
have hd' : d.support ⊆ d.support ∪ e.support := Finset.subset_union_left _ _
have he' : e.support ⊆ d.support ∪ e.support := Finset.subset_union_right _ _
rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd', Finset.sum_subset he', ←
  Finset.sum_add_distrib]
· congr
all_goals intro i hi; apply Finsupp.not_mem_support_iff.mp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
rw [coeff_mul] at hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
  contrapose! H
  by_cases h : coeff d φ = 0 <;> simp_all only [Ne.def, not_false_iff, zero_mul, mul_zero]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
[PROOFSTEP]
contrapose! H
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
⊢ coeff d φ * coeff e ψ = 0
[PROOFSTEP]
by_cases h : coeff d φ = 0
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
h : coeff d φ = 0
⊢ coeff d φ * coeff e ψ = 0
[PROOFSTEP]
simp_all only [Ne.def, not_false_iff, zero_mul, mul_zero]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
h : ¬coeff d φ = 0
⊢ coeff d φ * coeff e ψ = 0
[PROOFSTEP]
simp_all only [Ne.def, not_false_iff, zero_mul, mul_zero]
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ : MvPolynomial σ R
hφ : φ ∈ homogeneousSubmodule σ R m
ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
specialize hφ aux.1
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
hψ : ψ ∈ homogeneousSubmodule σ R n
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
specialize hψ aux.2
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ Finsupp.antidiagonal c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
rw [Finsupp.mem_antidiagonal] at hde
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
classical
have hd' : d.support ⊆ d.support ∪ e.support := Finset.subset_union_left _ _
have he' : e.support ⊆ d.support ∪ e.support := Finset.subset_union_right _ _
rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd', Finset.sum_subset he', ←
  Finset.sum_add_distrib]
· congr
all_goals intro i hi; apply Finsupp.not_mem_support_iff.mp
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
have hd' : d.support ⊆ d.support ∪ e.support := Finset.subset_union_left _ _
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
have he' : e.support ⊆ d.support ∪ e.support := Finset.subset_union_right _ _
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ i in c.support, ↑c i = m + n
[PROOFSTEP]
rw [← hde, ← hφ, ← hψ, Finset.sum_subset Finsupp.support_add, Finset.sum_subset hd', Finset.sum_subset he', ←
  Finset.sum_add_distrib]
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∑ x in (d, e).fst.support ∪ (d, e).snd.support, ↑((d, e).fst + (d, e).snd) x =
    ∑ x in d.support ∪ e.support, (↑d x + ↑e x)
[PROOFSTEP]
congr
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ e.support → ↑e x = 0
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ d.support → ↑d x = 0
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ),
    x ∈ (d, e).fst.support ∪ (d, e).snd.support →
      ¬x ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) x = 0
[PROOFSTEP]
all_goals intro i hi; apply Finsupp.not_mem_support_iff.mp
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ e.support → ↑e x = 0
[PROOFSTEP]
intro i hi
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
i : σ
hi : i ∈ d.support ∪ e.support
⊢ ¬i ∈ e.support → ↑e i = 0
[PROOFSTEP]
apply Finsupp.not_mem_support_iff.mp
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ), x ∈ d.support ∪ e.support → ¬x ∈ d.support → ↑d x = 0
[PROOFSTEP]
intro i hi
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
i : σ
hi : i ∈ d.support ∪ e.support
⊢ ¬i ∈ d.support → ↑d i = 0
[PROOFSTEP]
apply Finsupp.not_mem_support_iff.mp
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
⊢ ∀ (x : σ),
    x ∈ (d, e).fst.support ∪ (d, e).snd.support →
      ¬x ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) x = 0
[PROOFSTEP]
intro i hi
[GOAL]
case intro.mk.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
m n : ℕ
φ ψ : MvPolynomial σ R
c : σ →₀ ℕ
hc✝ : coeff c (φ * ψ) ≠ 0
hc : ∑ x in Finsupp.antidiagonal c, coeff x.fst φ * coeff x.snd ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e).fst + (d, e).snd = c
H : coeff (d, e).fst φ * coeff (d, e).snd ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
hφ : ∑ i in d.support, ↑d i = m
hψ : ∑ i in e.support, ↑e i = n
hd' : d.support ⊆ d.support ∪ e.support
he' : e.support ⊆ d.support ∪ e.support
i : σ
hi : i ∈ (d, e).fst.support ∪ (d, e).snd.support
⊢ ¬i ∈ ((d, e).fst + (d, e).snd).support → ↑((d, e).fst + (d, e).snd) i = 0
[PROOFSTEP]
apply Finsupp.not_mem_support_iff.mp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
⊢ IsHomogeneous (↑(monomial d) r) n
[PROOFSTEP]
intro c hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
classical
rw [coeff_monomial] at hc
split_ifs at hc  with h
· subst c
  exact hn
· contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
rw [coeff_monomial] at hc
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
hc : (if d = c then r else 0) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
split_ifs at hc  with h
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : d = c
hc : r ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
subst c
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
hc✝ : r ≠ 0
hc : coeff d (↑(monomial d) r) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
[PROOFSTEP]
exact hn
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : ¬d = c
hc : 0 ≠ 0
⊢ ∑ i in c.support, ↑c i = n
[PROOFSTEP]
contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : totalDegree p = 0
⊢ IsHomogeneous p 0
[PROOFSTEP]
erw [totalDegree, Finset.sup_eq_bot_iff] at hp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : ∀ (s : σ →₀ ℕ), s ∈ support p → (Finsupp.sum s fun x e => e) = ⊥
⊢ IsHomogeneous p 0
[PROOFSTEP]
simp_rw [mem_support_iff] at hp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : ∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → (Finsupp.sum s fun x e => e) = ⊥
⊢ IsHomogeneous p 0
[PROOFSTEP]
exact hp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
r : R
⊢ IsHomogeneous (↑C r) 0
[PROOFSTEP]
apply isHomogeneous_monomial
[GOAL]
case hn
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
r : R
⊢ ∑ i in 0.support, ↑0 i = 0
[PROOFSTEP]
simp only [Finsupp.zero_apply, Finset.sum_const_zero]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
i : σ
⊢ IsHomogeneous (X i) 1
[PROOFSTEP]
apply isHomogeneous_monomial
[GOAL]
case hn
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
i : σ
⊢ ∑ i_1 in (Finsupp.single i 1).support, ↑(Finsupp.single i 1) i_1 = 1
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton]
[GOAL]
case hn
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
i : σ
⊢ ↑(Finsupp.single i 1) i = 1
[PROOFSTEP]
exact Finsupp.single_eq_same
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
⊢ coeff d φ = 0
[PROOFSTEP]
have aux := mt (@hφ d) hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
[PROOFSTEP]
classical rwa [Classical.not_not] at aux
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
[PROOFSTEP]
rwa [Classical.not_not] at aux
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hm : IsHomogeneous φ m
hn : IsHomogeneous φ n
hφ : φ ≠ 0
⊢ m = n
[PROOFSTEP]
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
[GOAL]
case intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hm : IsHomogeneous φ m
hn : IsHomogeneous φ n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
[PROOFSTEP]
rw [← hm hd, ← hn hd]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
[PROOFSTEP]
classical
revert h
refine' Finset.induction_on s _ _
· intro
  simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
· intro i s his IH h
  simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
  apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
  intro j hjs
  exact h j (Finset.mem_insert_of_mem hjs)
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
[PROOFSTEP]
revert h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
[PROOFSTEP]
refine' Finset.induction_on s _ _
[GOAL]
case refine'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)
[PROOFSTEP]
intro
[GOAL]
case refine'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h✝ : ∀ (i : ι), i ∈ ∅ → IsHomogeneous (φ i) (n i)
⊢ IsHomogeneous (∏ i in ∅, φ i) (∑ i in ∅, n i)
[PROOFSTEP]
simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
[GOAL]
case refine'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)) →
        (∀ (i : ι), i ∈ insert a s → IsHomogeneous (φ i) (n i)) →
          IsHomogeneous (∏ i in insert a s, φ i) (∑ i in insert a s, n i)
[PROOFSTEP]
intro i s his IH h
[GOAL]
case refine'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (∏ i in insert i s, φ i) (∑ i in insert i s, n i)
[PROOFSTEP]
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
[GOAL]
case refine'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ IsHomogeneous (φ i * ∏ i in s, φ i) (n i + ∑ i in s, n i)
[PROOFSTEP]
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
⊢ ∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)
[PROOFSTEP]
intro j hjs
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ✝ ψ : MvPolynomial σ R
m n✝ : ℕ
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : ¬i ∈ s
IH : (∀ (i : ι), i ∈ s → IsHomogeneous (φ i) (n i)) → IsHomogeneous (∏ i in s, φ i) (∑ i in s, n i)
h : ∀ (i_1 : ι), i_1 ∈ insert i s → IsHomogeneous (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsHomogeneous (φ j) (n j)
[PROOFSTEP]
exact h j (Finset.mem_insert_of_mem hjs)
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ MvPolynomial.totalDegree φ = n
[PROOFSTEP]
rw [totalDegree]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) = n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) ≤ n
[PROOFSTEP]
apply Finset.sup_le
[GOAL]
case a.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) ≤ n
[PROOFSTEP]
intro d hd
[GOAL]
case a.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ (Finsupp.sum d fun x e => e) ≤ n
[PROOFSTEP]
rw [mem_support_iff] at hd
[GOAL]
case a.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (Finsupp.sum d fun x e => e) ≤ n
[PROOFSTEP]
rw [Finsupp.sum, hφ hd]
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
[PROOFSTEP]
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
[GOAL]
case a.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
[PROOFSTEP]
simp only [← hφ hd, Finsupp.sum]
[GOAL]
case a.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
[PROOFSTEP]
replace hd := Finsupp.mem_support_iff.mpr hd
[GOAL]
case a.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
[PROOFSTEP]
exact Finset.le_sup (f := fun s ↦ ∑ x in s.support, (⇑s) x) hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ IsHomogeneous (↑(homogeneousComponent n) φ) n
[PROOFSTEP]
intro d hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d (↑(homogeneousComponent n) φ) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
[PROOFSTEP]
contrapose! hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ∑ x in d.support, ↑d x ≠ n
⊢ coeff d (↑(homogeneousComponent n) φ) = 0
[PROOFSTEP]
rw [coeff_homogeneousComponent, if_neg hd]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ↑(homogeneousComponent 0) φ = ↑C (coeff 0 φ)
[PROOFSTEP]
ext1 d
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
[PROOFSTEP]
rcases em (d = 0) with (rfl | hd)
[GOAL]
case a.inl
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ coeff 0 (↑(homogeneousComponent 0) φ) = coeff 0 (↑C (coeff 0 φ))
case a.inr
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
[PROOFSTEP]
classical
·
  simp only [coeff_homogeneousComponent, sum_eq_zero_iff, Finsupp.zero_apply, if_true, coeff_C, eq_self_iff_true,
    forall_true_iff]
· rw [coeff_homogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
  simp only [FunLike.ext_iff, Finsupp.zero_apply] at hd
  simp [hd]
[GOAL]
case a.inl
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ coeff 0 (↑(homogeneousComponent 0) φ) = coeff 0 (↑C (coeff 0 φ))
[PROOFSTEP]
simp only [coeff_homogeneousComponent, sum_eq_zero_iff, Finsupp.zero_apply, if_true, coeff_C, eq_self_iff_true,
  forall_true_iff]
[GOAL]
case a.inr
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
[PROOFSTEP]
rw [coeff_homogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
[GOAL]
case a.inr.hnc
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬∑ i in d.support, ↑d i = 0
[PROOFSTEP]
simp only [FunLike.ext_iff, Finsupp.zero_apply] at hd
[GOAL]
case a.inr.hnc
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬∀ (x : σ), ↑d x = 0
⊢ ¬∑ i in d.support, ↑d i = 0
[PROOFSTEP]
simp [hd]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
n : ℕ
r : R
⊢ ↑(homogeneousComponent n) (↑C r * φ) = ↑C r * ↑(homogeneousComponent n) φ
[PROOFSTEP]
simp only [C_mul', LinearMap.map_smul]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
⊢ ↑(homogeneousComponent n) φ = 0
[PROOFSTEP]
rw [homogeneousComponent_apply, sum_eq_zero]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
⊢ ∀ (x : σ →₀ ℕ), x ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ) → ↑(monomial x) (coeff x φ) = 0
[PROOFSTEP]
intro d hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ filter (fun d => ∑ i in d.support, ↑d i = n) (support φ)
⊢ ↑(monomial d) (coeff d φ) = 0
[PROOFSTEP]
rw [mem_filter] at hd
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ ↑(monomial d) (coeff d φ) = 0
[PROOFSTEP]
exfalso
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
d : σ →₀ ℕ
hd : d ∈ support φ ∧ ∑ i in d.support, ↑d i = n
⊢ False
[PROOFSTEP]
exact h _ hd.1 hd.2
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : totalDegree φ < n
⊢ ↑(homogeneousComponent n) φ = 0
[PROOFSTEP]
apply homogeneousComponent_eq_zero'
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : totalDegree φ < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
[PROOFSTEP]
rw [totalDegree, Finset.sup_lt_iff] at h
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
[PROOFSTEP]
intro d hd
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ ∑ i in d.support, ↑d i ≠ n
[PROOFSTEP]
exact ne_of_lt (h d hd)
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : (sup (support φ) fun s => Finsupp.sum s fun x e => e) < n
⊢ ⊥ < n
[PROOFSTEP]
exact lt_of_le_of_lt (Nat.zero_le _) h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ = φ
[PROOFSTEP]
ext1 d
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ) = coeff d φ
[PROOFSTEP]
suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by simpa [coeff_sum, coeff_homogeneousComponent]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
this : totalDegree φ < Finset.sum d.support ↑d → 0 = coeff d φ
⊢ coeff d (∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ) = coeff d φ
[PROOFSTEP]
simpa [coeff_sum, coeff_homogeneousComponent]
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ totalDegree φ < Finset.sum d.support ↑d → 0 = coeff d φ
[PROOFSTEP]
exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : p ∈ homogeneousSubmodule σ R n
⊢ ↑(homogeneousComponent m) p = if m = n then p else 0
[PROOFSTEP]
simp only [mem_homogeneousSubmodule] at h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
⊢ ↑(homogeneousComponent m) p = if m = n then p else 0
[PROOFSTEP]
ext x
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ coeff x (↑(homogeneousComponent m) p) = coeff x (if m = n then p else 0)
[PROOFSTEP]
rw [coeff_homogeneousComponent]
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
[PROOFSTEP]
by_cases zero_coeff : coeff x p = 0
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ coeff x p = coeff x p
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ 0 = coeff x p
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
[PROOFSTEP]
all_goals simp only [zero_coeff, coeff_zero]
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ coeff x p = coeff x p
[PROOFSTEP]
simp only [zero_coeff, coeff_zero]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0
[PROOFSTEP]
simp only [zero_coeff, coeff_zero]
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ 0 = coeff x p
[PROOFSTEP]
simp only [zero_coeff, coeff_zero]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
[PROOFSTEP]
simp only [zero_coeff, coeff_zero]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
[PROOFSTEP]
rw [h zero_coeff]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
[PROOFSTEP]
simp only [show n = m ↔ m = n from eq_comm]
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
[PROOFSTEP]
split_ifs with h1
[GOAL]
case pos
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : m = n
⊢ coeff x p = coeff x p
[PROOFSTEP]
rfl
[GOAL]
case neg
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : ¬m = n
⊢ 0 = coeff x 0
[PROOFSTEP]
simp only [coeff_zero]