awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
h : Eq (α := Fin 4) (Fin.ofNat 4 n) 1
⊢ (match (motive := Fin 4 → ℕ) 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 1 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
have rw : (n + 1 ^^^
    match (motive := Fin 4 → ℕ) 1 with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0) =
  match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 1 (Fin.ofNat 4 1) with
  | 0 => n + 1
  | 1 => 1
  | 2 => n + 1 + 1
  | 3 => 0
Tactic: rw [Nat.xor_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
h : Eq (α := Fin 4) (Fin.ofNat 4 n) 1
⊢ (n + 1 ^^^
      match (motive := Fin 4 → ℕ) 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 1 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
have refine : (n + 1) % 2 = 0
Tactic: refine xor_one_of_even <| even_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
h : Eq (α := Fin 4) (Fin.ofNat 4 n) 1
⊢ (n + 1) % 2 = 0
have rw : ((↑1 : ℕ) % 2 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
Tactic: rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
have zero : Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (HAdd.hAdd (α := ℕ) 0 1)))
  (match (motive := Fin 4 → ℕ) Fin.ofNat 4 0 with
  | 0 => 0
  | 1 => 1
  | 2 => HAdd.hAdd (α := ℕ) 0 1
  | 3 => 0)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    nth_rw 3 [← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..]
    rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]
    match h : Fin.ofNat 4 n with
    | 0 =>
      rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]
      rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 1 =>
      rw [Nat.xor_comm]
      refine xor_one_of_even <| even_iff.mpr ?_
      rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 2 =>
      apply Nat.xor_self
    | 3 =>
      apply zero_xor
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
zero :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (HAdd.hAdd (α := ℕ) 0 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 0 with
    | 0 => 0
    | 1 => 1
    | 2 => HAdd.hAdd (α := ℕ) 0 1
    | 3 => 0)
