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
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
neg₄ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
⊢ p ∈ s
have neg₅ : ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ) (H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))),
  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
neg₄ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ) (H : Eq (α := ℤ[X]) X (↑w : ℤ[X])), Eq (α := ℤ) 1 0
neg₅ :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s) (h : p ∉ s) (w : ℤ)
    (H : Eq (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) (↑w : ℤ))), Eq (α := ℤ) 1 0
⊢ p ∈ s
have neg₆ : ∀ (this : 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
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
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
have refine_1 : Eq (α := FreeCommRing α)
  ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) 1))
  1
Tactic: refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
refine_1 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) 1))
    1
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
have refine_2 : Eq (α := FreeCommRing α)
  ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (-1)))
  (-1)
Tactic: refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
refine_1 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) 1))
    1
refine_2 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (-1)))
    (-1)
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
have refine_3 : ∀ z ∈ of '' s,
  ∀ (n : FreeCommRing α),
    (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
        n →
      (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (z * n)) =
        z * n
Tactic: refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
refine_1 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) 1))
    1
refine_2 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (-1)))
    (-1)
refine_3 :
  ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
            ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
          n →
        (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
            ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (z * n)) =
          z * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
have refine_4 : ∀ {x y : FreeCommRing α},
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
      x →
    (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) =
        y →
      (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (x + y)) =
        x + y
Tactic: refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3 : (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
  of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3₁ : (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := 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))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
  of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₁ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := 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))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3₂ : (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    (HMul.hMul (β := FreeCommRing (↑s : Type u)) (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
  of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₁ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := 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))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₂ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (β := FreeCommRing (↑s : Type u)) (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3₃ : HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps)) :
      FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
      FreeCommRing α) =
  of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₁ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := 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))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₂ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (β := FreeCommRing (↑s : Type u)) (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₃ :
  HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps)) :
        FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
        FreeCommRing α) =
    of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3₄ : HMul.hMul (β := FreeCommRing α) (of (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps) : α))
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
      FreeCommRing α) =
  of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : 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 (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₁ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := 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))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₂ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (β := FreeCommRing (↑s : Type u)) (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₃ :
  HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps)) :
        FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
        FreeCommRing α) =
    of p * n
refine_3₄ :
  HMul.hMul (β := FreeCommRing α) (of (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps) : α))
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
        FreeCommRing α) =
    of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n
have refine_3₅ : of (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps) : α) * n = of p * n
Tactic: rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]