[GOAL]
α : Type u
⊢ CommRing (FreeCommRing α)
[PROOFSTEP]
delta FreeCommRing
[GOAL]
α : Type u
⊢ CommRing (FreeAbelianGroup (Multiplicative (Multiset α)))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
⊢ Inhabited (FreeCommRing α)
[PROOFSTEP]
delta FreeCommRing
[GOAL]
α : Type u
⊢ Inhabited (FreeAbelianGroup (Multiplicative (Multiset α)))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (↑Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (↑Multiplicative.ofAdd m)
[PROOFSTEP]
dsimp [FreeCommRing]
[GOAL]
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (↑Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (↑Multiplicative.ofAdd m)
[PROOFSTEP]
rw [← Multiset.singleton_add, ofAdd_add, of, FreeAbelianGroup.of_mul_of]
[GOAL]
α : Type u
C : FreeCommRing α → Prop
z : FreeCommRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeCommRing α), C x → C (-x)
h1 : C 1
m✝ : Multiplicative (Multiset α)
a : α
m : Multiset α
ih : C (FreeAbelianGroup.of m)
⊢ C (FreeAbelianGroup.of (a ::ₘ m))
[PROOFSTEP]
convert hm (of a) _ (hb a) ih
[GOAL]
case h.e'_1
α : Type u
C : FreeCommRing α → Prop
z : FreeCommRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeCommRing α), C x → C (-x)
h1 : C 1
m✝ : Multiplicative (Multiset α)
a : α
m : Multiset α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a ::ₘ m) = of a * FreeAbelianGroup.of m
[PROOFSTEP]
apply of_cons
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ OneHom.toFun
      { toFun := fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s)),
        map_one' :=
          (_ :
            (fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s))) 1 =
              (fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s))) 1) }
      (x * y) =
    Multiset.prod (Multiset.map f x + Multiset.map f y)
[PROOFSTEP]
rw [← Multiset.map_add]
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ OneHom.toFun
      { toFun := fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s)),
        map_one' :=
          (_ :
            (fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s))) 1 =
              (fun s => Multiset.prod (Multiset.map f (↑Multiplicative.toAdd s))) 1) }
      (x * y) =
    Multiset.prod (Multiset.map f (x + y))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x : α
