[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * zero) = ↑m * ↑zero
[PROOFSTEP]
simp [mul_succ, mul_add, *]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m n✝ : ℕ
n_ih✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * succ n✝) = ↑m * ↑(succ n✝)
[PROOFSTEP]
simp [mul_succ, mul_add, *]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x
[PROOFSTEP]
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)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x
[PROOFSTEP]
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)
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑zero) x
[PROOFSTEP]

| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑zero) x
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
[PROOFSTEP]
exact Commute.zero_left x
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(succ n)) x
[PROOFSTEP]

| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(succ n)) x
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x
[PROOFSTEP]
exact ihn.add_left (Commute.one_left x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1
[PROOFSTEP]
exact le_add_of_nonneg_right zero_le_one
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n ↔ 0 < n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ 0 < ↑zero ↔ 0 < zero
[PROOFSTEP]
simp [cast_add_one_pos]
  -- without this more specific version Lean often chokes
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(succ n✝) ↔ 0 < succ n✝
[PROOFSTEP]
simp [cast_add_one_pos]
  -- without this more specific version Lean often chokes
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ 1 < ↑n ↔ 1 < n
[PROOFSTEP]
rw [← cast_one, cast_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ 1 ≤ ↑n ↔ 1 ≤ n
[PROOFSTEP]
rw [← cast_one, cast_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ ↑n < 1 ↔ n = 0
[PROOFSTEP]
rw [← cast_one, cast_lt, lt_succ_iff, ← bot_eq_zero, le_bot_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ ↑n ≤ 1 ↔ n ≤ 1
[PROOFSTEP]
rw [← cast_one, cast_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
cases' le_total m n with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
rw [tsub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n
[PROOFSTEP]
exact mono_cast h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n
[PROOFSTEP]
rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ∀ (x : ℕ), ↑f x = ↑g x
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
induction n with
| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
induction n with
| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]

| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]
simp_rw [Nat.zero_eq, map_zero f, map_zero g]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
ihn : ↑f n = ↑g n
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]

| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
ihn : ↑f n = ↑g n
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]
simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
⊢ ↑f 0 = ↑0
[PROOFSTEP]
simp [map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
n : ℕ
⊢ ↑f (n + 1) = ↑(n + 1)
[PROOFSTEP]
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
[GOAL]
α : Type u_1
β : Type u_2
A✝ : Type u_3
B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_6
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
⊢ ↑f ↑0 = ↑0
[PROOFSTEP]
simp [map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
A✝ : Type u_3
B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_6
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
n : ℕ
⊢ ↑f ↑(n + 1) = ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_add, map_add, Nat.cast_add, map_natCast' f h n, Nat.cast_one, h, Nat.cast_one]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ f = g
[PROOFSTEP]
apply FunLike.ext
[GOAL]
case h
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ∀ (x : ℕ), ↑f x = ↑g x
[PROOFSTEP]
rintro (_ | n)
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]
simp [map_zero f, map_zero g]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
n : ℕ
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]
exact h_pos n.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : RingHomClass F ℕ R
f g : F
⊢ ↑f 1 = ↑g 1
[PROOFSTEP]
simp only [map_one f, map_one g]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
n : ℕ
h✝ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ↑f
h : ↑n = 0
⊢ ↑f ↑n = ↑f 0
[PROOFSTEP]
simpa only [map_natCast, map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
S✝ : Type u_4
F✝ : Type u_5
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
R : Type u_6
S : Type u_7
inst✝² : Semiring R
inst✝¹ : Semiring S
F : Type u_8
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (↑f ↑n)
[PROOFSTEP]
simp only [map_natCast, hn]
