awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : Odd (α := ℕ) 0
⊢ HXor.hXor (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
exact not_odd_zero h |>.elim

Premises used: False.elim, Nat.not_odd_zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : Odd (n + 1)
succ :
  (if n + 1 = 0 then if (false != true) = true then 1 else 0
    else
      if Eq (α := ℕ) 1 0 then if (true != false) = true then n + 1 else 0
      else
        if (decide ((n + 1) % 2 = 1) != decide True) = true then
          ((if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) + 1
        else (if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) =
    n + 1 - 1
⊢ n + 1 ^^^ 1 = n + 1 - 1

Tactic:
simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]

Premises used: Nat.instXorOp, Nat.bitwise, HXor.hXor, Nat.xor, Nat.reduceDiv, Nat.bitwise_zero_right
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : Odd (n + 1)
⊢ (if n + 1 = 0 then if (false != true) = true then 1 else 0
    else
      if Eq (α := ℕ) 1 0 then if (true != false) = true then n + 1 else 0
      else
        if (decide ((n + 1) % 2 = 1) != decide True) = true then
          ((if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) + 1
        else (if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) =
    n + 1 - 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : Odd n
zero : ∀ (h : Odd (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
succ : ∀ (n : ℕ) (h : Odd (n + 1)), n + 1 ^^^ 1 = n + 1 - 1
⊢ n ^^^ 1 = n - 1

Tactic:
cases n with
  | zero =>
    exact not_odd_zero h |>.elim
  | succ n =>
    simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]
    grind

Premises used: Nat.instXorOp, Nat.bitwise, HXor.hXor, Nat.xor, Nat.zero, Nat.reduceDiv, Nat.bitwise_zero_right, Nat.succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ 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:
simp
-- Module: Mathlib.Data.Nat.Bitwise
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)
succ :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 (n + (↑(Fin.ofNat 4 1) : ℕ)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 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:
nth_rw 3 [← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..]

Premises used: OfNat.ofNat, Fin.val_ofNat
-- Module: Mathlib.Data.Nat.Bitwise
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)
succ :
  (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) (Fin.ofNat 4 n) (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 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 + (↑(Fin.ofNat 4 1) : ℕ)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0)

Tactic:
rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]

Premises used: List.foldl_nil, List.foldl_append, List.foldl_cons, Fin.ofNat_add, List.range_succ
-- Module: Mathlib.Data.Nat.Bitwise
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) 0
rw : n % 2 = 0
⊢ (match (motive := Fin 4 → ℕ) 0 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 0 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]

Premises used: Iff.mpr, Fin.zero_add, Nat.xor_xor_cancel_left, Nat.even_iff, Nat.xor_one_of_even
-- Module: Mathlib.Data.Nat.Bitwise
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) 0
⊢ Dvd.dvd (α := ℕ) 2 4

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
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) 0
rw : (↑0 : ℕ) % 2 = 0
⊢ n % 2 = 0

Tactic:
rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]

Premises used: Nat.mod_mod_of_dvd, OfNat.ofNat, Fin.val_ofNat
-- Module: Mathlib.Data.Nat.Bitwise
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) 0
⊢ (↑0 : ℕ) % 2 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
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
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
⊢ (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

Tactic:
rw [Nat.xor_comm]

Premises used: Nat.xor_comm
-- Module: Mathlib.Data.Nat.Bitwise
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

Tactic:
xor_one_of_even <| even_iff.mpr ?_

Premises used: Iff.mpr, Nat.even_iff, Nat.xor_one_of_even
-- Module: Mathlib.Data.Nat.Bitwise
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
refine : (n + 1) % 2 = 0
⊢ (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:
refine xor_one_of_even <| even_iff.mpr ?_

Premises used: Iff.mpr, Nat.even_iff, Nat.xor_one_of_even
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ Dvd.dvd (α := ℕ) 2 4

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
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
rw : ((↑1 : ℕ) % 2 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
⊢ (n + 1) % 2 = 0

Tactic:
rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]

Premises used: Nat.mod_mod_of_dvd, Nat.add_mod, OfNat.ofNat, Fin.val_ofNat
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ ((↑1 : ℕ) % 2 + HMod.hMod (α := ℕ) 1 2) % 2 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
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) 2
⊢ (match (motive := Fin 4 → ℕ) 2 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 2 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
apply Nat.xor_self

Premises used: Nat.xor_self
-- Module: Mathlib.Data.Nat.Bitwise
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) 3
⊢ (match (motive := Fin 4 → ℕ) 3 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 3 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
apply zero_xor

Premises used: Nat.zero_xor
-- Module: Mathlib.Data.Nat.Bitwise
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)
⊢ (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) (Fin.ofNat 4 n) (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
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
-- Module: Mathlib.Data.Nat.Bitwise
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)
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)
⊢ 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)

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