⊢ Multiset.prod (Multiset.map f {x}) = f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f : α → R
F : Multiplicative (Multiset α) →* R
x : Multiplicative (Multiset α)
F' : (fun x => Multiset α →+ Additive R) F := ↑MonoidHom.toAdditive'' F
x' : (fun x => Multiset α) x := ↑Multiplicative.toAdd x
⊢ Multiset.sum (Multiset.map (fun a => ↑F' {a}) x') = ↑F' x'
[PROOFSTEP]
erw [← Multiset.map_map (fun x => F' x) (fun x => { x }), ← AddMonoidHom.map_multiset_sum]
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f : α → R
F : Multiplicative (Multiset α) →* R
x : Multiplicative (Multiset α)
F' : (fun x => Multiset α →+ Additive R) F := ↑MonoidHom.toAdditive'' F
x' : (fun x => Multiset α) x := ↑Multiplicative.toAdd x
⊢ ↑F' (Multiset.sum (Multiset.map (fun x => {x}) x')) = ↑F' x'
[PROOFSTEP]
exact F.congr_arg (Multiset.sum_map_singleton x')
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ ↑(↑lift (↑f ∘ of)) (-1) = ↑f (-1)
[PROOFSTEP]
rw [RingHom.map_neg, RingHom.map_one, f.map_neg, f.map_one]
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : ↑(↑lift (↑f ∘ of)) x = ↑f x
ihy : ↑(↑lift (↑f ∘ of)) y = ↑f y
⊢ ↑(↑lift (↑f ∘ of)) (x + y) = ↑f (x + y)
[PROOFSTEP]
rw [RingHom.map_add, f.map_add, ihx, ihy]
[GOAL]
α : Type u
R : Type v
inst✝ : CommRing R
f✝ : α → R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : ↑(↑lift (↑f ∘ of)) x = ↑f x
ihy : ↑(↑lift (↑f ∘ of)) y = ↑f y
⊢ ↑(↑lift (↑f ∘ of)) (x * y) = ↑f (x * y)
[PROOFSTEP]
rw [RingHom.map_mul, f.map_mul, ihx, ihy]
[GOAL]
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑↑i) s
⊢ IsSupported (↑(↑i + 1)) s
[PROOFSTEP]
rw [Int.cast_add, Int.cast_one]
[GOAL]
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑↑i) s
⊢ IsSupported (↑↑i + 1) s
[PROOFSTEP]
exact isSupported_add hi isSupported_one
[GOAL]
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-↑i)) s
⊢ IsSupported (↑(-↑i - 1)) s
[PROOFSTEP]
rw [Int.cast_sub, Int.cast_one]
[GOAL]
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-↑i)) s
⊢ IsSupported (↑(-↑i) - 1) s
[PROOFSTEP]
exact isSupported_sub hi isSupported_one
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
⊢ p ∈ s
[PROOFSTEP]
haveI := Classical.decPred s
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
⊢ p ∈ s
[PROOFSTEP]
have : ∀ x, IsSupported x s → ∃ n : ℤ, lift (fun a => if a ∈ s then (0 : ℤ[X]) else Polynomial.X) x = n :=
  by
  intro x hx
  refine' Subring.InClosure.recOn hx _ _ _ _
  · use 1
    rw [RingHom.map_one]
    norm_cast
  · use-1
    rw [RingHom.map_neg, RingHom.map_one, Int.cast_neg, Int.cast_one]
  · rintro _ ⟨z, hzs, rfl⟩ _ _
    use 0
    rw [RingHom.map_mul, lift_of, if_pos hzs, zero_mul]
    norm_cast
  · rintro x y ⟨q, hq⟩ ⟨r, hr⟩
    refine' ⟨q + r, _⟩
    rw [RingHom.map_add, hq, hr]
    norm_cast
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
⊢ ∀ (x : FreeCommRing α), IsSupported x s → ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
[PROOFSTEP]
refine' Subring.InClosure.recOn hx _ _ _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑n
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) 1 = ↑1
[PROOFSTEP]
rw [RingHom.map_one]
[GOAL]
case h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ 1 = ↑1
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (-1) = ↑n
[PROOFSTEP]
use-1
[GOAL]
case h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (-1) = ↑(-1)
[PROOFSTEP]
rw [RingHom.map_neg, RingHom.map_one, Int.cast_neg, Int.cast_one]
[GOAL]
case refine'_3
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∀ (z : FreeCommRing α),
    z ∈ of '' s →
      ∀ (n : FreeCommRing α),
        (∃ n_1, ↑(↑lift fun a => if a ∈ s then 0 else X) n = ↑n_1) →
          ∃ n_1, ↑(↑lift fun a => if a ∈ s then 0 else X) (z * n) = ↑n_1
[PROOFSTEP]
rintro _ ⟨z, hzs, rfl⟩ _ _
[GOAL]
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (of z * n✝) = ↑n
[PROOFSTEP]
use 0
[GOAL]
case h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (of z * n✝) = ↑0
[PROOFSTEP]
rw [RingHom.map_mul, lift_of, if_pos hzs, zero_mul]
[GOAL]
case h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) n✝ = ↑n
⊢ 0 = ↑0
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_4
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x : FreeCommRing α
hx : IsSupported x s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) y = ↑n) →
        ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑n
