awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r
have simp : (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
  (↑(k.choose ij.1) : R) * (s - HSMul.hSMul (β := R) ij.2 1) +
    (↑(k.choose ij.2) : R) * (r - HSMul.hSMul (β := R) ij.1 1)
Tactic: simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (s - HSMul.hSMul (β := R) ij.2 1) +
      (↑(k.choose ij.2) : R) * (r - HSMul.hSMul (β := R) ij.1 1)
have rw : (r + s - (HSMul.hSMul (β := R) ij.1 1 + HSMul.hSMul (β := R) ij.2 1)) * (↑((ij.1 + ij.2).choose ij.1) : R) =
  (s - HSMul.hSMul (β := R) ij.2 1 + (r - HSMul.hSMul (β := R) ij.1 1)) * (↑((ij.1 + ij.2).choose ij.1) : R)
Tactic: rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have hl : (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
  (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
    (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r
Tactic: have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
hl :
  (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have succ : ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r) *
    (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
  (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
    (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
Tactic: rw [hl, ← add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
hl :
  (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r
succ :
  ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
        (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r) *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
        (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have succ₁ : ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r) *
    (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
  ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r) *
    (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
Tactic: rw [hl, ← add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
k : ℕ
h : Commute r s
⊢ smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have zero : smeval (descPochhammer ℤ 0) (r + s) =
  ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
    (↑(Nat.choose 0 ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, sum_antidiagonal_choose_succ_mul
      fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s),
      ← sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]
    refine sum_congr rfl ?_
    intro ij hij -- try to move `descPochhammer`s to right, gather multipliers.
    have hdx : (descPochhammer ℤ ij.1).smeval r * (X - (ij.2 : ℤ[X])).smeval s =
        (X - (ij.2 : ℤ[X])).smeval s * (descPochhammer ℤ ij.1).smeval r := by
      refine (commute_iff_eq ((descPochhammer ℤ ij.1).smeval r)
        ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_
      exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
    simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
      ← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]
    have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
    rw [hl, ← add_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
k : ℕ
h : Commute r s
zero :
  smeval (descPochhammer ℤ 0) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
      (↑(Nat.choose 0 ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
⊢ smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have succ : ∀ (k : ℕ)
  (ih :
    smeval (descPochhammer ℤ k) (r + s) =
      ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
        (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)),
  smeval (descPochhammer ℤ (k + 1)) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ (k + 1),
      (↑((k + 1).choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, sum_antidiagonal_choose_succ_mul
      fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s),
      ← sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]
    refine sum_congr rfl ?_
    intro ij hij -- try to move `descPochhammer`s to right, gather multipliers.
    have hdx : (descPochhammer ℤ ij.1).smeval r * (X - (ij.2 : ℤ[X])).smeval s =
        (X - (ij.2 : ℤ[X])).smeval s * (descPochhammer ℤ ij.1).smeval r := by
      refine (commute_iff_eq ((descPochhammer ℤ ij.1).smeval r)
        ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_
      exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
    simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
      ← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]
    have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
    rw [hl, ← add_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ choose (r + s) k = ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k, choose r ij.1 * choose s ij.2
have rw : Eq.{u_1 + 1} (α := R)
  (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
    (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s))
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, k.factorial • (choose r x.1 * choose s x.2))
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, smul_sum, descPochhammer_smeval_add _ h]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ Eq.{u_1 + 1} (α := R)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, k.factorial • (choose r x.1 * choose s x.2))
have refine : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ k,
  (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
    k.factorial • (choose r x.1 * choose s x.2)
Tactic: refine sum_congr rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
    k.factorial • (choose r x.1 * choose s x.2)
have rw : (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
  HMul.hMul (α := R) (↑(k.choose x.1) : R) (↑x.1.factorial : R) * (choose r x.1 * x.2.factorial • choose s x.2)
Tactic: rw [← Nat.choose_mul_factorial_mul_factorial (antidiagonal.fst_le hx),
    tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm, mul_assoc, nsmul_eq_mul,
    Nat.cast_mul, Nat.cast_mul, ← mul_assoc _ (x.1.factorial : R), mul_assoc _ (x.2.factorial : R),
    ← mul_assoc (x.2.factorial : R), Nat.cast_commute x.2.factorial,
    mul_assoc _ (x.2.factorial : R), ← nsmul_eq_mul x.2.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = a * b
ha : a = p
⊢ IsUnit b
have h₂ : p = p * b
Tactic: rw [ha] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
| p
have rw : p * b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ Associated (p * b) p
have conv_rhs : Associated (p * b) p
Tactic: conv_rhs => rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
conv_rhs : Associated (p * b) p
⊢ Associated (p * b) p
have conv_rhs₁ : Associated (p * b) (p * b)
Tactic: conv_rhs => rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb_1 : ¬p ∣ b
hb : IsUnit b
⊢ b = ⊥
have rwa : ∀ (hb : b = 1), b = ⊥
Tactic: rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb_1 : ¬p ∣ b
hb : IsUnit b
rwa : ∀ (hb : b = 1), b = ⊥
⊢ b = ⊥
have rwa₁ : ∀ (hb : b = ⊥), b = ⊥
Tactic: rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * (↑ha.unit⁻¹ : Associates M)
have rw : b = b * a * (↑ha.unit⁻¹ : Associates M)
Tactic: rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
rw : b = b * a * (↑ha.unit⁻¹ : Associates M)
⊢ b = p * (↑ha.unit⁻¹ : Associates M)
have rw₁ : b = b * (a * (↑ha.unit⁻¹ : Associates M))
Tactic: rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
rw : b = b * a * (↑ha.unit⁻¹ : Associates M)
rw₁ : b = b * (a * (↑ha.unit⁻¹ : Associates M))
⊢ b = p * (↑ha.unit⁻¹ : Associates M)
have rw₂ : b = b * 1
Tactic: rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
h : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
rw : b = b * a * (↑ha.unit⁻¹ : Associates M)
rw₁ : b = b * (a * (↑ha.unit⁻¹ : Associates M))
rw₂ : b = b * 1
⊢ b = p * (↑ha.unit⁻¹ : Associates M)
have rw₃ : b = b
Tactic: rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ∃ (c : Fin (n + 1) → Associates M),
    c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ (i : Fin (n + 1)), r = c i
have refine_1 : (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) 1 = p
Tactic: refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
refine_1 : (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) 1 = p
⊢ ∃ (c : Fin (n + 1) → Associates M),
    c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ (i : Fin (n + 1)), r = c i
have refine_2 : ∀ (n_1 m : Fin (n + 1)) (h : n_1 < m),
  LT.lt.{u_1} (α := Associates M) ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) n_1)
    ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) m)
Tactic: refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
refine_1 : (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) 1 = p
refine_2 :
  ∀ (n_1 m : Fin (n + 1)) (h : n_1 < m),
    LT.lt.{u_1} (α := Associates M) ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) n_1)
      ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) m)
⊢ ∃ (c : Fin (n + 1) → Associates M),
    c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ (i : Fin (n + 1)), r = c i
have refine_3 : ∀ (y : Associates M) (h : y ≤ p ^ n), ∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i
Tactic: refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
refine_1 : (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) 1 = p
refine_2 :
  ∀ (n_1 m : Fin (n + 1)) (h : n_1 < m),
    LT.lt.{u_1} (α := Associates M) ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) n_1)
      ((fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) m)
refine_3 : ∀ (y : Associates M) (h : y ≤ p ^ n), ∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i
⊢ ∃ (c : Fin (n + 1) → Associates M),
    c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ (i : Fin (n + 1)), r = c i
have refine_4 : ∀ (y : Associates M), (∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i) → y ≤ p ^ n
Tactic: refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ (↑1 : ℕ) = p
have refine_1 : 1 < n + 1
Tactic: rw [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
⊢ ∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i
have refine_3 : ∀ (i : ℕ) (i_le : i ≤ n) (hi : Associated y (p ^ i)), ∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i
Tactic: obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : Associated y (p ^ i)
⊢ ∃ (i : Fin (n + 1)), y = (fun (i : Fin (n + 1)) ↦ p ^ (↑i : ℕ)) i
have hi₁ : y = p ^ i
Tactic: rw [associated_iff_eq] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
⊢ IsUnit (c 0)
have obtain : ∀ (i : Fin (n + 1)) (hr : 1 = c i), IsUnit (c 0)
Tactic: obtain ⟨i, hr⟩ := h₂.mp one_le
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ IsUnit (c 0)
have rw : c 0 ≤ c i
Tactic: rw [Associates.isUnit_iff_eq_one, ← Associates.le_one_iff, hr]
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hq : q ≠ 0
⊢ Irreducible (c 1)
have zero : ∀ (hn : Ne (α := ℕ) 0 0) {c : Fin (HAdd.hAdd (α := ℕ) 0 1) → Associates M} (h₁ : StrictMono c)
  (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), r = c i), Irreducible (c 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn, c, h₁, h₂