awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
zero : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S 0)) (Set.Ici (HSub.hSub (α := S) (↑0 : S) 1))
⊢ MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
have succ : ∀ (n : ℕ)
  (ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))),
  MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S (n + 1))) (Set.Ici (HSub.hSub (α := S) (↑(n + 1) : S) 1))
Tactic: induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
    have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
    simp_rw [descPochhammer_succ_eval]
    exact mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S))
      (sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)
have rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)
have rw₁ : (↑(a.choose b * b !) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)
have rw₂ : (↑(b ! * a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)
have rw₃ : (↑(a.descFactorial b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₃ : (↑(a.descFactorial b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)
have rw₄ : Eq.{u_1 + 1} (α := K) (↑(a.descFactorial b) : K) (↑(a.descFactorial b) : K)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)
have rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)
have rw₁ : (↑(a.choose b * b !) : K) = eval (↑a : K) (descPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑a : K) (descPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)
have rw₂ : (↑(b ! * a.choose b) : K) = eval (↑a : K) (descPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑a : K) (descPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑a : K) (descPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)
have rw₃ : (↑(a.descFactorial b) : K) = eval (↑a : K) (descPochhammer K b)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑a : K) (descPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑a : K) (descPochhammer K b)
rw₃ : (↑(a.descFactorial b) : K) = eval (↑a : K) (descPochhammer K b)
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)
have rw₄ : Eq.{u_1 + 1} (α := K) (↑(a.descFactorial b) : K) (↑(a.descFactorial b) : K)
Tactic: rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Eq (α := Ideal R[X])
    (Ideal.span
      (insert (α := R[X]) ((C : (a : R) → R[X]) x : R[X])
        {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
have rw : Eq (α := Ideal R[X])
  (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])) ⊔
    Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})
  (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
    Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
Tactic: rw [Ideal.span_insert, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
rw :
  Eq (α := Ideal R[X])
    (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])) ⊔
      Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
⊢ Eq (α := Ideal R[X])
    (Ideal.span
      (insert (α := R[X]) ((C : (a : R) → R[X]) x : R[X])
        {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
have rw₁ : Eq (α := Ideal R[X])
  (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
    Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
  (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
    Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
Tactic: rw [Ideal.span_insert, sup_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Eq (α := Ideal R)
    (Ideal.map (R :=
      HasQuotient.Quotient R[X] (B := Ideal R[X])
        (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
      (F :=
      HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) →+*
        R)
      (↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R)
      (Ideal.map (R := R[X]) (F :=
        R[X] →ₐ[R]
          HasQuotient.Quotient R[X] (B := Ideal R[X])
            (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
        (Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
        (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))))
    (Ideal.span {x})
have simp : Eq (α := Ideal R)
  (Ideal.span
    (singleton (α := R)
      (((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
            (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
          ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
                (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
              ((C : (a : R) → R[X]) x) :
            HasQuotient.Quotient R[X] (B := Ideal R[X])
              (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) :
        R)))
  (Ideal.span {x})
Tactic: simp only [Ideal.map_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Eq (α := Ideal R)
    (Ideal.span
      (singleton (α := R)
        (((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
              (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
            ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
                  (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
                ((C : (a : R) → R[X]) x) :
              HasQuotient.Quotient R[X] (B := Ideal R[X])
                (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) :
          R)))
    (Ideal.span {x})
have e_s : ((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
      (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
    ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
          (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
        ((C : (a : R) → R[X]) x) :
      HasQuotient.Quotient R[X] (B := Ideal R[X])
        (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) =
  x
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hq : q.Monic
⊢ p %ₘ q = 0 ↔
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
have rw : q ∣ p ↔
  Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
    ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
    (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
Tactic: rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hq : q.Monic
rw :
  q ∣ p ↔
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
⊢ p %ₘ q = 0 ↔
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
have rw₁ : q ∣ p ↔ q ∣ p
Tactic: rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C : (a : R) → R[X] ⧸ map C I) a :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
have rw : Membership.mem (α := R[X]) (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) ((C : (a : R) → R[X]) a : R[X])
Tactic: rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
⊢ Eq (α := (R ⧸ I)[X]) ((eval₂RingHom (RingHom.comp C (Quotient.mk I)) X : (a : R[X]) → (R ⧸ I)[X]) a : (R ⧸ I)[X])
    (0 : (R ⧸ I)[X])
have rw : Eq (α := (R ⧸ I)[X])
  ((eval₂RingHom (RingHom.comp C (Quotient.mk I)) X : (a : R[X]) → (R ⧸ I)[X])
    (a.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a))
  0
Tactic: rw [← sum_monomial_eq a]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (a.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) = 0
have rw : Eq (α := (R ⧸ I)[X])
  (a.sum fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) 0
Tactic: rw [eval₂_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
⊢ Eq (α := (R ⧸ I)[X])
    (a.sum fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) 0
have refine : ∀ n ∈ a.support,
  Eq.{u_1 + 1} (α := (R ⧸ I)[X])
    ((fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) n (a.coeff n)) 0
Tactic: refine Finset.sum_eq_zero fun n _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) (a.coeff n)) = 0
have rw : HMul.hMul (α := (R ⧸ I)[X]) ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n) : (R ⧸ I)[X])
    (HPow.hPow (α := (R ⧸ I)[X]) X n) =
  0
Tactic: rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
⊢ HMul.hMul (α := (R ⧸ I)[X]) ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n) : (R ⧸ I)[X])
      (HPow.hPow (α := (R ⧸ I)[X]) X n) =
    0
have refine : ∀ (m : ℕ),
  Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n)) m) (coeff 0 m)
Tactic: refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
m : ℕ
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n)) m) (coeff 0 m)
have rw : Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
Tactic: rw [RingHom.comp_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
m : ℕ
⊢ Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
have pos : ∀ (h : m = 0),
  Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
m : ℕ
pos :
  ∀ (h : m = 0),
    Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
⊢ Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
have neg : ∀ (h : ¬m = 0),
  Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        f) =
    f
have refine_1 : ∀ (p q : (R ⧸ I)[X]),
  (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) sorry :
          (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          p) =
      p →
    (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) sorry :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            q) =
        q →
      (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) sorry :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            (p + q)) =
        p + q
Tactic: refine Polynomial.induction_on' f ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
refine_1 :
  ∀ (p q : (R ⧸ I)[X]),
    (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            p) =
        p →
      (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
              (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
            ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              q) =
          q →
        (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
              (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
            ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              (p + q)) =
          p + q
⊢ (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        f) =
    f
have refine_2 : ∀ (n : ℕ) (a : R ⧸ I),
  Eq (α := (R ⧸ I)[X])
    ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) sorry :
          (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) a)) :
      (R ⧸ I)[X])
    ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) a : (R ⧸ I)[X])
Tactic: refine Polynomial.induction_on' f ?_ ?_