case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
i : σ →₀ ℕ
fr : S₁
⊢ ∃ a, ↑(map f) a = ↑(monomial i) fr

case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
a b : MvPolynomial σ S₁
ha : ∃ a_1, ↑(map f) a_1 = a
hb : ∃ a, ↑(map f) a = b
⊢ ∃ a_1, ↑(map f) a_1 = a + b
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
p : MvPolynomial σ S₁
⊢ ∃ a, ↑(map f) a = p
induction' p using MvPolynomial.induction_on' with i fr a b ha hb
case h1.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
i : σ →₀ ℕ
r : R
⊢ ∃ a, ↑(map f) a = ↑(monomial i) (↑f r)
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
i : σ →₀ ℕ
fr : S₁
⊢ ∃ a, ↑(map f) a = ↑(monomial i) fr
obtain ⟨r, rfl⟩ := hf fr
no goals
case h1.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
i : σ →₀ ℕ
r : R
⊢ ∃ a, ↑(map f) a = ↑(monomial i) (↑f r)
exact ⟨monomial i r, map_monomial _ _ _⟩
case h2.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
b : MvPolynomial σ S₁
hb : ∃ a, ↑(map f) a = b
a : MvPolynomial σ R
⊢ ∃ a_1, ↑(map f) a_1 = ↑(map f) a + b
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
a b : MvPolynomial σ S₁
ha : ∃ a_1, ↑(map f) a_1 = a
hb : ∃ a, ↑(map f) a = b
⊢ ∃ a_1, ↑(map f) a_1 = a + b
obtain ⟨a, rfl⟩ := ha
case h2.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
a b : MvPolynomial σ R
⊢ ∃ a_1, ↑(map f) a_1 = ↑(map f) a + ↑(map f) b
case h2.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
b : MvPolynomial σ S₁
hb : ∃ a, ↑(map f) a = b
a : MvPolynomial σ R
⊢ ∃ a_1, ↑(map f) a_1 = ↑(map f) a + b
obtain ⟨b, rfl⟩ := hb
no goals
case h2.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Surjective ↑f
a b : MvPolynomial σ R
⊢ ∃ a_1, ↑(map f) a_1 = ↑(map f) a + ↑(map f) b
exact ⟨a + b, RingHom.map_add _ _ _⟩