case h_C
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, ↑C a = ↑(rename Subtype.val) q

case h_add
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = ↑(rename Subtype.val) q) →
      (∃ s q_1, q = ↑(rename Subtype.val) q_1) → ∃ s q_1, p + q = ↑(rename Subtype.val) q_1

case h_X
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = ↑(rename Subtype.val) q) → ∃ s q, p * X n = ↑(rename Subtype.val) q
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ s q, p = ↑(rename Subtype.val) q
apply induction_on p
case h_C
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ∃ s q, ↑C r = ↑(rename Subtype.val) q
case h_C
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, ↑C a = ↑(rename Subtype.val) q
intro r
no goals
case h_C
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ∃ s q, ↑C r = ↑(rename Subtype.val) q
exact ⟨∅, C r, by rw [rename_C]⟩
no goals
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ↑C r = ↑(rename Subtype.val) (↑C r)
rw [rename_C]
case h_add.intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, ↑(rename Subtype.val) p + ↑(rename Subtype.val) q = ↑(rename Subtype.val) q_1
case h_add
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = ↑(rename Subtype.val) q) →
      (∃ s q_1, q = ↑(rename Subtype.val) q_1) → ∃ s q_1, p + q = ↑(rename Subtype.val) q_1
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
case h_add.intro.intro.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R

case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q = ↑(rename Subtype.val) ?h_add.intro.intro.intro.intro.refine'_1
case h_add.intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, ↑(rename Subtype.val) p + ↑(rename Subtype.val) q = ↑(rename Subtype.val) q_1
refine' ⟨s ∪ t, ⟨_, _⟩⟩
no goals
case h_add.intro.intro.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R
refine' rename (Subtype.map id _) p + rename (Subtype.map id _) q <;>
  simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff,
    Finset.mem_union, forall_true_iff]
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
      ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
        ↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q)
simp only [rename_rename, AlgHom.map_add]
no goals
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
      ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q
rfl
case h_X.intro.intro
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, ↑(rename Subtype.val) p * X n = ↑(rename Subtype.val) q
case h_X
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = ↑(rename Subtype.val) q) → ∃ s q, p * X n = ↑(rename Subtype.val) q
rintro p n ⟨s, p, rfl⟩
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R

case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n = ↑(rename Subtype.val) ?h_X.intro.intro.refine'_1
case h_X.intro.intro
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, ↑(rename Subtype.val) p * X n = ↑(rename Subtype.val) q
refine' ⟨insert n s, ⟨_, _⟩⟩
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ insert n s
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R
refine' rename (Subtype.map id _) p * X ⟨n, s.mem_insert_self n⟩
no goals
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ insert n s
simp (config := { contextual := true }) only [id.def, or_true_iff, Finset.mem_insert,
  forall_true_iff]
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p * X n
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p *
        X { val := n, property := (_ : n ∈ insert n s) })
simp only [rename_rename, rename_X, Subtype.coe_mk, AlgHom.map_mul]
no goals
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type ?u.711231
α : Type ?u.711234
R : Type u_2
S : Type ?u.711240
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p * X n
rfl