[PROOFSTEP]
rintro x y ⟨q, hq⟩ ⟨r, hr⟩
[GOAL]
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ s
x y : FreeCommRing α
q : ℤ
hq : ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : ↑(↑lift fun a => if a ∈ s then 0 else X) y = ↑r
⊢ ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑n
[PROOFSTEP]
refine' ⟨q + r, _⟩
[GOAL]
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ s
x y : FreeCommRing α
q : ℤ
hq : ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : ↑(↑lift fun a => if a ∈ s then 0 else X) y = ↑r
⊢ ↑(↑lift fun a => if a ∈ s then 0 else X) (x + y) = ↑(q + r)
[PROOFSTEP]
rw [RingHom.map_add, hq, hr]
[GOAL]
case refine'_4.intro.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
x✝ : FreeCommRing α
hx : IsSupported x✝ s
x y : FreeCommRing α
q : ℤ
hq : ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : ↑(↑lift fun a => if a ∈ s then 0 else X) y = ↑r
⊢ ↑q + ↑r = ↑(q + r)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∀ (x : FreeCommRing α), IsSupported x s → ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) x = ↑n
⊢ p ∈ s
[PROOFSTEP]
specialize this (of p) hps
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, ↑(↑lift fun a => if a ∈ s then 0 else X) (of p) = ↑n
⊢ p ∈ s
[PROOFSTEP]
rw [lift_of] at this 
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
this : ∃ n, (if p ∈ s then 0 else X) = ↑n
⊢ p ∈ s
[PROOFSTEP]
split_ifs at this  with h
[GOAL]
case pos
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s
[PROOFSTEP]
exact h
[GOAL]
case neg
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ p ∈ s
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ False
[PROOFSTEP]
apply Ne.symm Int.zero_ne_one
[GOAL]
case neg.h
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
this : ∃ n, X = ↑n
⊢ 1 = 0
[PROOFSTEP]
rcases this with ⟨w, H⟩
[GOAL]
case neg.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑w
⊢ 1 = 0
[PROOFSTEP]
rw [← Polynomial.C_eq_int_cast] at H 
[GOAL]
case neg.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ 1 = 0
[PROOFSTEP]
have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ coeff X 1 = coeff (↑C w) 1
[PROOFSTEP]
rw [H]
[GOAL]
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
⊢ coeff (↑C ↑w) 1 = coeff (↑C w) 1
[PROOFSTEP]
rfl
[GOAL]
case neg.h.intro
α : Type u
β : Type v
f : α → β
p : α
s : Set α
hps : IsSupported (of p) s
this✝ : DecidablePred s
h : ¬p ∈ s
w : ℤ
H : X = ↑C ↑w
this : coeff X 1 = coeff (↑C w) 1
⊢ 1 = 0
[PROOFSTEP]
rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this 
[GOAL]
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ↑(map Subtype.val) (↑(restriction s) x) = x
[PROOFSTEP]
refine' Subring.InClosure.recOn hxs _ _ _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ↑(map Subtype.val) (↑(restriction s) 1) = 1
[PROOFSTEP]
rw [RingHom.map_one]
[GOAL]
case refine'_1
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ↑(map Subtype.val) 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ↑(map Subtype.val) (↑(restriction s) (-1)) = -1
[PROOFSTEP]
rw [map_neg, map_one]
[GOAL]
case refine'_2
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ↑(map Subtype.val) (-1) = -1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ∀ (z : FreeCommRing α),
    z ∈ of '' s →
      ∀ (n : FreeCommRing α),
        ↑(map Subtype.val) (↑(restriction s) n) = n → ↑(map Subtype.val) (↑(restriction s) (z * n)) = z * n
[PROOFSTEP]
rintro _ ⟨p, hps, rfl⟩ n ih
[GOAL]
case refine'_3.intro.intro
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : ↑(map Subtype.val) (↑(restriction s) n) = n
⊢ ↑(map Subtype.val) (↑(restriction s) (of p * n)) = of p * n
[PROOFSTEP]
rw [RingHom.map_mul, restriction_of, dif_pos hps, RingHom.map_mul, map_of, ih]
[GOAL]
case refine'_4
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x s
⊢ ∀ {x y : FreeCommRing α},
    ↑(map Subtype.val) (↑(restriction s) x) = x →
      ↑(map Subtype.val) (↑(restriction s) y) = y → ↑(map Subtype.val) (↑(restriction s) (x + y)) = x + y
