[GOAL]
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_2
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ ↑q ^ n = 1 ↔ q = 1
[PROOFSTEP]
rw [← cast_pow, cast_eq_one]
[GOAL]
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_2
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ q ^ n = 1 ↔ q = 1
[PROOFSTEP]
exact pow_eq_one_iff hn
[GOAL]
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m : ℕ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_2
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
exact cast_div n_dvd (cast_ne_zero.2 hn)
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 2 ≠ 0
[PROOFSTEP]
have : ((2 : ℕ) : M) ≠ 0 := Nat.cast_ne_zero.2 (by decide)
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 2 ≠ 0
[PROOFSTEP]
decide
[GOAL]
M : Type u_1
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
this : ↑2 ≠ 0
⊢ 2 ≠ 0
[PROOFSTEP]
rwa [Nat.cast_two] at this 
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ a + a = 0 ↔ a = 0
[PROOFSTEP]
simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or_iff]
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ 0 = bit0 a ↔ a = 0
[PROOFSTEP]
rw [eq_comm]
[GOAL]
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a✝ a : R
⊢ bit0 a = 0 ↔ a = 0
[PROOFSTEP]
exact bit0_eq_zero
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
⊢ n = 0 ∨ a = b
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h 
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h✝ : ↑n * a = ↑n * b
h : ↑n = 0 ∨ a = b
⊢ n = 0 ∨ a = b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
w : n ≠ 0
⊢ a = b
[PROOFSTEP]
simpa [w] using nat_mul_inj h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
[PROOFSTEP]
dsimp [bit0] at h 
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : a + a = b + b
⊢ a = b
[PROOFSTEP]
simp only [(two_mul a).symm, (two_mul b).symm] at h 
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : 2 * a = 2 * b
⊢ a = b
[PROOFSTEP]
refine' nat_mul_inj' _ two_ne_zero
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : 2 * a = 2 * b
⊢ ↑2 * a = ↑2 * b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit1 a = bit1 b
⊢ a = b
[PROOFSTEP]
simp only [bit1, add_left_inj] at h 
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
[PROOFSTEP]
exact bit0_injective h
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ bit1 a = 1 ↔ a = 0
[PROOFSTEP]
rw [show (1 : R) = bit1 0 by simp, bit1_eq_bit1]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ 1 = bit1 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ 1 = bit1 a ↔ a = 0
[PROOFSTEP]
rw [eq_comm]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ bit1 a = 1 ↔ a = 0
[PROOFSTEP]
exact bit1_eq_one
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ (a + a) / 2 = a
[PROOFSTEP]
rw [← mul_two, mul_div_cancel a two_ne_zero]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a / 2 + a / 2 = a
[PROOFSTEP]
rw [← add_div, half_add_self]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a - a / 2 = a / 2
[PROOFSTEP]
rw [sub_eq_iff_eq_add, add_halves']
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
a : R
⊢ a / 2 - a = -(a / 2)
[PROOFSTEP]
rw [← neg_sub, sub_half]
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h 
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
m n : ℕ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h 
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hS : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ↑a = ↑b
[PROOFSTEP]
rw [← map_natCast ϕ, ← map_natCast ϕ, h]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
⊢ Function.Injective Nat.cast
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
[PROOFSTEP]
rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]
