awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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])
⊢ False
have neg : Eq (α := ℤ) 1 0
Tactic: apply Ne.symm Int.zero_ne_one
-- 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])
⊢ Eq (α := ℤ) 1 0
have neg : ∀ (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
Tactic: rcases this with ⟨w, H⟩
Cleared hypotheses: this
-- 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
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X (↑w : ℤ[X])
⊢ Eq (α := ℤ) 1 0
have H₁ : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
Tactic: rw [← Polynomial.C_eq_intCast] at H
Cleared hypotheses: H
-- 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
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
⊢ Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)
have rw : Eq (α := ℤ) (coeff ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ)) 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)
Tactic: rw [H]
-- 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
h : p ∉ s
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
⊢ Eq (α := ℤ) 1 0
have this₁ : 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
-- 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
w : ℤ
H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))
this : Eq (α := ℤ) (coeff X 1) (coeff ((C : (a : ℤ) → ℤ[X]) w) 1)
⊢ Eq (α := ℤ) 1 0
have neg : ∀ (this : coeff X 1 = if Eq (α := ℕ) 1 0 then w else 0), Eq (α := ℤ) 1 0
Tactic: rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] 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
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
⊢ Eq (α := ℤ) 1 0
have neg₁ : ∀ (this : Eq (α := ℤ) (coeff X 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
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
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
⊢ Eq (α := ℤ) 1 0
have neg₂ : ∀ (this : Eq (α := ℤ) (if Eq (α := ℕ) 1 1 then 1 else 0) 0), Eq (α := ℤ) 1 0
Tactic: rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] 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
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
⊢ Eq (α := ℤ) 1 0
have neg₃ : ∀ (this : 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
Cleared hypotheses: this
-- 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: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
⊢ p ∈ s
have haveI₃ : ∀ (this : 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
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
⊢ p ∈ s
have haveI₄ : ∀ (this : 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
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
⊢ p ∈ s
have haveI₅ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
  p ∈ s
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
⊢ p ∈ s
have pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
⊢ p ∈ s
have neg : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
neg neg₁ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
⊢ p ∈ s
have neg₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), False
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
neg neg₁ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
neg₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), False
⊢ p ∈ s
have neg₃ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])),
  Eq (α := ℤ) 1 0
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
haveI haveI₁ haveI₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s), p ∈ s
haveI₃ :
  ∀ (this : 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
haveI₄ :
  ∀ (this : 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
haveI₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) (if p ∈ s then 0 else X) (↑n : ℤ[X])),
    p ∈ s
pos : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∈ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) 0 (↑n : ℤ[X])), p ∈ s
neg neg₁ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), p ∈ s
neg₂ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])), False
neg₃ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (this : ∃ (n : ℤ), Eq (α := ℤ[X]) X (↑n : ℤ[X])),
    Eq (α := ℤ) 1 0
⊢ p ∈ s
have neg₄ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
Tactic: classical
  haveI := Classical.decPred (· ∈ s)
  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
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this