[PROOFSTEP]
intro x y ihx ihy
[GOAL]
case refine'_4
α : Type u
β : Type v
f : α → β
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : IsSupported x✝ s
x y : FreeCommRing α
ihx : ↑(map Subtype.val) (↑(restriction s) x) = x
ihy : ↑(map Subtype.val) (↑(restriction s) y) = y
⊢ ↑(map Subtype.val) (↑(restriction s) (x + y)) = x + y
[PROOFSTEP]
rw [RingHom.map_add, RingHom.map_add, ihx, ihy]
[GOAL]
α : Type u
β : Type v
f : α → β
x : FreeCommRing α
s : Set α
hfs : Set.Finite s
hxs : IsSupported x s
⊢ IsSupported x ↑(Set.Finite.toFinset hfs)
[PROOFSTEP]
rwa [Set.Finite.coe_toFinset]
[GOAL]
α : Type u
x : FreeRing α
⊢ ↑(-x) = -↑x
[PROOFSTEP]
rw [castFreeCommRing, map_neg]
[GOAL]
α : Type u
x y : FreeRing α
⊢ ↑(x - y) = ↑x - ↑y
[PROOFSTEP]
rw [castFreeCommRing, map_sub]
[GOAL]
α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x
[PROOFSTEP]
induction x using FreeCommRing.induction_on with
| hn1 =>
  use-1
  rfl
| hb b => exact ⟨FreeRing.of b, rfl⟩
| ha _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
| hm _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
[GOAL]
α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x
[PROOFSTEP]
induction x using FreeCommRing.induction_on with
| hn1 =>
  use-1
  rfl
| hb b => exact ⟨FreeRing.of b, rfl⟩
| ha _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
| hm _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
[GOAL]
case hn1
α : Type u
⊢ ∃ a, ↑a = -1
[PROOFSTEP]

| hn1 =>
  use-1
  rfl
[GOAL]
case hn1
α : Type u
⊢ ∃ a, ↑a = -1
[PROOFSTEP]
use-1
[GOAL]
case h
α : Type u
⊢ ↑(-1) = -1
[PROOFSTEP]
rfl
[GOAL]
case hb
α : Type u
b : α
⊢ ∃ a, ↑a = FreeCommRing.of b
[PROOFSTEP]

| hb b => exact ⟨FreeRing.of b, rfl⟩
[GOAL]
case hb
α : Type u
b : α
⊢ ∃ a, ↑a = FreeCommRing.of b
[PROOFSTEP]
exact ⟨FreeRing.of b, rfl⟩
[GOAL]
case ha
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝
[PROOFSTEP]

| ha _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
[GOAL]
case ha
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case ha.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝
[PROOFSTEP]
rcases hy with ⟨y, rfl⟩
[GOAL]
case ha.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y
[PROOFSTEP]
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
[GOAL]
case hm
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝
[PROOFSTEP]

| hm _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
[GOAL]
case hm
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case hm.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝
[PROOFSTEP]
rcases hy with ⟨y, rfl⟩
[GOAL]
case hm.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x * ↑y
[PROOFSTEP]
exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
[GOAL]
α : Type u
⊢ castFreeCommRing = Functor.map fun l => ↑l
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u
x : FreeRing α
⊢ ↑x = (fun l => ↑l) <$> x
[PROOFSTEP]
erw [castFreeCommRing, toFreeCommRing, FreeRing.lift, Equiv.coe_trans, Function.comp,
  FreeAbelianGroup.liftMonoid_coe (FreeMonoid.lift FreeCommRing.of)]
[GOAL]
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x
[PROOFSTEP]
dsimp [Functor.map]
[GOAL]
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
[PROOFSTEP]
rw [← AddMonoidHom.coe_coe]
[GOAL]
case h
α : Type u
x : FreeRing α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
[PROOFSTEP]
apply FreeAbelianGroup.lift.unique
[GOAL]
case h.hg
α : Type u
x : FreeRing α
⊢ ∀ (x : FreeMonoid α),
    ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) =
      ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) x
