awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
π : α → Type u_3
inst : (a : α) → NatCast (π a)
n : ℕ
a : α
⊢ Eq.{u_3 + 1} (α := π a) ((↑n : (a : α) → π a) a) (↑n : π a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
π : α → Type u_3
inst : (a : α) → NatCast (π a)
n : ℕ
⊢ Eq (α := (a : α) → π a) (↑n : (a : α) → π a) fun (x : α) ↦ (↑n : π x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
π : α → Type u_3
n : ℕ
inst : (i : α) → OfNat (π i) n
a : α
⊢ Eq.{u_3 + 1} (α := π a) ((OfNat.ofNat n : (a : α) → π a) a) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
π : α → Type u_3
n : ℕ
inst : (i : α) → OfNat (π i) n
⊢ Eq (α := (a : α) → π a) (OfNat.ofNat n) fun (x : α) ↦ OfNat.ofNat n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : NatCast γ
n : ℕ
⊢ Eq (α := α ⊕ β → γ) (Sum.elim (↑n : α → γ) (↑n : β → γ)) (↑n : α ⊕ β → γ)

Tactic:
Sum.elim_lam_const_lam_const (γ := γ) n

Premises used: Nat.cast, Sum.elim_lam_const_lam_const
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
zero : Commute 0 x
⊢ Commute (↑0 : α) x

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
⊢ Commute 0 x

Tactic:
Commute.zero_left x

Premises used: Commute.zero_left
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
⊢ Commute 0 x

Tactic:
exact Commute.zero_left x

Premises used: Commute.zero_left
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n : α) x
succ : Commute (HAdd.hAdd (α := α) (↑n : α) 1) x
⊢ Commute (↑(n + 1) : α) x

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n : α) x
⊢ Commute (HAdd.hAdd (α := α) (↑n : α) 1) x

Tactic:
ihn.add_left (Commute.one_left x)

Premises used: Commute.add_left, Commute.one_left
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n : α) x
⊢ Commute (HAdd.hAdd (α := α) (↑n : α) 1) x

Tactic:
exact ihn.add_left (Commute.one_left x)

Premises used: Commute.add_left, Commute.one_left
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
x : α
zero : Commute (↑0 : α) x
succ : ∀ (n : ℕ) (ihn : Commute (↑n : α) x), Commute (↑(n + 1) : α) x
⊢ Commute (↑n : α) 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)

Premises used: Nat.cast_succ, Commute.zero_left, Nat.zero, Nat.cast_zero, Nat.succ
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
inst_1 : n.AtLeastTwo
x : α
⊢ Commute (OfNat.ofNat n) x

Tactic:
n.cast_commute x

Premises used: Nat.cast_commute
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
x : α
⊢ (↑n : α) * x = x * (↑n : α)

Tactic:
(cast_commute n x).eq

Premises used: Commute.eq, Nat.cast_commute
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
⊢ Commute x (↑n : α)

Tactic:
(n.cast_commute x).symm

Premises used: Commute.symm, Nat.cast_commute
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : NonAssocSemiring α
x : α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Commute x (OfNat.ofNat n)

Tactic:
n.commute_cast x

Premises used: Nat.commute_cast
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a x y : α
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a ((↑n : α) * x) ((↑n : α) * y)

Tactic:
SemiconjBy.mul_right (Nat.commute_cast _ _) h

Premises used: Nat.commute_cast, SemiconjBy.mul_right
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a x y : α
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy ((↑n : α) * a) x y

Tactic:
SemiconjBy.mul_left (Nat.cast_commute _ _) h

Premises used: SemiconjBy.mul_left, Nat.cast_commute
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a x y : α
h : SemiconjBy a x y
m n : ℕ
⊢ SemiconjBy ((↑m : α) * a) ((↑n : α) * x) ((↑n : α) * y)

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a b : α
h : Commute a b
n : ℕ
⊢ Commute a ((↑n : α) * b)

Tactic:
SemiconjBy.natCast_mul_right h n

Premises used: Commute, SemiconjBy.natCast_mul_right
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a b : α
h : Commute a b
n : ℕ
⊢ Commute ((↑n : α) * a) b

Tactic:
SemiconjBy.natCast_mul_left h n

Premises used: Commute, SemiconjBy.natCast_mul_left
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a b : α
h : Commute a b
m n : ℕ
⊢ Commute ((↑m : α) * a) ((↑n : α) * b)

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a : α
n : ℕ
⊢ Commute a ((↑n : α) * a)

