awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
| (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑(k + 1) : R)
have rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: rhs; rw [← Nat.mod_add_div (k + 1) 2]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑(k + 1) : R)
have pos : (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
  else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
  (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have pos : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
⊢ Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have pos : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(0 + 2 * ((k + 1) / 2)) : R)
Tactic: rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
pos : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(0 + 2 * ((k + 1) / 2)) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have pos₁ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(2 * ((k + 1) / 2)) : R)
Tactic: rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
pos : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(0 + 2 * ((k + 1) / 2)) : R)
pos₁ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(2 * ((k + 1) / 2)) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have pos₂ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(1 * ((k + 1) / 2) + (k + 1) / 2) : R)
Tactic: rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : (k + 1) % 2 = 0
pos : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(0 + 2 * ((k + 1) / 2)) : R)
pos₁ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(2 * ((k + 1) / 2)) : R)
pos₂ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑(1 * ((k + 1) / 2) + (k + 1) / 2) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have pos₃ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((k + 1) / 2 + (k + 1) / 2) : R)
Tactic: rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
| (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑(k + 1) : R)
have rhs : (↑(k + 1) : R)
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
| (↑(k + 1) : R)
have rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: rw [← Nat.mod_add_div (k + 1) 2]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
| (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑(k + 1) : R)
have rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: rhs; rw [← Nat.mod_add_div (k + 1) 2]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑(k + 1) : R)
have neg : (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
  else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
  (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast
    else HAdd.hAdd (α := R) ((k + 1) / 2).binCast ((k + 1) / 2).binCast + 1) =
    (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have neg : HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
Tactic: rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (hypothesis)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
⊢ HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have h1 : k.succ % 2 = 1
Tactic: have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
have neg : HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) / 2 + (k + 1) / 2 + 1) : R)
Tactic: rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
⊢ Eq.{u_1 + 1} (α := R) k.binCast (↑k : R)
have ind : ∀ (hk : ∀ (m : ℕ), m < 0 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)), Eq.{u_1 + 1} (α := R) (Nat.binCast 0) (↑0 : R)
Tactic: cases k with
  | zero => rw [Nat.binCast, Nat.cast_zero]
  | succ k =>
      rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
ind :
  ∀ (hk : ∀ (m : ℕ), m < 0 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)), Eq.{u_1 + 1} (α := R) (Nat.binCast 0) (↑0 : R)
⊢ Eq.{u_1 + 1} (α := R) k.binCast (↑k : R)
have ind₁ : ∀ (k : ℕ) (hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)),
  Eq.{u_1 + 1} (α := R) (k + 1).binCast (↑(k + 1) : R)
Tactic: cases k with
  | zero => rw [Nat.binCast, Nat.cast_zero]
  | succ k =>
      rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
⊢ (n + 1).binCast = HAdd.hAdd (α := R) n.binCast 1
have rw : (↑(n + 1) : R) = HAdd.hAdd (α := R) n.binCast 1
Tactic: rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
rw : (↑(n + 1) : R) = HAdd.hAdd (α := R) n.binCast 1
⊢ (n + 1).binCast = HAdd.hAdd (α := R) n.binCast 1
have rw₁ : (↑(n + 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : One R
n : ℕ
this : AddMonoidWithOne R := AddMonoidWithOne.unary
rw : (↑(n + 1) : R) = HAdd.hAdd (α := R) n.binCast 1
rw₁ : (↑(n + 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1
⊢ (n + 1).binCast = HAdd.hAdd (α := R) n.binCast 1
have rw₂ : HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := R) 1 1 = 2
have rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 2
Tactic: rw [← Nat.cast_one, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 2
have h : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: apply congrArg
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := R) 2 1 = 3
have rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : R) 3
Tactic: rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : R) 3
have h : HAdd.hAdd (α := ℕ) 1 1 + 1 = 3
Tactic: apply congrArg
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := R) 3 1 = 4
have rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1 + 1) : R) 4
Tactic: rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one,
    ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1 + 1) : R) 4