⊢ Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
have succ : ∀ (n : ℕ)
  (ih :
    Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
      (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0)),
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 (n + 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    nth_rw 3 [← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..]
    rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]
    match h : Fin.ofNat 4 n with
    | 0 =>
      rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]
      rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 1 =>
      rw [Nat.xor_comm]
      refine xor_one_of_even <| even_iff.mpr ?_
      rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]
      rfl
    | 2 =>
      apply Nat.xor_self
    | 3 =>
      apply zero_xor
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
⊢ y <<< n ||| x < HPow.hPow (α := ℕ) 2 (n + m)
have left : y <<< n < HPow.hPow (α := ℕ) 2 (n + m)
Tactic: apply bitwise_lt_two_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
left : y <<< n < HPow.hPow (α := ℕ) 2 (n + m)
⊢ y <<< n ||| x < HPow.hPow (α := ℕ) 2 (n + m)
have right : x < HPow.hPow (α := ℕ) 2 (n + m)
Tactic: apply bitwise_lt_two_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
⊢ y <<< n < HPow.hPow (α := ℕ) 2 (n + m)
have left : y <<< n < HPow.hPow (α := ℕ) 2 (m + n)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : ℕ
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have zero : (↑(m * 0) : α) = HMul.hMul (α := α) (↑m : α) (↑0 : α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : ℕ
zero : (↑(m * 0) : α) = HMul.hMul (α := α) (↑m : α) (↑0 : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have succ : ∀ (n : ℕ),
  (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α) →
    (↑(m * (n + 1)) : α) = HMul.hMul (α := α) (↑m : α) (↑(n + 1) : α)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
have zero : 0 = a * (↑0 : α)
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
zero : 0 = a * (↑0 : α)
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
have zero₁ : 0 = a * 0
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
zero : 0 = a * (↑0 : α)
zero₁ : 0 = a * 0
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
have zero₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [zero_nsmul, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * (↑n : α)
⊢ (n + 1) • a = a * (↑(n + 1) : α)
have succ : n • a + a = a * (↑(n + 1) : α)
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * (↑n : α)
succ : n • a + a = a * (↑(n + 1) : α)
⊢ (n + 1) • a = a * (↑(n + 1) : α)
have succ₁ : a * (↑n : α) + a = a * (↑(n + 1) : α)
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * (↑n : α)
succ : n • a + a = a * (↑(n + 1) : α)
succ₁ : a * (↑n : α) + a = a * (↑(n + 1) : α)
⊢ (n + 1) • a = a * (↑(n + 1) : α)
have succ₂ : a * (↑n : α) + a = a * HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * (↑n : α)
succ : n • a + a = a * (↑(n + 1) : α)
succ₁ : a * (↑n : α) + a = a * (↑(n + 1) : α)
succ₂ : a * (↑n : α) + a = a * HAdd.hAdd (α := α) (↑n : α) 1
⊢ (n + 1) • a = a * (↑(n + 1) : α)
have succ₃ : a * (↑n : α) + a = a * (↑n : α) + a * 1
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * (↑n : α)
succ : n • a + a = a * (↑(n + 1) : α)
succ₁ : a * (↑n : α) + a = a * (↑(n + 1) : α)
succ₂ : a * (↑n : α) + a = a * HAdd.hAdd (α := α) (↑n : α) 1
succ₃ : a * (↑n : α) + a = a * (↑n : α) + a * 1
⊢ (n + 1) • a = a * (↑(n + 1) : α)
have succ₄ : a * (↑n : α) + a = a * (↑n : α) + a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * (↑n : α)
have zero : HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
Tactic: induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
⊢ n • a = a * (↑n : α)
have succ : ∀ (n : ℕ) (ih : n • a = a * (↑n : α)), (n + 1) • a = a * (↑(n + 1) : α)
Tactic: induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
m n : ℕ
⊢ (↑(m ^ (n + 1)) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
have rw : (↑(m * m ^ n) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
Tactic: rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
m n : ℕ
rw : (↑(m * m ^ n) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
⊢ (↑(m ^ (n + 1)) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
have rw₁ : (↑(m * m ^ n) : α) = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
Tactic: rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
m n : ℕ
rw : (↑(m * m ^ n) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
rw₁ : (↑(m * m ^ n) : α) = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
⊢ (↑(m ^ (n + 1)) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
have rw₂ : HMul.hMul (α := α) (↑m : α) (↑(m ^ n) : α) = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
Tactic: rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
α : Type u_1
inst : Semiring α
m n : ℕ
rw : (↑(m * m ^ n) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
rw₁ : (↑(m * m ^ n) : α) = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
rw₂ : HMul.hMul (α := α) (↑m : α) (↑(m ^ n) : α) = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
⊢ (↑(m ^ (n + 1)) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)
have rw₃ : (↑m : α) * HPow.hPow (α := α) (↑m : α) n = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
Tactic: rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
A : Type u_3
F : Type u_5
inst : FunLike F ℕ A
inst_1 : AddMonoidWithOne A
inst_2 : AddMonoidHomClass F ℕ A
f : F
h1 : Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) (1 : A)
n : ℕ
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((↑(n + 1) : A) : A)
have rw : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) ((f : (a : ℕ) → A) 1 : A) = (↑(n + 1) : A)
Tactic: rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
A : Type u_3
F : Type u_5
inst : FunLike F ℕ A
inst_1 : AddMonoidWithOne A
inst_2 : AddMonoidHomClass F ℕ A
f : F
h1 : Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) (1 : A)
n : ℕ
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) ((f : (a : ℕ) → A) 1 : A) = (↑(n + 1) : A)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((↑(n + 1) : A) : A)
have rw₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) (1 : A) = (↑(n + 1) : A)
Tactic: rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
A : Type u_3
F : Type u_5
inst : FunLike F ℕ A
inst_1 : AddMonoidWithOne A
inst_2 : AddMonoidHomClass F ℕ A
f : F
h1 : Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) (1 : A)
n : ℕ
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) ((f : (a : ℕ) → A) 1 : A) = (↑(n + 1) : A)
rw₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) (1 : A) = (↑(n + 1) : A)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((↑(n + 1) : A) : A)
have rw₂ : HAdd.hAdd (α := A) (↑n : A) 1 = (↑(n + 1) : A)
Tactic: rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
A : Type u_3
F : Type u_5
inst : FunLike F ℕ A
inst_1 : AddMonoidWithOne A
inst_2 : AddMonoidHomClass F ℕ A
f : F
h1 : Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) (1 : A)
n : ℕ
rw : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) ((f : (a : ℕ) → A) 1 : A) = (↑(n + 1) : A)
rw₁ : HAdd.hAdd (α := A) (β := A) ((f : (a : ℕ) → A) n : A) (1 : A) = (↑(n + 1) : A)
rw₂ : HAdd.hAdd (α := A) (↑n : A) 1 = (↑(n + 1) : A)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((↑(n + 1) : A) : A)
have rw₃ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (↑n : A) 1
Tactic: rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Basic (goal)
Goal:
A : Type u_3
F : Type u_4
inst : MulZeroOneClass A
inst_1 : FunLike F ℕ A
inst_2 : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)
⊢ f = g
have h : ∀ (x : ℕ), Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) x : A) ((g : (a : ℕ) → A) x : A)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Commute (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
⊢ Commute (↑0 : α) x
have zero : Commute 0 x
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Commute (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n : α) x
⊢ Commute (↑(n + 1) : α) x
have succ : Commute (HAdd.hAdd (α := α) (↑n : α) 1) x
Tactic: rw [Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Commute (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n : α) x
have zero : Commute (↑0 : α) x
Tactic: induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Commute (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
x : α
zero : Commute (↑0 : α) x
⊢ Commute (↑n : α) x
have succ : ∀ (n : ℕ) (ihn : Commute (↑n : α) x), Commute (↑(n + 1) : α) x
Tactic: induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
P : Prop
inst_1 : Decidable P
m n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(if P then m else n) : R) (if P then (↑m : R) else (↑n : R))
have pos : P → Eq.{u_1 + 1} (α := R) (↑m : R) (↑m : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
P : Prop
inst_1 : Decidable P
m n : ℕ
pos : P → Eq.{u_1 + 1} (α := R) (↑m : R) (↑m : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(if P then m else n) : R) (if P then (↑m : R) else (↑n : R))
have neg : ¬P → Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1
have rw : HAdd.hAdd (α := R) (↑0 : R) 1 = 1
Tactic: rw [cast_succ, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : HAdd.hAdd (α := R) (↑0 : R) 1 = 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1
have rw₁ : HAdd.hAdd (α := R) 0 1 = 1
Tactic: rw [cast_succ, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : HAdd.hAdd (α := R) (↑0 : R) 1 = 1
rw₁ : HAdd.hAdd (α := R) 0 1 = 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [cast_succ, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
have succ : (↑(m + n).succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
Tactic: rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
succ : (↑(m + n).succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
have succ₁ : HAdd.hAdd (α := R) (↑(m + n) : R) 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
Tactic: rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
succ : (↑(m + n).succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₁ : HAdd.hAdd (α := R) (↑(m + n) : R) 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
have succ₂ : HAdd.hAdd (α := R) (↑m : R) (↑n : R) + 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
Tactic: rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
succ : (↑(m + n).succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₁ : HAdd.hAdd (α := R) (↑(m + n) : R) 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₂ : HAdd.hAdd (α := R) (↑m : R) (↑n : R) + 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
have succ₃ : HAdd.hAdd (α := R) (↑m : R) (↑n : R) + 1 = (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
succ : (↑(m + n).succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₁ : HAdd.hAdd (α := R) (↑(m + n) : R) 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₂ : HAdd.hAdd (α := R) (↑m : R) (↑n : R) + 1 = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
succ₃ : HAdd.hAdd (α := R) (↑m : R) (↑n : R) + 1 = (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
have succ₄ : (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
⊢ (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
have zero : (↑(m + 0) : R) = HAdd.hAdd (α := R) (↑m : R) (↑0 : R)
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
zero : (↑(m + 0) : R) = HAdd.hAdd (α := R) (↑m : R) (↑0 : R)
⊢ (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)
have succ : ∀ (n : ℕ) (ih : (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)),
  (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) n.binCast (↑n : R)
have ind : ∀ (k : ℕ) (hk : ∀ (m : ℕ), m < k → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)), Eq.{u_1 + 1} (α := R) k.binCast (↑k : R)
Tactic: induction n using Nat.strongRecOn with | ind k hk => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
hk : ∀ (m : ℕ), m < 0 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
⊢ Eq.{u_1 + 1} (α := R) (Nat.binCast 0) (↑0 : R)
have ind : Eq.{u_1 + 1} (α := R) 0 (↑0 : R)
Tactic: rw [Nat.binCast, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Cast.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
hk : ∀ (m : ℕ), m < 0 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
ind : Eq.{u_1 + 1} (α := R) 0 (↑0 : R)
⊢ Eq.{u_1 + 1} (α := R) (Nat.binCast 0) (↑0 : R)
have ind₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Nat.binCast, Nat.cast_zero]
-- 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)
⊢ Eq.{u_1 + 1} (α := R) (k + 1).binCast (↑(k + 1) : R)
have ind : (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)
Tactic: rw [Nat.binCast]
-- 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)
⊢ (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 : ∀ (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)
Tactic: by_cases h : (k + 1) % 2 = 0
-- 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)
pos :
  ∀ (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)
⊢ (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 : ∀ (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)
Tactic: by_cases h : (k + 1) % 2 = 0
-- 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]