Tactic:
(Commute.refl a).natCast_mul_right n

Premises used: Commute.natCast_mul_right, Commute.refl
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a : α
n : ℕ
⊢ Commute ((↑n : α) * a) a

Tactic:
(Commute.refl a).natCast_mul_left n

Premises used: Commute.natCast_mul_left, Commute.refl
-- Module: Mathlib.Data.Nat.Cast.Commute
Goal:
α : Type u_1
inst : Semiring α
a : α
m n : ℕ
⊢ Commute ((↑m : α) * a) ((↑n : α) * a)

Tactic:
(Commute.refl a).natCast_mul_natCast_mul m n

Premises used: Commute.refl, Commute.natCast_mul_natCast_mul
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
n : ℕ
inst : NatCast R
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (↑(OfNat.ofNat n) : R) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
AddMonoidWithOne.natCast_zero

Premises used: AddMonoidWithOne.natCast_zero
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
⊢ (↑n.succ : R) = HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
AddMonoidWithOne.natCast_succ _

Premises used: AddMonoidWithOne.natCast_succ
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
⊢ (↑(n + 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
cast_succ _

Premises used: Nat.cast_succ
-- Module: Mathlib.Data.Nat.Cast.Defs
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)
neg : ¬P → Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(if P then m else n) : R) (if P then (↑m : R) else (↑n : R))

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
P : Prop
inst_1 : Decidable P
m n : ℕ
h : P
⊢ Eq.{u_1 + 1} (α := R) (↑m : R) (↑m : R)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
P : Prop
inst_1 : Decidable P
m n : ℕ
h : ¬P
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : HAdd.hAdd (α := R) (↑0 : R) 1 = 1
rw₁ : HAdd.hAdd (α := R) 0 1 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
rw [cast_succ, Nat.cast_zero, zero_add]

Premises used: Nat.cast_succ, zero_add, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m : ℕ
⊢ (↑(m + 0) : R) = HAdd.hAdd (α := R) (↑m : R) (↑0 : R)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Defs
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
succ₄ succ₅ : (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R) + HAdd.hAdd (α := R) (↑n : R) 1
⊢ (↑(m + (n + 1)) : R) = HAdd.hAdd (α := R) (↑m : R) (↑(n + 1) : R)

Tactic:
rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

Premises used: Nat.cast_succ, add_assoc, Nat.add_succ
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m n : ℕ
zero : (↑(m + 0) : R) = HAdd.hAdd (α := R) (↑m : R) (↑0 : R)
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)
⊢ (↑(m + n) : R) = HAdd.hAdd (α := R) (↑m : R) (↑n : R)

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

Premises used: Nat.cast_succ, add_assoc, Nat.add_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Cast.Defs
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)

Tactic:
?_
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
ind :
  ∀ (k : ℕ) (hk : ∀ (m : ℕ), m < k → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)), Eq.{u_1 + 1} (α := R) k.binCast (↑k : R)
⊢ Eq.{u_1 + 1} (α := R) n.binCast (↑n : R)

Tactic:
induction n using Nat.strongRecOn with | ind k hk => ?_
-- Module: Mathlib.Data.Nat.Cast.Defs
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)
ind₁ ind₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (Nat.binCast 0) (↑0 : R)

Tactic:
rw [Nat.binCast, Nat.cast_zero]

Premises used: Nat.binCast, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → Eq.{u_1 + 1} (α := R) m.binCast (↑m : R)
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)
⊢ Eq.{u_1 + 1} (α := R) (k + 1).binCast (↑(k + 1) : R)

Tactic:
rw [Nat.binCast]

Premises used: Nat.binCast
-- Module: Mathlib.Data.Nat.Cast.Defs
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)
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)
⊢ (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

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rhs : (↑(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)

Tactic:
rhs
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
| (↑(k + 1) : R)

Tactic:
rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : 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)

Tactic:
rhs; rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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 :
  (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)
⊢ (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:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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) (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : 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) % 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]

Premises used: Nat.le_refl, Nat.div_lt_self, if_pos, Nat.cast_add, Nat.succ_pos, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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)
pos₃ pos₄ : Eq.{u_1 + 1} (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) (↑((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)

Tactic:
rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]

Premises used: Nat.succ_mul, Nat.zero_add, Nat.one_mul
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rhs : (↑(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)

Tactic:
rhs
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)
| (↑(k + 1) : R)

Tactic:
rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rw : (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : 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)

Tactic:
rhs; rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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
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)
⊢ (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:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]

