awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeCommRing α
s : Set α
hxs : x.IsSupported s
hys : y.IsSupported s
⊢ (x + y).IsSupported s

Tactic:
Subring.add_mem _ hxs hys

Premises used: FreeCommRing.IsSupported, Subring.add_mem, Set.Mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
hxs : x.IsSupported s
⊢ (-x).IsSupported s

Tactic:
Subring.neg_mem _ hxs

Premises used: FreeCommRing.IsSupported, Set.Mem, Subring.neg_mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeCommRing α
s : Set α
hxs : x.IsSupported s
hys : y.IsSupported s
⊢ (x - y).IsSupported s

Tactic:
Subring.sub_mem _ hxs hys

Premises used: FreeCommRing.IsSupported, Set.Mem, Subring.sub_mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeCommRing α
s : Set α
hxs : x.IsSupported s
hys : y.IsSupported s
⊢ (x * y).IsSupported s

Tactic:
Subring.mul_mem _ hxs hys

Premises used: FreeCommRing.IsSupported, Set.Mem, Subring.mul_mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
s : Set α
⊢ IsSupported 0 s

Tactic:
Subring.zero_mem _

Premises used: Subring.zero_mem, FreeCommRing.IsSupported, Set.Mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
s : Set α
⊢ IsSupported 1 s

Tactic:
Subring.one_mem _

Premises used: FreeCommRing.IsSupported, Set.Mem, Subring.one_mem
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(↑i : ℤ) : FreeCommRing α) s
rw : (HAdd.hAdd (α := FreeCommRing α) (↑(↑i : ℤ) : FreeCommRing α) 1).IsSupported s
⊢ IsSupported (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : FreeCommRing α) s

Tactic:
rw [Int.cast_add, Int.cast_one]

Premises used: Int.cast_add, Int.cast_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(↑i : ℤ) : FreeCommRing α) s
⊢ (HAdd.hAdd (α := FreeCommRing α) (↑(↑i : ℤ) : FreeCommRing α) 1).IsSupported s

Tactic:
isSupported_add hi isSupported_one

Premises used: FreeCommRing.isSupported_add, FreeCommRing.isSupported_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(↑i : ℤ) : FreeCommRing α) s
⊢ (HAdd.hAdd (α := FreeCommRing α) (↑(↑i : ℤ) : FreeCommRing α) 1).IsSupported s

Tactic:
exact isSupported_add hi isSupported_one

Premises used: FreeCommRing.isSupported_add, FreeCommRing.isSupported_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-(↑i : ℤ)) : FreeCommRing α) s
rw : (HSub.hSub (α := FreeCommRing α) (↑(-(↑i : ℤ)) : FreeCommRing α) 1).IsSupported s
⊢ IsSupported (↑(HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1) : FreeCommRing α) s

Tactic:
rw [Int.cast_sub, Int.cast_one]

Premises used: Int.cast_sub, Int.cast_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-(↑i : ℤ)) : FreeCommRing α) s
⊢ (HSub.hSub (α := FreeCommRing α) (↑(-(↑i : ℤ)) : FreeCommRing α) 1).IsSupported s

Tactic:
isSupported_sub hi isSupported_one

Premises used: FreeCommRing.isSupported_sub, FreeCommRing.isSupported_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-(↑i : ℤ)) : FreeCommRing α) s
⊢ (HSub.hSub (α := FreeCommRing α) (↑(-(↑i : ℤ)) : FreeCommRing α) 1).IsSupported s

Tactic:
exact isSupported_sub hi isSupported_one

Premises used: FreeCommRing.isSupported_sub, FreeCommRing.isSupported_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
p : α
⊢ Eq (α := FreeCommRing (↑s : Type u))
    ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
    (if H : p ∈ s then of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p H) else 0 : FreeCommRing (↑s : Type u))

Tactic:
lift_of _ _

Premises used: FreeCommRing.lift_of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
⊢ p ∈ s

Tactic:
haveI := Classical.decPred (· ∈ s)
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          x :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])

Tactic:
Subring.InClosure.recOn hx ?_ ?_ ?_ ?_

Premises used: Subring.InClosure.recOn
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
refine_1 :
  ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        1)
      (↑n : ℤ[X])
refine_2 :
  ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (-1))
      (↑n : ℤ[X])
refine_3 :
  ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (∃ (n_1 : ℤ),
          Eq (α := ℤ[X])
            ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                    FreeCommRing α →+* ℤ[X]) :
                  (a : FreeCommRing α) → ℤ[X])
                n :
              ℤ[X])
            ((↑n_1 : ℤ[X]) : ℤ[X])) →
        ∃ (n_1 : ℤ),
          Eq (α := ℤ[X])
            ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                    FreeCommRing α →+* ℤ[X]) :
                  (a : FreeCommRing α) → ℤ[X])
                (z * n) :
              ℤ[X])
            ((↑n_1 : ℤ[X]) : ℤ[X])