Premises used: List.foldl_nil, List.foldl_append, List.foldl_cons, Nat.zero, OfNat.ofNat, Nat.succ, Fin.ofNat_add, Fin.val_ofNat, List.range_succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
x n m : ℕ
h : x < HPow.hPow (α := ℕ) 2 n
⊢ x <<< m < HPow.hPow (α := ℕ) 2 (n + m)

Tactic:
simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]

Premises used: Nat.shiftLeft_eq, Nat.pow_add, Nat.two_pow_pos, Nat.mul_lt_mul_right
-- Module: Mathlib.Data.Nat.Bitwise
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)
right : x < HPow.hPow (α := ℕ) 2 (n + m)
⊢ y <<< n ||| x < HPow.hPow (α := ℕ) 2 (n + m)

Tactic:
apply bitwise_lt_two_pow

Premises used: Nat.bitwise_lt_two_pow
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
left : y <<< n < HPow.hPow (α := ℕ) 2 (m + n)
⊢ y <<< n < HPow.hPow (α := ℕ) 2 (n + m)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
⊢ y <<< n < HPow.hPow (α := ℕ) 2 (m + n)

Tactic:
apply shiftLeft_lt hy

Premises used: Nat.shiftLeft_lt
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
x y n m : ℕ
hx : x < HPow.hPow (α := ℕ) 2 n
hy : y < HPow.hPow (α := ℕ) 2 m
⊢ x < HPow.hPow (α := ℕ) 2 (n + m)

Tactic:
apply lt_of_lt_of_le hx <| Nat.pow_le_pow_right (le_succ _) (le_add_right _ _)

Premises used: Nat.le_add_right, Nat.le_succ, Nat.pow_le_pow_right, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
⊢ Eq (α := (a : ℕ) → α) (⇑(castAddMonoidHom α) : (a : ℕ) → α) Nat.cast

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
hn : Even n
⊢ Even.{u_1} (α := α) (↑n : α)

Tactic:
hn.map <| Nat.castAddMonoidHom α

Premises used: Nat.castAddMonoidHom, Even.map
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : ℕ
zero : (↑(m * 0) : α) = HMul.hMul (α := α) (↑m : α) (↑0 : α)
succ :
  ∀ (n : ℕ),
    (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α) →
      (↑(m * (n + 1)) : α) = HMul.hMul (α := α) (↑m : α) (↑(n + 1) : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
m : ℕ
⊢ (↑(m * 0) : α) = HMul.hMul (α := α) (↑m : α) (↑0 : α)

Tactic:
simp [mul_add, *]

Premises used: mul_add
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : ℕ
h : (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * (n + 1)) : α) = HMul.hMul (α := α) (↑m : α) (↑(n + 1) : α)

Tactic:
simp [mul_add, *]

Premises used: mul_add
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
⊢ Eq (α := (a : ℕ) → α) (⇑(castRingHom α) : (a : ℕ) → α) Nat.cast

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
zero : 0 = a * (↑0 : α)
zero₁ : 0 = a * 0
zero₂ zero₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, zero_nsmul, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.Basic
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
succ₄ succ₅ : a * (↑n : α) + a = a * (↑n : α) + a
⊢ (n + 1) • a = a * (↑(n + 1) : α)

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

Premises used: Nat.cast_succ, mul_add, mul_one, succ_nsmul
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
a : α
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : α)
succ : ∀ (n : ℕ) (ih : n • a = a * (↑n : α)), (n + 1) • a = a * (↑(n + 1) : α)
⊢ n • a = a * (↑n : α)

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]

Premises used: Nat.cast_succ, MulZeroClass.mul_zero, zero_nsmul, Nat.zero, mul_add, Nat.cast_zero, mul_one, Nat.succ, succ_nsmul
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : ℕ
inst_1 : n.AtLeastTwo
a : α
⊢ HSMul.hSMul (α := ℕ) (OfNat.ofNat n) a = OfNat.ofNat n * a

