awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x * y)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₂ :
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x * y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x * y) : R)
have rw₃ : HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R) =
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_mul, f.map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(↑i : ℤ) : FreeCommRing α) s
⊢ IsSupported (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : FreeCommRing α) s
have rw : (HAdd.hAdd (α := FreeCommRing α) (↑(↑i : ℤ) : FreeCommRing α) 1).IsSupported s
Tactic: rw [Int.cast_add, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
i_1 : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-(↑i : ℤ)) : FreeCommRing α) s
⊢ IsSupported (↑(HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1) : FreeCommRing α) s
have rw : (HSub.hSub (α := FreeCommRing α) (↑(-(↑i : ℤ)) : FreeCommRing α) 1).IsSupported s
Tactic: rw [Int.cast_sub, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
⊢ p ∈ s
have haveI : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
Tactic: haveI := Classical.decPred (· ∈ s)
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
have 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])
Tactic: refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ ∃ (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])
have 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])
Tactic: refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ ∃ (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])
have 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])
Tactic: refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ ∃ (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])
have 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])
Tactic: refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
        1)
      (↑n : ℤ[X])
have 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])
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      1)
    (↑1 : ℤ[X])
have h : Eq (α := ℤ[X]) 1 (↑1 : ℤ[X])
Tactic: rw [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ Eq (α := ℤ[X]) 1 (↑1 : ℤ[X])
have h : Eq (α := ℕ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
        (-1))
      (↑n : ℤ[X])
have 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])
Tactic: use -1
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])
have 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])
Tactic: rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])
have h₁ : Eq (α := ℤ[X]) (-1) (↑(-1) : ℤ[X])
Tactic: rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])
have h₂ : Eq (α := ℤ[X]) (-1) (-(↑1 : ℤ[X]))
Tactic: rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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]))
⊢ Eq (α := ℤ[X])
    ((((lift : (a : α → ℤ[X]) → FreeCommRing α →+* ℤ[X]) fun (a : α) ↦ if a ∈ s then 0 else X :
          FreeCommRing α →+* ℤ[X]) :
        (a : FreeCommRing α) → ℤ[X])
      (-1))
    (↑(-1) : ℤ[X])
have h₃ : Eq (α := ℤ[X]) (-1) (-1)
Tactic: rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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 :
  ∃ (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])
          (of z * n) :
        ℤ[X])
      ((↑n_1 : ℤ[X]) : ℤ[X])
have 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])
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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 :
  ∃ (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])
⊢ 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])
have h : Eq (α := ℤ[X]) 0 (↑0 : ℤ[X])
Tactic: rw [map_mul, lift_of, if_pos hzs, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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 :
  ∃ (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])
⊢ Eq (α := ℤ[X]) 0 (↑0 : ℤ[X])
have h : Eq (α := ℕ) 0 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
have 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])
Tactic: refine ⟨q + r, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ 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])
have refine_4 : HAdd.hAdd (α := ℤ[X]) (↑q : ℤ[X]) (↑r : ℤ[X]) = (↑(q + r) : ℤ[X])
Tactic: rw [map_add, hq, hr]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ HAdd.hAdd (α := ℤ[X]) (↑q : ℤ[X]) (↑r : ℤ[X]) = (↑(q + r) : ℤ[X])
have refine_4 : q + r = q + r
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (hypothesis)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun (x : α) ↦ x ∈ s
⊢ p ∈ s
have 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])
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
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (hypothesis)
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])
⊢ p ∈ s
have 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])
Tactic: specialize this (of p) hps
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (hypothesis)
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])
⊢ p ∈ s
have this₁ : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])
Tactic: rw [lift_of] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ p ∈ s
have pos : ∀ (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
Tactic: split_ifs at this with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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
⊢ p ∈ s
have neg : ∀ (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
Tactic: split_ifs at this with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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])
⊢ p ∈ s
have neg : False
Tactic: exfalso