refine_4 :
  ∀ {x y : FreeCommRing α},
    (∃ (n : ℤ),
        Eq (α := ℤ[X])
          ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                  FreeCommRing α →+* ℤ[X]) :
                (a : FreeCommRing α) → ℤ[X])
              x :
            ℤ[X])
          ((↑n : ℤ[X]) : ℤ[X])) →
      (∃ (n : ℤ),
          Eq (α := ℤ[X])
            ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                    FreeCommRing α →+* ℤ[X]) :
                  (a : FreeCommRing α) → ℤ[X])
                y :
              ℤ[X])
            ((↑n : ℤ[X]) : ℤ[X])) →
        ∃ (n : ℤ),
          Eq (α := ℤ[X])
            ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                    FreeCommRing α →+* ℤ[X]) :
                  (a : FreeCommRing α) → ℤ[X])
                (x + y) :
              ℤ[X])
            ((↑n : ℤ[X]) : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          x :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])

Tactic:
refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
h :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      1)
    (↑1 : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        1)
      (↑n : ℤ[X])

Tactic:
use 1
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
h : Eq (α := ℤ[X]) 1 (↑1 : ℤ[X])
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      1)
    (↑1 : ℤ[X])

Tactic:
rw [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
h h₁ h₂ h₃ : Eq (α := ℕ) 1 1
⊢ Eq (α := ℤ[X]) 1 (↑1 : ℤ[X])

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
h :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (-1))
      (↑n : ℤ[X])

Tactic:
use -1
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
h :
  Eq (α := ℤ[X])
    (-(((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        1)
    (↑(-1) : ℤ[X])
h₁ : Eq (α := ℤ[X]) (-1) (↑(-1) : ℤ[X])
h₂ : Eq (α := ℤ[X]) (-1) (-(↑1 : ℤ[X]))
h₃ h₄ : Eq (α := ℤ[X]) (-1) (-1)
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])

Tactic:
rw [map_neg, map_one, Int.cast_neg, Int.cast_one]

Premises used: Int.cast_neg, map_neg, map_one, Int.cast_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n : FreeCommRing α
h_1 :
  ∃ (n_1 : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          n :
        ℤ[X])
      ((↑n_1 : ℤ[X]) : ℤ[X])
h :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (of z * n) :
      ℤ[X])
    ((↑0 : ℤ[X]) : ℤ[X])
⊢ ∃ (n_1 : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          (of z * n) :
        ℤ[X])
      ((↑n_1 : ℤ[X]) : ℤ[X])

Tactic:
use 0
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n : FreeCommRing α
h_1 :
  ∃ (n_1 : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          n :
        ℤ[X])
      ((↑n_1 : ℤ[X]) : ℤ[X])
h : Eq (α := ℤ[X]) 0 (↑0 : ℤ[X])
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (of z * n) :
      ℤ[X])
    ((↑0 : ℤ[X]) : ℤ[X])

Tactic:
rw [map_mul, lift_of, if_pos hzs, zero_mul]

Premises used: MulZeroClass.zero_mul, FreeCommRing.lift_of, if_pos, map_mul
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n : FreeCommRing α
h_1 :
  ∃ (n_1 : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          n :
        ℤ[X])
      ((↑n_1 : ℤ[X]) : ℤ[X])
h h₁ h₂ h₃ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℤ[X]) 0 (↑0 : ℤ[X])

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x_1 : FreeCommRing α
hx : x_1.IsSupported s
x y : FreeCommRing α
q : ℤ
hq :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        x :
      ℤ[X])
    ((↑q : ℤ[X]) : ℤ[X])
r : ℤ
hr :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        y :
      ℤ[X])
    ((↑r : ℤ[X]) : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          (x + y) :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])

Tactic:
⟨q + r, ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x_1 : FreeCommRing α
hx : x_1.IsSupported s
x y : FreeCommRing α
q : ℤ
hq :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        x :
      ℤ[X])
    ((↑q : ℤ[X]) : ℤ[X])
r : ℤ
hr :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        y :
      ℤ[X])
    ((↑r : ℤ[X]) : ℤ[X])
refine_4 :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (x + y) :
      ℤ[X])
    ((↑(q + r) : ℤ[X]) : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          (x + y) :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])

Tactic:
refine ⟨q + r, ?_⟩
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x_1 : FreeCommRing α
hx : x_1.IsSupported s
x y : FreeCommRing α
q : ℤ
hq :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        x :
      ℤ[X])
    ((↑q : ℤ[X]) : ℤ[X])
r : ℤ
hr :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        y :
      ℤ[X])
    ((↑r : ℤ[X]) : ℤ[X])
