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

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

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

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
α : 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
refine' Subring.InClosure.recOn hxs _ _ _ _
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
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
rw [RingHom.map_one]
no goals
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
rfl
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
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
rw [map_neg, map_one]
no goals
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
rfl
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
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
rintro _ ⟨p, hps, rfl⟩ n ih
no goals
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
rw [RingHom.map_mul, restriction_of, dif_pos hps, RingHom.map_mul, map_of, ih]
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
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
intro x y ihx ihy
no goals
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
rw [RingHom.map_add, RingHom.map_add, ihx, ihy]