have h : HAdd.hAdd (α := ℕ) 1 1 + 1 + 1 = 4
Tactic: apply congrArg
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
hnm : n ∣ m
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have obtain : ∀ (k : ℕ), (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
Tactic: obtain ⟨k, rfl⟩ := hnm
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (hypothesis)
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
have this : n ≠ 0
Tactic: have : n ≠ 0 := by rintro rfl; simp at hn
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
this : n ≠ 0
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
have rw : (↑k : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
Tactic: rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
this : n ≠ 0
rw : (↑k : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
have rw₁ : (↑k : K) = HDiv.hDiv (α := K) (↑(k * n) : K) (↑n : K)
Tactic: rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
this : n ≠ 0
rw : (↑k : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
rw₁ : (↑k : K) = HDiv.hDiv (α := K) (↑(k * n) : K) (↑n : K)
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
have rw₂ : (↑k : K) = HMul.hMul (α := K) (↑k : K) (↑n : K) / (↑n : K)
Tactic: rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
this : n ≠ 0
rw : (↑k : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
rw₁ : (↑k : K) = HDiv.hDiv (α := K) (↑(k * n) : K) (↑n : K)
rw₂ : (↑k : K) = HMul.hMul (α := K) (↑k : K) (↑n : K) / (↑n : K)
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
have rw₃ : Eq.{u_1 + 1} (α := K) (↑k : K) (↑k : K)
Tactic: rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
inst_1 : CharZero K
hnm : n ∣ m
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have inl : ∀ (hnm : 0 ∣ m), (↑(m / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑0 : K)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
inst_1 : CharZero K
hnm : n ∣ m
inl : ∀ (hnm : 0 ∣ m), (↑(m / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑0 : K)
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have inr : ∀ (hn : n ≠ 0), (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
⊢ HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have inl : ∀ (hn : 0 ∣ n) (hm : 0 ∣ m), HDiv.hDiv (α := K) (↑(m / 0) : K) (↑(n / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
Cleared hypotheses: d, hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
inl :
  ∀ (hn : 0 ∣ n) (hm : 0 ∣ m), HDiv.hDiv (α := K) (↑(m / 0) : K) (↑(n / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
⊢ HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have inr : ∀ (hd : d ≠ 0), HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
Tactic: rcases eq_or_ne d 0 with (rfl | hd)
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ Ne.{u_1 + 1} (α := K) (↑d : K) 0
have norm_cast : ¬d = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Field (hypothesis)
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
have hd₁ : Ne.{u_1 + 1} (α := K) (↑d : K) 0
Tactic: replace hd : (d : K) ≠ 0 := by norm_cast
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.NeZero (hypothesis)
Goal:
n : ℕ
inst : NeZero n
⊢ 1 ≤ n
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑n : α) (↑(n + 1) : α)
have rw : (↑n : α) ≤ HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1
have apply : 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1
Tactic: apply zero_lt_one.trans_le
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1
have h : Eq.{u_1 + 1} (α := α) 1 (↑1 : α)
Tactic: convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
h : Eq.{u_1 + 1} (α := α) 1 (↑1 : α)
⊢ 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1
have h₁ : HAdd.hAdd (α := α) (↑n : α) 1 = (↑(n + 1) : α)
Tactic: convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
h : Eq.{u_1 + 1} (α := α) 1 (↑1 : α)
h₁ : HAdd.hAdd (α := α) (↑n : α) 1 = (↑(n + 1) : α)
⊢ 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1
have convert! : 1 ≤ n + 1
Tactic: convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α) ↔ 0 < n
have zero : LT.lt.{u_1} (α := α) 0 (↑0 : α) ↔ LT.lt (α := ℕ) 0 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
zero : LT.lt.{u_1} (α := α) 0 (↑0 : α) ↔ LT.lt (α := ℕ) 0 0
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α) ↔ 0 < n
have succ : ∀ (n : ℕ), LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α) ↔ 0 < n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LT.lt.{u_1} (α := α) 1 (↑n : α) ↔ 1 < n
have rw : LT.lt.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 < n
Tactic: rw [← cast_one, cast_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 < n
⊢ LT.lt.{u_1} (α := α) 1 (↑n : α) ↔ 1 < n
have rw₁ : 1 < n ↔ 1 < n
Tactic: rw [← cast_one, cast_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LE.le.{u_1} (α := α) 1 (↑n : α) ↔ 1 ≤ n
have rw : LE.le.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 ≤ n
Tactic: rw [← cast_one, cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LE.le.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 ≤ n
⊢ LE.le.{u_1} (α := α) 1 (↑n : α) ↔ 1 ≤ n
have rw₁ : 1 ≤ n ↔ 1 ≤ n
Tactic: rw [← cast_one, cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LT.lt.{u_1} (α := α) (↑n : α) 1 ↔ n = 0
have rw : LT.lt.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n = 0
Tactic: rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n = 0
⊢ LT.lt.{u_1} (α := α) (↑n : α) 1 ↔ n = 0
have rw₁ : n < 1 ↔ n = 0
Tactic: rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n = 0
rw₁ : n < 1 ↔ n = 0
⊢ LT.lt.{u_1} (α := α) (↑n : α) 1 ↔ n = 0
have rw₂ : n ≤ 0 ↔ n = 0
Tactic: rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n = 0
rw₁ : n < 1 ↔ n = 0
rw₂ : n ≤ 0 ↔ n = 0
⊢ LT.lt.{u_1} (α := α) (↑n : α) 1 ↔ n = 0
have rw₃ : n = 0 ↔ n = 0
Tactic: rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑n : α) 1 ↔ n ≤ 1
have rw : LE.le.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n ≤ 1
Tactic: rw [← cast_one, cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LE.le.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n ≤ 1
⊢ LE.le.{u_1} (α := α) (↑n : α) 1 ↔ n ≤ 1
have rw₁ : n ≤ 1 ↔ n ≤ 1
Tactic: rw [← cast_one, cast_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Order.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑n : α) 0 ↔ n = 0
have norm_cast : n ≤ 0 ↔ n = 0
Tactic: norm_cast