refine_4 : HAdd.hAdd (α := ℤ[X]) (↑q : ℤ[X]) (↑r : ℤ[X]) = (↑(q + r) : ℤ[X])
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        (x + y) :
      ℤ[X])
    ((↑(q + r) : ℤ[X]) : ℤ[X])

Tactic:
rw [map_add, hq, hr]

Premises used: map_add
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x_1 : FreeCommRing α
hx : x_1.IsSupported s
x y : FreeCommRing α
q : ℤ
hq :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        x :
      ℤ[X])
    ((↑q : ℤ[X]) : ℤ[X])
r : ℤ
hr :
  Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
            FreeCommRing α →+* ℤ[X]) :
          (a : FreeCommRing α) → ℤ[X])
        y :
      ℤ[X])
    ((↑r : ℤ[X]) : ℤ[X])
refine_4 refine_4₁ refine_4₂ refine_4₃ : q + r = q + r
⊢ HAdd.hAdd (α := ℤ[X]) (↑q : ℤ[X]) (↑r : ℤ[X]) = (↑(q + r) : ℤ[X])

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ∀ (x : FreeCommRing α),
    x.IsSupported s →
      ∃ (n : ℤ),
        Eq (α := ℤ[X])
          ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                  FreeCommRing α →+* ℤ[X]) :
                (a : FreeCommRing α) → ℤ[X])
              x :
            ℤ[X])
          ((↑n : ℤ[X]) : ℤ[X])

Tactic:
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 [map_one]
      norm_cast
    · use -1
      rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
    · rintro _ ⟨z, hzs, rfl⟩ _ _
      use 0
      rw [map_mul, lift_of, if_pos hzs, zero_mul]
      norm_cast
    · rintro x y ⟨q, hq⟩ ⟨r, hr⟩
      refine ⟨q + r, ?_⟩
      rw [map_add, hq, hr]
      norm_cast
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
this :
  ∀ (x : FreeCommRing α),
    x.IsSupported s →
      ∃ (n : ℤ),
        Eq (α := ℤ[X])
          ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
                  FreeCommRing α →+* ℤ[X]) :
                (a : FreeCommRing α) → ℤ[X])
              x :
            ℤ[X])
          ((↑n : ℤ[X]) : ℤ[X])
⊢ ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          (of p) :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])

Tactic:
specialize this (of p) hps

Premises used: FreeCommRing.of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
this :
  ∃ (n : ℤ),
    Eq (α := ℤ[X])
      ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
              FreeCommRing α →+* ℤ[X]) :
            (a : FreeCommRing α) → ℤ[X])
          (of p) :
        ℤ[X])
      ((↑n : ℤ[X]) : ℤ[X])
⊢ ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])

Tactic:
rw [lift_of] at this

Premises used: FreeCommRing.lift_of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])
pos : ∀ (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
neg : ∀ (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
⊢ p ∈ s

Tactic:
split_ifs at this with h
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∈ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])
⊢ p ∈ s

Tactic:
h
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∈ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])
⊢ p ∈ s

Tactic:
exact h
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])
neg : False
⊢ p ∈ s

Tactic:
exfalso
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])
neg : Eq (α := ℤ) 1 0
⊢ False

Tactic:
apply Ne.symm Int.zero_ne_one

Premises used: Int.zero_ne_one, Ne.symm
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])
neg : ∀ (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
⊢ Eq (α := ℤ) 1 0

Tactic:
rcases this with ⟨w, H⟩
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X (↑w : ℤ[X])
⊢ Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))

Tactic:
rw [← Polynomial.C_eq_intCast] at H

Premises used: Polynomial.C_eq_intCast
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
rw : Eq (α := ℤ) (coeff ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ)) 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)
⊢ Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)

Tactic:
rw [H]
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
⊢ Eq (α := ℤ) (coeff ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ)) 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
⊢ Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)

Tactic:
have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
this : Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)
neg : ∀ (this : coeff X 1 = if Eq (α := ℕ) 1 0 then w else 0), Eq (α := ℤ) 1 0
neg₁ : ∀ (this : Eq (α := ℤ) (coeff X 1) 0), Eq (α := ℤ) 1 0
neg₂ : ∀ (this : Eq (α := ℤ) (if Eq (α := ℕ) 1 1 then 1 else 0) 0), Eq (α := ℤ) 1 0
neg₃ neg₄ neg₅ neg₆ : ∀ (this : Eq (α := ℤ) 1 0), Eq (α := ℤ) 1 0
⊢ Eq (α := ℤ) 1 0

Tactic:
rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this

Premises used: if_pos, Polynomial.coeff_C, one_ne_zero, Polynomial.coeff_X, if_neg, rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x

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

Premises used: Subring.InClosure.recOn