Premises used: Nat.mod_add_div, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Cast.Defs
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
neg : HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : 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) % 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]

Premises used: Nat.le_refl, Nat.div_lt_self, Nat.cast_add, Nat.succ_pos, OfNat.ofNat, if_neg
-- Module: Mathlib.Data.Nat.Cast.Defs
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.succ % 2 = 1

Tactic:
have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
-- Module: Mathlib.Data.Nat.Cast.Defs
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
neg : HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) / 2 + (k + 1) / 2 + 1) : R)
⊢ HAdd.hAdd (α := R) (↑((k + 1) / 2 + (k + 1) / 2) : R) 1 = (↑((k + 1) % 2 + 2 * ((k + 1) / 2)) : R)

Tactic:
rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]

Premises used: Nat.succ_mul, OfNat.ofNat, Nat.one_mul, Nat.add_comm
-- Module: Mathlib.Data.Nat.Cast.Defs
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 + (k + 1) / 2 + 1) : R)

Tactic:
simp only [Nat.cast_add, Nat.cast_one]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Defs
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)
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)
⊢ Eq.{u_1 + 1} (α := R) k.binCast (↑k : 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]

Premises used: Nat.le_refl, Nat.div_lt_self, Nat.cast_add, Nat.mod_add_div, Nat.succ_mul, HAdd.hAdd, Nat.succ_pos, Nat.zero, Nat.binCast, Nat.cast_zero, Nat.zero_add, OfNat.ofNat, Nat.succ, Nat.cast_one, Nat.one_mul, Nat.add_comm
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : NatCast R
⊢ Eq.{u_1 + 1} (α := R) (↑2 : R) 2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : NatCast R
⊢ Eq.{u_1 + 1} (α := R) (↑3 : R) 3

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : NatCast R
⊢ Eq.{u_1 + 1} (α := R) (↑4 : R) 4

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : One R
⊢ Eq.{u_1 + 1} (α := R) (Nat.binCast 0) 0

Tactic:
simp only [Nat.binCast]

Premises used: Nat.binCast
-- Module: Mathlib.Data.Nat.Cast.Defs
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
rw₂ rw₃ : HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1
⊢ (n + 1).binCast = HAdd.hAdd (α := R) n.binCast 1

Tactic:
rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ]

Premises used: Nat.cast_succ, Nat.binCast_eq
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 2
⊢ HAdd.hAdd (α := R) 1 1 = 2

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 2

Tactic:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := ℕ) 1 1 = 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : R) 3
⊢ HAdd.hAdd (α := R) 2 1 = 3

Tactic:
rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]

Premises used: one_add_one_eq_two, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h : HAdd.hAdd (α := ℕ) 1 1 + 1 = 3
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : R) 3

Tactic:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := ℕ) 1 1 + 1 = 3

Tactic:
decide
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
rw : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1 + 1) : R) 4
⊢ HAdd.hAdd (α := R) 3 1 = 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]

Premises used: one_add_one_eq_two, Nat.cast_add, two_add_one_eq_three, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h : HAdd.hAdd (α := ℕ) 1 1 + 1 + 1 = 4
⊢ Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1 + 1) : R) 4

Tactic:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := ℕ) 1 1 + 1 + 1 = 4

Tactic:
decide
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
⊢ HAdd.hAdd (α := R) 2 2 = 4

Tactic:
simp [← one_add_one_eq_two, ← Nat.cast_one, ← three_add_one_eq_four,
    ← two_add_one_eq_three, add_assoc]

Premises used: add_assoc, three_add_one_eq_four, one_add_one_eq_two, two_add_one_eq_three, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
A : Type u_2
inst : AddMonoidWithOne A
⊢ HSMul.hSMul (α := ℕ) (β := A) 0 1 = (↑0 : A)

Tactic:
simp [zero_nsmul]

Premises used: zero_nsmul
-- Module: Mathlib.Data.Nat.Cast.Defs
Goal:
A : Type u_2
inst : AddMonoidWithOne A
n : ℕ
⊢ HSMul.hSMul (β := A) (n + 1) 1 = (↑(n + 1) : A)

Tactic:
simp [succ_nsmul, nsmul_one n]

Premises used: succ_nsmul
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
hnm : n ∣ m
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
obtain : ∀ (k : ℕ), (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
obtain ⟨k, rfl⟩ := hnm

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
k : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑0 : K) 0
⊢ False

Tactic:
simp at hn