[PROOFSTEP]
intro L
[GOAL]
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) L
[PROOFSTEP]
erw [FreeAbelianGroup.lift.of, Function.comp]
[GOAL]
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(↑FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L
[PROOFSTEP]
exact
  FreeMonoid.recOn L rfl fun hd tl ih =>
    by
    rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
    conv_lhs => reduce
[GOAL]
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ ↑(↑FreeMonoid.lift FreeCommRing.of) (FreeMonoid.of hd * tl) = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)
[PROOFSTEP]
rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
[GOAL]
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ FreeCommRing.of hd * FreeAbelianGroup.of ↑tl = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)
[PROOFSTEP]
conv_lhs => reduce
[GOAL]
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
| FreeCommRing.of hd * FreeAbelianGroup.of ↑tl
[PROOFSTEP]
reduce
[GOAL]
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
| FreeCommRing.of hd * FreeAbelianGroup.of ↑tl
[PROOFSTEP]
reduce
[GOAL]
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
| FreeCommRing.of hd * FreeAbelianGroup.of ↑tl
[PROOFSTEP]
reduce
[GOAL]
α : Type u
inst✝ : Subsingleton α
⊢ Bijective ↑(coeRingHom α)
[PROOFSTEP]
have :
  (coeRingHom _ : FreeRing α → FreeCommRing α) = Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α) :=
  coe_eq α
[GOAL]
α : Type u
inst✝ : Subsingleton α
this : ↑(coeRingHom α) = ↑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
⊢ Bijective ↑(coeRingHom α)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝ : Subsingleton α
this : ↑(coeRingHom α) = ↑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
⊢ Bijective ↑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
[PROOFSTEP]
apply Equiv.bijective
[GOAL]
α : Type u
inst✝ : Subsingleton α
src✝ : Ring (FreeRing α) := inferInstanceAs (Ring (FreeRing α))
x y : FreeRing α
⊢ x * y = y * x
[PROOFSTEP]
rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x), (subsingletonEquivFreeCommRing α).map_mul, mul_comm, ←
  (subsingletonEquivFreeCommRing α).map_mul, (subsingletonEquivFreeCommRing α).symm_apply_apply]
[GOAL]
α : Type u
⊢ RingHom.comp ↑(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)
      ↑(↑FreeCommRing.lift fun a => MvPolynomial.X a) =
    RingHom.id (FreeCommRing α)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
x✝ : α
⊢ ↑(RingHom.comp ↑(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)
          ↑(↑FreeCommRing.lift fun a => MvPolynomial.X a))
      (FreeCommRing.of x✝) =
    ↑(RingHom.id (FreeCommRing α)) (FreeCommRing.of x✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u
⊢ RingHom.comp ↑(↑FreeCommRing.lift fun a => MvPolynomial.X a)
      ↑(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) =
    RingHom.id (MvPolynomial α ℤ)
[PROOFSTEP]
ext
[GOAL]
case hC.a.a
α : Type u
x✝ : ℤ
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (↑(RingHom.comp
            (RingHom.comp ↑(↑FreeCommRing.lift fun a => MvPolynomial.X a)
              ↑(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
            MvPolynomial.C)
        x✝) =
    MvPolynomial.coeff m✝ (↑(RingHom.comp (RingHom.id (MvPolynomial α ℤ)) MvPolynomial.C) x✝)
[PROOFSTEP]
simp
[GOAL]
case hX.a
α : Type u
i✝ : α
m✝ : α →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (↑(RingHom.comp ↑(↑FreeCommRing.lift fun a => MvPolynomial.X a)
            ↑(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ (↑(RingHom.id (MvPolynomial α ℤ)) (MvPolynomial.X i✝))
[PROOFSTEP]
simp