Tactic:
simp [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : Semiring α
m : ℕ
⊢ (↑(HPow.hPow (β := ℕ) m 0) : α) = HPow.hPow (α := α) (β := ℕ) (↑m : α) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Basic
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
rw₃ rw₄ : (↑m : α) * HPow.hPow (α := α) (↑m : α) n = (↑m : α) * HPow.hPow (α := α) (↑m : α) n
⊢ (↑(m ^ (n + 1)) : α) = HPow.hPow (α := α) (↑m : α) (n + 1)

Tactic:
rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

Premises used: Nat.cast_mul, pow_succ'
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
α : Type u_1
inst : Semiring α
m n : ℕ
h : m ∣ n
⊢ Dvd.dvd.{u_1} (α := α) (↑m : α) (↑n : α)

Tactic:
map_dvd (Nat.castRingHom α) h

Premises used: map_dvd, Nat.castRingHom
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((↑0 : A) : A)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
rw₃ rw₄ : HAdd.hAdd (α := A) (↑n : A) 1 = HAdd.hAdd (α := A) (↑n : A) 1
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((↑(n + 1) : A) : A)

Tactic:
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

Premises used: map_add, Nat.cast_add_one
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
B : Type u_4
F : Type u_5
inst : AddMonoidWithOne B
A : Type u_6
inst_1 : AddMonoidWithOne A
inst_2 : FunLike F A B
inst_3 : AddMonoidHomClass F A B
f : F
h : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
⊢ Eq (α := B) ((AddMonoidHom.comp (↑f : A →+ B) (Nat.castAddMonoidHom A) : (a : ℕ) → B) 1 : B) (1 : B)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
B : Type u_4
F : Type u_5
inst : AddMonoidWithOne B
A : Type u_6
inst_1 : AddMonoidWithOne A
inst_2 : FunLike F A B
inst_3 : AddMonoidHomClass F A B
f : F
h : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (OfNat.ofNat n) : B) (OfNat.ofNat n : B)

Tactic:
map_natCast' f h n

Premises used: map_natCast'
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
h : ∀ (x : ℕ), Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) x : A) ((g : (a : ℕ) → A) x : A)
⊢ f = g

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
n : ℕ
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((g : (a : ℕ) → A) (n + 1) : A)

Tactic:
h_pos n.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Cast.Basic
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)
n : ℕ
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((g : (a : ℕ) → A) (n + 1) : A)

Tactic:
exact h_pos n.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
A : Type u_3
inst : MulZeroOneClass A
f g : ℕ →*₀ A
⊢ (∀ {n : ℕ}, 0 < n → Eq (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)) → f = g

Tactic:
ext_nat'' f g

Premises used: ext_nat''
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_3
F : Type u_5
inst : NonAssocSemiring R
inst_1 : FunLike F ℕ R
inst_2 : RingHomClass F ℕ R
f : F
⊢ ∀ (n : ℕ), Eq.{u_3 + 1} (α := R) ((f : (a : ℕ) → R) n : R) ((↑n : R) : R)

Tactic:
eq_natCast' f <| map_one f

Premises used: map_one, eq_natCast'
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
⊢ ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)

Tactic:
map_natCast' f <| map_one f

Premises used: map_one, map_natCast'
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (OfNat.ofNat n) : S) (OfNat.ofNat n : S)

Tactic:
map_natCast f n

Premises used: map_natCast
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_3
F : Type u_5
inst : NonAssocSemiring R
inst_1 : FunLike F ℕ R
inst_2 : RingHomClass F ℕ R
f g : F
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : ℕ) → R) 1 : R) ((g : (a : ℕ) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_6
S : Type u_7
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
F : Type u_8
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
n : ℕ
hn : NeZero.{u_7} (R := S) (↑n : S)
⊢ NeZero.{u_7} (R := S) ((f : (a : R) → S) (↑n : R) : S)

Tactic:
simp only [map_natCast, hn]

Premises used: map_natCast
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
R : Type u_3
inst : NonAssocSemiring R
f : ℕ →+* R
⊢ f = Nat.castRingHom R

Tactic:
RingHom.ext <| eq_natCast f

Premises used: RingHom.ext, eq_natCast
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
n : ℕ
⊢ (↑n : ℕ) = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Cast.Basic
Goal:
⊢ castRingHom ℕ = RingHom.id ℕ

Tactic:
rfl

Premises used: rfl