-- Mathlib/RingTheory/FreeCommRing.lean
theorem map_subtype_val_restriction {x} (s : Set α) [DecidablePred (· ∈ s)]
    (hxs : IsSupported x s) : map (↑) (restriction s x) = x

Proof state:
case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported 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

Tactic:
intro x y ihx ihy

Result:
case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x✝.IsSupported 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

Proof state:
case refine_3.intro.intro
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported 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

Tactic:
rw [RingHom.map_mul, restriction_of, dif_pos hps, RingHom.map_mul, map_of, ih]

Result:
no goals

Proof state:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) (-1)) = -1

Tactic:
rw [map_neg, map_one]

Result:
case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) (-1) = -1

Proof state:
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) x) = x

Tactic:
refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) 1) = 1

case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) (-1)) = -1

case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ ∀ 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
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported 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

Proof state:
case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) (-1) = -1

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) 1) = 1

Tactic:
rw [RingHom.map_one]

Result:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) 1 = 1

Proof state:
case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x✝.IsSupported 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

Tactic:
rw [RingHom.map_add, RingHom.map_add, ihx, ihy]

Result:
no goals

Proof state:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

Tactic:
rintro _ ⟨p, hps, rfl⟩ n ih

Result:
case refine_3.intro.intro
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hxs : x.IsSupported 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