[GOAL]
⊢ CharZero ℤ
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val a < n
[PROOFSTEP]
cases n
[GOAL]
case zero
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ val a < Nat.zero
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ val a < Nat.succ n✝
[PROOFSTEP]
exact Fin.is_lt a
[GOAL]
n a : ℕ
⊢ val ↑a = a % n
[PROOFSTEP]
cases n
[GOAL]
case zero
a : ℕ
⊢ val ↑a = a % Nat.zero
[PROOFSTEP]
rw [Nat.mod_zero]
[GOAL]
case zero
a : ℕ
⊢ val ↑a = a
[PROOFSTEP]
exact Int.natAbs_ofNat a
[GOAL]
case succ
a n✝ : ℕ
⊢ val ↑a = a % Nat.succ n✝
[PROOFSTEP]
rw [← Fin.ofNat_eq_val]
[GOAL]
case succ
a n✝ : ℕ
⊢ val (Fin.ofNat'' a) = a % Nat.succ n✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
[PROOFSTEP]
intro k
[GOAL]
n k : ℕ
⊢ ↑k = 0 ↔ n ∣ k
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
k : ℕ
⊢ ↑k = 0 ↔ Nat.zero ∣ k
[PROOFSTEP]
simp [zero_dvd_iff, Int.coe_nat_eq_zero, Nat.zero_eq]
[GOAL]
case succ
k n : ℕ
⊢ ↑k = 0 ↔ Nat.succ n ∣ k
[PROOFSTEP]
rw [Fin.eq_iff_veq]
[GOAL]
case succ
k n : ℕ
⊢ ↑↑k = ↑0 ↔ Nat.succ n ∣ k
[PROOFSTEP]
show (k : ZMod (n + 1)).val = (0 : ZMod (n + 1)).val ↔ _
[GOAL]
case succ
k n : ℕ
⊢ val ↑k = val 0 ↔ Nat.succ n ∣ k
[PROOFSTEP]
rw [val_nat_cast, val_zero, Nat.dvd_iff_mod_eq_zero]
[GOAL]
a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑a = n / Nat.gcd n a
[PROOFSTEP]
cases' a with a
[GOAL]
case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑Nat.zero = n / Nat.gcd n Nat.zero
case succ n : ℕ n0 : n ≠ 0 a : ℕ ⊢ addOrderOf ↑(Nat.succ a) = n / Nat.gcd n (Nat.succ a)
[PROOFSTEP]
simp [Nat.pos_of_ne_zero n0]
[GOAL]
case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(Nat.succ a) = n / Nat.gcd n (Nat.succ a)
[PROOFSTEP]
rw [← Nat.smul_one_eq_coe, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]
[GOAL]
a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf ↑a = n / Nat.gcd n a
[PROOFSTEP]
rw [← Nat.smul_one_eq_coe, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]
[GOAL]
n : ℕ
⊢ ringChar (ZMod n) = n
[PROOFSTEP]
rw [ringChar.eq_iff]
[GOAL]
n : ℕ
⊢ CharP (ZMod n) n
[PROOFSTEP]
exact ZMod.charP n
[GOAL]
n : ℕ
⊢ ↑n + 1 = 0
[PROOFSTEP]
rw [← Nat.cast_add_one, nat_cast_self (n + 1)]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑0 = 0
[PROOFSTEP]
delta ZMod.cast
[GOAL]
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.zero with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
[PROOFSTEP]
exact Int.cast_zero
[GOAL]
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero n
a : ZMod n
⊢ ↑a = ↑(val a)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑a = ↑(val a)
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑a = ↑(val a)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ (↑a).fst = ↑a
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod Nat.zero
⊢ (↑a).fst = ↑a
[PROOFSTEP]
rfl
[GOAL]
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
[PROOFSTEP]
simp [ZMod.cast]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ (↑a).snd = ↑a
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod Nat.zero
⊢ (↑a).snd = ↑a
[PROOFSTEP]
rfl
[GOAL]
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).snd = ↑a
[PROOFSTEP]
simp [ZMod.cast]
[GOAL]
n✝ : ℕ
R : Type u_1
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = a
[PROOFSTEP]
cases n
[GOAL]
case zero
n : ℕ
R : Type u_1
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑(val a) = a
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
n : ℕ
R : Type u_1
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑(val a) = a
[PROOFSTEP]
apply Fin.cast_val_eq_self
[GOAL]
n : ℕ
R : Type u_1
a : ZMod n
⊢ ↑↑a = a
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
a : ZMod Nat.zero
⊢ ↑↑a = a
[PROOFSTEP]
simp [ZMod.cast, ZMod]
[GOAL]
case succ
R : Type u_1
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑a = a
[PROOFSTEP]
dsimp [ZMod.cast, ZMod]
[GOAL]
case succ
R : Type u_1
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑(val a) = a
[PROOFSTEP]
erw [Int.cast_ofNat, Fin.cast_val_eq_self]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero n
⊢ Nat.cast ∘ val = cast
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero Nat.zero
⊢ Nat.cast ∘ val = cast
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Nat.cast ∘ val = cast
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast
[PROOFSTEP]
exact congr_arg ((· ∘ ·) Int.cast) ZMod.cast_id'
[GOAL]
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
[PROOFSTEP]
ext
[GOAL]
case succ.h
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (Nat.succ n✝)
⊢ (Int.cast ∘ cast) x✝ = ↑x✝
[PROOFSTEP]
simp [ZMod, ZMod.cast]
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : ZMod n
⊢ ↑(a + b) = if ↑n ≤ ↑a + ↑b then ↑a + ↑b - ↑n else ↑a + ↑b
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
n : ℕ
R : Type u_1
inst✝ : Ring R
a b : ZMod Nat.zero
⊢ ↑(a + b) = if ↑Nat.zero ≤ ↑a + ↑b then ↑a + ↑b - ↑Nat.zero else ↑a + ↑b
[PROOFSTEP]
simp
[GOAL]
case zero
n : ℕ
R : Type u_1
inst✝ : Ring R
a b : ZMod Nat.zero
⊢ ↑(a + b) = ↑a + ↑b
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : ZMod (Nat.succ n)
⊢ ↑(a + b) = if ↑(Nat.succ n) ≤ ↑a + ↑b then ↑a + ↑b - ↑(Nat.succ n) else ↑a + ↑b
[PROOFSTEP]
change Fin (n + 1) at a b
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
⊢ ↑(a + b) = if ↑(Nat.succ n) ≤ ↑a + ↑b then ↑a + ↑b - ↑(Nat.succ n) else ↑a + ↑b
[PROOFSTEP]
change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
⊢ ↑↑(a + b) = if ↑(n + 1) ≤ ↑↑a + ↑↑b then ↑a + ↑b - ↑(Nat.succ n) else ↑a + ↑b
[PROOFSTEP]
simp only [Fin.val_add_eq_ite, Int.ofNat_succ, Int.ofNat_le]
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) = if ↑n + 1 ≤ ↑↑a + ↑↑b then ↑a + ↑b - (↑n + 1) else ↑a + ↑b
[PROOFSTEP]
norm_cast
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) = if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - ↑(n + 1) else ↑a + ↑b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = ↑a + ↑b - ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_sub h]
[GOAL]
case pos
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) - ↑(n + 1) = ↑a + ↑b - ↑(n + 1)
[PROOFSTEP]
congr
[GOAL]
case neg
n✝ : ℕ
R : Type u_1
inst✝ : Ring R
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = ↑a + ↑b
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
⊢ ↑1 = 1
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
⊢ ↑1 = 1
[PROOFSTEP]
exact Int.cast_one
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑1 = 1
[PROOFSTEP]
show ((1 % (n + 1) : ℕ) : R) = 1
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑(1 % (n + 1)) = 1
[PROOFSTEP]
cases n
[GOAL]
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.succ Nat.zero
⊢ ↑(1 % (Nat.zero + 1)) = 1
[PROOFSTEP]
rw [Nat.dvd_one] at h
[GOAL]
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
[PROOFSTEP]
subst m
[GOAL]
case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑(1 % (Nat.succ n✝ + 1)) = 1
[PROOFSTEP]
rw [Nat.mod_eq_of_lt]
[GOAL]
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑1 = 1
[PROOFSTEP]
exact Nat.cast_one
[GOAL]
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ 1 < Nat.succ n✝ + 1
[PROOFSTEP]
exact Nat.lt_of_sub_eq_succ rfl
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ ↑(a + b) = ↑a + ↑b
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
a b : ZMod Nat.zero
⊢ ↑(a + b) = ↑a + ↑b
[PROOFSTEP]
apply Int.cast_add
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(a + b) = ↑a + ↑b
[PROOFSTEP]
symm
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑a + ↑b = ↑(a + b)
[PROOFSTEP]
dsimp [ZMod, ZMod.cast]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(val a) + ↑(val b) = ↑(val (a + b))
[PROOFSTEP]
erw [← Nat.cast_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _), @CharP.cast_eq_zero_iff R _ m]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ m ∣ val a + val b - (val a + val b) % Nat.succ n✝
[PROOFSTEP]
exact h.trans (Nat.dvd_sub_mod _)
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ ↑(a * b) = ↑a * ↑b
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
a b : ZMod Nat.zero
⊢ ↑(a * b) = ↑a * ↑b
[PROOFSTEP]
apply Int.cast_mul
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(a * b) = ↑a * ↑b
[PROOFSTEP]
symm
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑a * ↑b = ↑(a * b)
[PROOFSTEP]
dsimp [ZMod, ZMod.cast]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(val a) * ↑(val b) = ↑(val (a * b))
[PROOFSTEP]
erw [← Nat.cast_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _), @CharP.cast_eq_zero_iff R _ m]
[GOAL]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ m ∣ val a * val b - val a * val b % Nat.succ n✝
[PROOFSTEP]
exact h.trans (Nat.dvd_sub_mod _)
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ Injective ↑(castHom (_ : n ∣ n) R)
[PROOFSTEP]
rw [injective_iff_map_eq_zero]
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), ↑(castHom (_ : n ∣ n) R) a = 0 → a = 0
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ ↑(castHom (_ : n ∣ n) R) x = 0 → x = 0
[PROOFSTEP]
obtain ⟨k, rfl⟩ := ZMod.int_cast_surjective x
[GOAL]
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑(castHom (_ : n ∣ n) R) ↑k = 0 → ↑k = 0
[PROOFSTEP]
rw [map_intCast, CharP.int_cast_eq_zero_iff R n, CharP.int_cast_eq_zero_iff (ZMod n) n]
[GOAL]
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
[PROOFSTEP]
exact id
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ Bijective ↑(castHom (_ : n ∣ n) R)
[PROOFSTEP]
haveI : NeZero n :=
  ⟨by
    intro hn
    rw [hn] at h
    exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ n ≠ 0
[PROOFSTEP]
intro hn
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False
[PROOFSTEP]
rw [hn] at h
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False
[PROOFSTEP]
exact (Fintype.card_eq_zero_iff.mp h).elim' 0
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective ↑(castHom (_ : n ∣ n) R)
[PROOFSTEP]
rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true_iff]
[GOAL]
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ↑(castHom (_ : n ∣ n) R)
[PROOFSTEP]
apply ZMod.castHom_injective
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m = n
⊢ ZMod m ≃+* ZMod n
[PROOFSTEP]
cases' m with m
[GOAL]
case zero
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : Nat.zero = n
⊢ ZMod Nat.zero ≃+* ZMod n
[PROOFSTEP]
cases' n with n
[GOAL]
case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n m : ℕ
h : Nat.succ m = n
⊢ ZMod (Nat.succ m) ≃+* ZMod n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
h : Nat.zero = Nat.zero
⊢ ZMod Nat.zero ≃+* ZMod Nat.zero
[PROOFSTEP]
exact RingEquiv.refl _
[GOAL]
case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : Nat.zero = Nat.succ n
⊢ ZMod Nat.zero ≃+* ZMod (Nat.succ n)
[PROOFSTEP]
exfalso
[GOAL]
case zero.succ.h
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : Nat.zero = Nat.succ n
⊢ False
[PROOFSTEP]
exact n.succ_ne_zero h.symm
[GOAL]
case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : Nat.succ m = Nat.zero
⊢ ZMod (Nat.succ m) ≃+* ZMod Nat.zero
[PROOFSTEP]
exfalso
[GOAL]
case succ.zero.h
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : Nat.succ m = Nat.zero
⊢ False
[PROOFSTEP]
exact m.succ_ne_zero h
[GOAL]
case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
⊢ ZMod (Nat.succ m) ≃+* ZMod (Nat.succ n)
[PROOFSTEP]
exact
  {
    Fin.castIso
      h with
    map_mul' := fun a b => by
      dsimp [ZMod]
      ext
      rw [Fin.coe_castIso, Fin.coe_mul, Fin.coe_mul, Fin.coe_castIso, Fin.coe_castIso, ← h]
    map_add' := fun a b => by
      dsimp [ZMod]
      ext
      rw [Fin.coe_castIso, Fin.val_add, Fin.val_add, Fin.coe_castIso, Fin.coe_castIso, ← h] }
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ Equiv.toFun src✝.toEquiv (a * b) = Equiv.toFun src✝.toEquiv a * Equiv.toFun src✝.toEquiv b
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ ↑(Fin.castIso h) (a * b) = ↑(Fin.castIso h) a * ↑(Fin.castIso h) b
[PROOFSTEP]
ext
[GOAL]
case h
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ ↑(↑(Fin.castIso h) (a * b)) = ↑(↑(Fin.castIso h) a * ↑(Fin.castIso h) b)
[PROOFSTEP]
rw [Fin.coe_castIso, Fin.coe_mul, Fin.coe_mul, Fin.coe_castIso, Fin.coe_castIso, ← h]
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ Equiv.toFun src✝.toEquiv (a + b) = Equiv.toFun src✝.toEquiv a + Equiv.toFun src✝.toEquiv b
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ ↑(Fin.castIso h) (a + b) = ↑(Fin.castIso h) a + ↑(Fin.castIso h) b
[PROOFSTEP]
ext
[GOAL]
case h
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : Nat.succ m = Nat.succ n
src✝ : Fin (Nat.succ m) ≃o Fin (Nat.succ n) := Fin.castIso h
a b : ZMod (Nat.succ m)
⊢ ↑(↑(Fin.castIso h) (a + b)) = ↑(↑(Fin.castIso h) a + ↑(Fin.castIso h) b)
[PROOFSTEP]
rw [Fin.coe_castIso, Fin.val_add, Fin.val_add, Fin.coe_castIso, Fin.coe_castIso, ← h]
[GOAL]
a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]
[PROOFSTEP]
simpa [Int.coe_nat_modEq_iff] using ZMod.int_cast_eq_int_cast_iff a b c
[GOAL]
a : ℤ
b : ℕ
⊢ ↑a = 0 ↔ ↑b ∣ a
[PROOFSTEP]
rw [← Int.cast_zero, ZMod.int_cast_eq_int_cast_iff, Int.modEq_zero_iff_dvd]
[GOAL]
a b : ℤ
c : ℕ
⊢ ↑a = ↑b ↔ ↑c ∣ b - a
[PROOFSTEP]
rw [ZMod.int_cast_eq_int_cast_iff, Int.modEq_iff_dvd]
[GOAL]
a b : ℕ
⊢ ↑a = 0 ↔ b ∣ a
[PROOFSTEP]
rw [← Nat.cast_zero, ZMod.nat_cast_eq_nat_cast_iff, Nat.modEq_zero_iff_dvd]
[GOAL]
n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(val ↑a) = a % ↑n
[PROOFSTEP]
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.coe_nat_nonneg _
[GOAL]
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
⊢ ↑(val ↑a) = a % ↑n
[PROOFSTEP]
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
[GOAL]
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) = a % ↑n
[PROOFSTEP]
refine' (Int.emod_eq_of_lt hle hlt).symm.trans _
[GOAL]
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) % ↑n = a % ↑n
[PROOFSTEP]
rw [← ZMod.int_cast_eq_int_cast_iff', Int.cast_ofNat, ZMod.nat_cast_val, ZMod.cast_id]
[GOAL]
n : ℕ
a : ℤ
⊢ ↑↑a = a % ↑n
[PROOFSTEP]
cases n
[GOAL]
case zero
a : ℤ
⊢ ↑↑a = a % ↑Nat.zero
[PROOFSTEP]
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]
[GOAL]
case zero
a : ℤ
⊢ ↑a = a
[PROOFSTEP]
rfl
[GOAL]
case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a = a % ↑(Nat.succ n✝)
[PROOFSTEP]
rw [← val_int_cast, val]
[GOAL]
case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a =
    ↑((match (motive := (x : ℕ) → ZMod x → ℕ) Nat.succ n✝ with
        | 0 => Int.natAbs
        | Nat.succ n => Fin.val)
        ↑a)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ val (-1) = n
[PROOFSTEP]
dsimp [val, Fin.coe_neg]
[GOAL]
n : ℕ
⊢ ↑(-1) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ ↑(-1) = Nat.zero
[PROOFSTEP]
simp [Nat.mod_one]
[GOAL]
case succ
n✝ : ℕ
⊢ ↑(-1) = Nat.succ n✝
[PROOFSTEP]
dsimp [ZMod, ZMod.cast]
[GOAL]
case succ
n✝ : ℕ
⊢ ↑(-1) = Nat.succ n✝
[PROOFSTEP]
rw [Fin.coe_neg_one]
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1) = ↑n - 1
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑Nat.zero - 1
[PROOFSTEP]
dsimp [ZMod, ZMod.cast]
[GOAL]
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1) = ↑(Nat.succ n) - 1
[PROOFSTEP]
rw [← nat_cast_val, val_neg_one, Nat.cast_succ, add_sub_cancel]
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
⊢ ↑(k - 1) = (if k = 0 then ↑n else ↑k) - 1
[PROOFSTEP]
split_ifs with hk
[GOAL]
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ ↑(k - 1) = ↑n - 1
[PROOFSTEP]
rw [hk, zero_sub, ZMod.cast_neg_one]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
[PROOFSTEP]
cases n
[GOAL]
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
[PROOFSTEP]
dsimp [ZMod, ZMod.cast]
[GOAL]
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
[PROOFSTEP]
rw [Int.cast_sub, Int.cast_one]
[GOAL]
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
[PROOFSTEP]
dsimp [ZMod, ZMod.cast, ZMod.val]
[GOAL]
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1
[PROOFSTEP]
rw [Fin.coe_sub_one, if_neg]
[GOAL]
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1
[PROOFSTEP]
rw [Nat.cast_sub, Nat.cast_one]
[GOAL]
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ 1 ≤ ↑k
[PROOFSTEP]
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
[GOAL]
case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ¬k = 0
[PROOFSTEP]
exact hk
[GOAL]
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = val z + p * k
[PROOFSTEP]
constructor
[GOAL]
case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = val z + p * k
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = val ↑n + p * k
[PROOFSTEP]
refine' ⟨n / p, _⟩
[GOAL]
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = val ↑n + p * (n / p)
[PROOFSTEP]
rw [val_nat_cast, Nat.mod_add_div]
[GOAL]
case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = val z + p * k) → ↑n = z
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(val z + p * k) = z
[PROOFSTEP]
rw [Nat.cast_add, nat_cast_zmod_val, Nat.cast_mul, nat_cast_self, zero_mul, add_zero]
[GOAL]
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = ↑(val z) + ↑p * k
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑(val z) + ↑p * k
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(val ↑n) + ↑p * k
[PROOFSTEP]
refine' ⟨n / p, _⟩
[GOAL]
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(val ↑n) + ↑p * (n / ↑p)
[PROOFSTEP]
rw [val_int_cast, Int.emod_add_ediv]
[GOAL]
case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑(val z) + ↑p * k) → ↑n = z
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑(val z) + ↑p * k) = z
[PROOFSTEP]
rw [Int.cast_add, Int.cast_mul, Int.cast_ofNat, Int.cast_ofNat, nat_cast_val, ZMod.nat_cast_self, zero_mul, add_zero,
  cast_id]
[GOAL]
a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a
[PROOFSTEP]
rw [ZMod.int_cast_eq_int_cast_iff]
[GOAL]
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]
[PROOFSTEP]
apply Int.mod_modEq
[GOAL]
n : ℕ
⊢ AddMonoidHom.ker (Int.castAddHom (ZMod n)) = AddSubgroup.zmultiples ↑n
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ AddMonoidHom.ker (Int.castAddHom (ZMod n)) ↔ x✝ ∈ AddSubgroup.zmultiples ↑n
[PROOFSTEP]
rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom, int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
n : ℕ
⊢ RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}
[PROOFSTEP]
rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom, int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
p n : ℕ
_h : 0 ≤ ↑n
⊢ ↑(Int.toNat ↑n) = ↑↑n
[PROOFSTEP]
simp only [Int.cast_ofNat, Int.toNat_coe_nat]
[GOAL]
p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ ↑(Int.toNat (Int.negSucc n)) = ↑(Int.negSucc n)
[PROOFSTEP]
simp at h
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ Injective val
[PROOFSTEP]
cases n
[GOAL]
case zero
inst✝ : NeZero Nat.zero
⊢ Injective val
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Injective val
[PROOFSTEP]
intro a b h
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
[PROOFSTEP]
ext
[GOAL]
case succ.h
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ ↑a = ↑b
[PROOFSTEP]
exact h
[GOAL]
n : ℕ
⊢ val 1 = 1 % n
[PROOFSTEP]
rw [← Nat.cast_one, val_nat_cast]
[GOAL]
n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1
[PROOFSTEP]
rw [val_one_eq_one_mod]
[GOAL]
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1
[PROOFSTEP]
exact Nat.mod_eq_of_lt Fact.out
[GOAL]
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ val (a + b) = (val a + val b) % n
[PROOFSTEP]
cases n
[GOAL]
case zero
inst✝ : NeZero Nat.zero
a b : ZMod Nat.zero
⊢ val (a + b) = (val a + val b) % Nat.zero
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
⊢ val (a + b) = (val a + val b) % Nat.succ n✝
[PROOFSTEP]
apply Fin.val_add
[GOAL]
n : ℕ
a b : ZMod n
⊢ val (a * b) = val a * val b % n
[PROOFSTEP]
cases n
[GOAL]
case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b % Nat.zero
[PROOFSTEP]
rw [Nat.mod_zero]
[GOAL]
case zero
a b : ZMod Nat.zero
⊢ val (a * b) = val a * val b
[PROOFSTEP]
apply Int.natAbs_mul
[GOAL]
case succ
n✝ : ℕ
a b : ZMod (Nat.succ n✝)
⊢ val (a * b) = val a * val b % Nat.succ n✝
[PROOFSTEP]
apply Fin.val_mul
[GOAL]
n : ℕ
inst✝ : Fact (1 < n)
h : 0 = 1
⊢ 0 = val 0
[PROOFSTEP]
rw [val_zero]
[GOAL]
⊢ Nontrivial (ZMod 0)
[PROOFSTEP]
delta ZMod
[GOAL]
⊢ Nontrivial
    (match 0 with
    | 0 => ℤ
    | Nat.succ n => Fin (n + 1))
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ ↑(Nat.gcdA (val 0) (n + 1)) = 0
[PROOFSTEP]
rw [val_zero]
[GOAL]
n : ℕ
⊢ ↑(Nat.gcdA 0 (n + 1)) = 0
[PROOFSTEP]
unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
[GOAL]
n : ℕ
⊢ ↑(n + 1, 0, 1).snd.fst = 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) n)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
a : ZMod Nat.zero
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) Nat.zero)
[PROOFSTEP]
dsimp [ZMod] at a ⊢
[GOAL]
case zero
a : ℤ
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) 0)
[PROOFSTEP]
calc
  _ = a * Int.sign a := rfl
  _ = a.natAbs := by rw [Int.mul_sign]
  _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
[GOAL]
a : ℤ
⊢ a * Int.sign a = ↑(Int.natAbs a)
[PROOFSTEP]
rw [Int.mul_sign]
[GOAL]
a : ℤ
⊢ ↑(Int.natAbs a) = ↑(Nat.gcd (Int.natAbs a) 0)
[PROOFSTEP]
rw [Nat.gcd_zero_right]
[GOAL]
case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) (Nat.succ n))
[PROOFSTEP]
calc
  a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by rw [nat_cast_self, zero_mul, add_zero]
  _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) :=
    by
    push_cast
    rw [nat_cast_zmod_val]
    rfl
  _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ = a * a⁻¹ + ↑(Nat.succ n) * ↑(Nat.gcdB (val a) (Nat.succ n))
[PROOFSTEP]
rw [nat_cast_self, zero_mul, add_zero]
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + ↑(Nat.succ n) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    ↑(↑(val a) * Nat.gcdA (val a) (Nat.succ n) + ↑(Nat.succ n) * Nat.gcdB (val a) (Nat.succ n))
[PROOFSTEP]
push_cast
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    ↑(val a) * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
[PROOFSTEP]
rw [nat_cast_zmod_val]
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    a * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ ↑(↑(val a) * Nat.gcdA (val a) (Nat.succ n) + ↑(Nat.succ n) * Nat.gcdB (val a) (Nat.succ n)) =
    ↑(Nat.gcd (val a) (Nat.succ n))
[PROOFSTEP]
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
⊢ ↑↑(Nat.gcd (val a) (Nat.succ n)) = ↑(Nat.gcd (val a) (Nat.succ n))
[PROOFSTEP]
rfl
[GOAL]
a n : ℕ
⊢ ↑(a % n) = ↑a
[PROOFSTEP]
conv =>
  rhs
  rw [← Nat.mod_add_div a n]
[GOAL]
a n : ℕ
| ↑(a % n) = ↑a
[PROOFSTEP]
  rhs
  rw [← Nat.mod_add_div a n]
[GOAL]
a n : ℕ
| ↑(a % n) = ↑a
[PROOFSTEP]
  rhs
  rw [← Nat.mod_add_div a n]
[GOAL]
a n : ℕ
| ↑(a % n) = ↑a
[PROOFSTEP]
rhs
[GOAL]
a n : ℕ
| ↑a
[PROOFSTEP]
rw [← Nat.mod_add_div a n]
[GOAL]
a n : ℕ
⊢ ↑(a % n) = ↑(a % n + n * (a / n))
[PROOFSTEP]
simp
[GOAL]
n a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD n]
[PROOFSTEP]
cases n
[GOAL]
case zero
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.zero]
[PROOFSTEP]
simp [Nat.ModEq, Int.coe_nat_inj', Nat.mod_zero]
[GOAL]
case succ
a b n✝ : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.succ n✝]
[PROOFSTEP]
rw [Fin.ext_iff, Nat.ModEq, ← val_nat_cast, ← val_nat_cast]
[GOAL]
case succ
a b n✝ : ℕ
⊢ ↑↑a = ↑↑b ↔ val ↑a = val ↑b
[PROOFSTEP]
exact Iff.rfl
[GOAL]
n x : ℕ
h : Nat.coprime x n
⊢ ↑x * (↑x)⁻¹ = 1
[PROOFSTEP]
rw [Nat.coprime, Nat.gcd_comm, Nat.gcd_rec] at h
[GOAL]
n x : ℕ
h : Nat.gcd (x % n) n = 1
⊢ ↑x * (↑x)⁻¹ = 1
[PROOFSTEP]
rw [mul_inv_eq_gcd, val_nat_cast, h, Nat.cast_one]
[GOAL]
n x : ℕ
h : Nat.coprime x n
⊢ (↑x)⁻¹ * ↑x = 1
[PROOFSTEP]
rw [mul_comm, coe_mul_inv_eq_one x h]
[GOAL]
n : ℕ
u : (ZMod n)ˣ
⊢ Nat.coprime (val ↑u) n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
u : (ZMod Nat.zero)ˣ
⊢ Nat.coprime (val ↑u) Nat.zero
[PROOFSTEP]
rcases Int.units_eq_one_or u with (rfl | rfl)
[GOAL]
case zero.inl
⊢ Nat.coprime (val ↑1) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case zero.inr
⊢ Nat.coprime (val ↑(-1)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ Nat.coprime (val ↑u) (Nat.succ n)
[PROOFSTEP]
apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
[PROOFSTEP]
have := Units.ext_iff.1 (mul_right_inv u)
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
[PROOFSTEP]
rw [Units.val_one] at this
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
[PROOFSTEP]
rw [← eq_iff_modEq_nat, Nat.cast_one, ← this]
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
[PROOFSTEP]
clear this
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
[PROOFSTEP]
rw [← nat_cast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
[GOAL]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(val ↑(u * u⁻¹))
[PROOFSTEP]
rw [Units.val_mul, val_mul, nat_cast_mod]
[GOAL]
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹
[PROOFSTEP]
have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑(Nat.gcd (val ↑u) n) = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹
[PROOFSTEP]
rw [← mul_inv_eq_gcd, Nat.cast_one] at this
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹
[PROOFSTEP]
let u' : (ZMod n)ˣ := ⟨u, (u : ZMod n)⁻¹, this, by rwa [mul_comm]⟩
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ * ↑u = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := (_ : (↑u)⁻¹ * ↑u = 1) }
⊢ (↑u)⁻¹ = ↑u⁻¹
[PROOFSTEP]
have h : u = u' := by
  apply Units.ext
  rfl
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := (_ : (↑u)⁻¹ * ↑u = 1) }
⊢ u = u'
[PROOFSTEP]
apply Units.ext
[GOAL]
case a
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := (_ : (↑u)⁻¹ * ↑u = 1) }
⊢ ↑u = ↑u'
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := (_ : (↑u)⁻¹ * ↑u = 1) }
h : u = u'
⊢ (↑u)⁻¹ = ↑u⁻¹
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := (_ : (↑u)⁻¹ * ↑u = 1) }
h : u = u'
⊢ (↑u')⁻¹ = ↑u'⁻¹
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1
[PROOFSTEP]
rcases h with ⟨u, rfl⟩
[GOAL]
case intro
n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * (↑u)⁻¹ = 1
[PROOFSTEP]
rw [inv_coe_unit, u.mul_inv]
[GOAL]
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1
[PROOFSTEP]
rw [mul_comm, mul_inv_of_unit a h]
[GOAL]
n : ℕ
inst✝ : NeZero n
x✝ : { x // Nat.coprime (val x) n }
val✝ : ZMod n
property✝ : Nat.coprime (val val✝) n
⊢ (fun x => { val := ↑x, property := (_ : Nat.coprime (val ↑x) n) })
      ((fun x => unitOfCoprime (val ↑x) (_ : Nat.coprime (val ↑x) n)) { val := val✝, property := property✝ }) =
    { val := val✝, property := property✝ }
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
h : Nat.coprime m n
⊢ Nat.lcm m n ∣ m * n
[PROOFSTEP]
simp [Nat.lcm_dvd_iff]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : m * n = 0
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case inl.intro
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
constructor
[GOAL]
case inl.intro.left
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun
[PROOFSTEP]
intro x
[GOAL]
case inl.intro.left
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
x : ZMod (0 * 1)
⊢ inv_fun (to_fun x) = x
[PROOFSTEP]
rfl
[GOAL]
case inl.intro.right
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
⊢ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case inl.intro.right.mk
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
x : ZMod 0
y : ZMod 1
⊢ to_fun (inv_fun (x, y)) = (x, y)
[PROOFSTEP]
fin_cases y
[GOAL]
case inl.intro.right.mk.head
h : Nat.coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ↑(castHom (_ : Nat.lcm 0 1 ∣ 0 * 1) (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x =>
    if 0 * 1 = 0 then if 0 = 1 then ↑(↑(RingHom.snd (ZMod 0) (ZMod 1)) x) else ↑(↑(RingHom.fst (ZMod 0) (ZMod 1)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 0 * 1 = 0
x : ZMod 0
⊢ to_fun (inv_fun (x, { val := 0, isLt := (_ : 0 < 0 + 1) })) = (x, { val := 0, isLt := (_ : 0 < 0 + 1) })
[PROOFSTEP]
simp [castHom, Prod.ext_iff]
[GOAL]
case inr.intro
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
constructor
[GOAL]
case inr.intro.left
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun
[PROOFSTEP]
intro x
[GOAL]
case inr.intro.left
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
x : ZMod (1 * 0)
⊢ inv_fun (to_fun x) = x
[PROOFSTEP]
rfl
[GOAL]
case inr.intro.right
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
⊢ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case inr.intro.right.mk
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
x : ZMod 1
y : ZMod 0
⊢ to_fun (inv_fun (x, y)) = (x, y)
[PROOFSTEP]
fin_cases x
[GOAL]
case inr.intro.right.mk.head
h : Nat.coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ↑(castHom (_ : Nat.lcm 1 0 ∣ 1 * 0) (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x =>
    if 1 * 0 = 0 then if 1 = 1 then ↑(↑(RingHom.snd (ZMod 1) (ZMod 0)) x) else ↑(↑(RingHom.fst (ZMod 1) (ZMod 0)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : 1 * 0 = 0
y : ZMod 0
⊢ to_fun (inv_fun ({ val := 0, isLt := (_ : 0 < 0 + 1) }, y)) = ({ val := 0, isLt := (_ : 0 < 0 + 1) }, y)
[PROOFSTEP]
simp [castHom, Prod.ext_iff]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
haveI : NeZero (m * n) := ⟨hmn0⟩
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
have left_inv : Function.LeftInverse inv_fun to_fun := by
  intro x
  dsimp only [dvd_mul_left, dvd_mul_right, ZMod.castHom_apply]
  conv_rhs => rw [← ZMod.nat_cast_zmod_val x]
  rw [if_neg hmn0, ZMod.eq_iff_modEq_nat, ← Nat.modEq_and_modEq_iff_modEq_mul h, Prod.fst_zmod_cast, Prod.snd_zmod_cast]
  refine'
    ⟨(Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.left.trans _,
      (Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.right.trans _⟩
  · rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
  · rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ LeftInverse inv_fun to_fun
[PROOFSTEP]
intro x
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ inv_fun (to_fun x) = x
[PROOFSTEP]
dsimp only [dvd_mul_left, dvd_mul_right, ZMod.castHom_apply]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) ↑x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) ↑x)
    else ↑↑(Nat.chineseRemainder h (val (↑x).fst) (val (↑x).snd))) =
    x
[PROOFSTEP]
conv_rhs => rw [← ZMod.nat_cast_zmod_val x]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
| x
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val x]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
| x
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val x]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
| x
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val x]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) ↑x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) ↑x)
    else ↑↑(Nat.chineseRemainder h (val (↑x).fst) (val (↑x).snd))) =
    ↑(val x)
[PROOFSTEP]
rw [if_neg hmn0, ZMod.eq_iff_modEq_nat, ← Nat.modEq_and_modEq_iff_modEq_mul h, Prod.fst_zmod_cast, Prod.snd_zmod_cast]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h (val ↑x) (val ↑x)) ≡ val x [MOD m] ∧
    ↑(Nat.chineseRemainder h (val ↑x) (val ↑x)) ≡ val x [MOD n]
[PROOFSTEP]
refine'
  ⟨(Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.left.trans _,
    (Nat.chineseRemainder h (x : ZMod m).val (x : ZMod n).val).2.right.trans _⟩
[GOAL]
case refine'_1
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ val ↑x ≡ val x [MOD m]
[PROOFSTEP]
rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
[GOAL]
case refine'_2
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ val ↑x ≡ val x [MOD n]
[PROOFSTEP]
rw [← ZMod.eq_iff_modEq_nat, ZMod.nat_cast_zmod_val, ZMod.nat_cast_val]
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
left_inv : LeftInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun
[PROOFSTEP]
exact ⟨left_inv, left_inv.rightInverse_of_card_le (by simp)⟩
[GOAL]
m n : ℕ
h : Nat.coprime m n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ↑(castHom (_ : Nat.lcm m n ∣ m * n) (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x =>
    if m * n = 0 then if m = 1 then ↑(↑(RingHom.snd (ZMod m) (ZMod n)) x) else ↑(↑(RingHom.fst (ZMod m) (ZMod n)) x)
    else ↑↑(Nat.chineseRemainder h (val x.fst) (val x.snd))
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
left_inv : LeftInverse inv_fun to_fun
⊢ Fintype.card (ZMod m × ZMod n) ≤ Fintype.card (ZMod (m * n))
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (a b : (ZMod 2)ˣ), a = b
[PROOFSTEP]
decide
[GOAL]
n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
[PROOFSTEP]
rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn
[GOAL]
n : ℕ
hn : Nat.coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
[PROOFSTEP]
rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]
[GOAL]
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ a ≠ -a
[PROOFSTEP]
rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]
[GOAL]
a : ZMod 2
⊢ -a = a
[PROOFSTEP]
fin_cases a
[GOAL]
case head
⊢ -{ val := 0, isLt := (_ : 0 < 1 + 1) } = { val := 0, isLt := (_ : 0 < 1 + 1) }
[PROOFSTEP]
apply Fin.ext
[GOAL]
case tail.head
⊢ -{ val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } = { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) }
[PROOFSTEP]
apply Fin.ext
[GOAL]
case head.h
⊢ ↑(-{ val := 0, isLt := (_ : 0 < 1 + 1) }) = ↑{ val := 0, isLt := (_ : 0 < 1 + 1) }
[PROOFSTEP]
simp [Fin.coe_neg, Int.natMod]
[GOAL]
case tail.head.h
⊢ ↑(-{ val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) }) = ↑{ val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) }
[PROOFSTEP]
simp [Fin.coe_neg, Int.natMod]
[GOAL]
a : ℤ
⊢ ↑(Int.natAbs a) = ↑a
[PROOFSTEP]
cases a
[GOAL]
case ofNat
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp only [Int.natAbs_ofNat, Int.cast_ofNat, Int.ofNat_eq_coe]
[GOAL]
case negSucc
a✝ : ℕ
⊢ ↑(Int.natAbs (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp only [neg_eq_self_mod_two, Nat.cast_succ, Int.natAbs, Int.cast_negSucc]
[GOAL]
n : ℕ
a : ZMod (n + 1)
⊢ val a = 0 ↔ a = 0
[PROOFSTEP]
rw [Fin.ext_iff]
[GOAL]
n : ℕ
a : ZMod (n + 1)
⊢ val a = 0 ↔ ↑a = ↑0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * val a = n
[PROOFSTEP]
rw [neg_eq_iff_add_eq_zero, ← two_mul]
[GOAL]
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = n
[PROOFSTEP]
cases n
[GOAL]
case zero
a : ZMod Nat.zero
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.zero
[PROOFSTEP]
erw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero]
[GOAL]
case zero
a : ZMod Nat.zero
⊢ 2 = 0 ∨ a = 0 ↔ a = 0 ∨ 2 = 0 ∨ a = 0
[PROOFSTEP]
exact ⟨fun h => h.elim (by simp) Or.inl, fun h => Or.inr (h.elim id fun h => h.elim (by simp) id)⟩
[GOAL]
a : ZMod Nat.zero
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0 ∨ 2 = 0 ∨ a = 0
[PROOFSTEP]
simp
[GOAL]
a : ZMod Nat.zero
h✝ : a = 0 ∨ 2 = 0 ∨ a = 0
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
conv_lhs => rw [← a.nat_cast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, nat_cast_zmod_eq_zero_iff_dvd]
[GOAL]
n✝ : ℕ
a : ZMod (Nat.succ n✝)
| 2 * a = 0
[PROOFSTEP]
rw [← a.nat_cast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, nat_cast_zmod_eq_zero_iff_dvd]
[GOAL]
n✝ : ℕ
a : ZMod (Nat.succ n✝)
| 2 * a = 0
[PROOFSTEP]
rw [← a.nat_cast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, nat_cast_zmod_eq_zero_iff_dvd]
[GOAL]
n✝ : ℕ
a : ZMod (Nat.succ n✝)
| 2 * a = 0
[PROOFSTEP]
rw [← a.nat_cast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, nat_cast_zmod_eq_zero_iff_dvd]
[GOAL]
case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a → a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
rintro ⟨m, he⟩
[GOAL]
case succ.mp.intro
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
cases' m with m
[GOAL]
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
erw [mul_zero, mul_eq_zero] at he
[GOAL]
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 = 0 ∨ val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
rcases he with (⟨⟨⟩⟩ | he)
[GOAL]
case succ.mp.intro.zero.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
exact Or.inl (a.val_eq_zero.1 he)
[GOAL]
case succ.mp.intro.succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * Nat.succ m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
cases m
[GOAL]
case succ.mp.intro.succ.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
[PROOFSTEP]
right
[GOAL]
case succ.mp.intro.succ.zero.h
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ 2 * val a = Nat.succ n✝
[PROOFSTEP]
rwa [show Nat.succ Nat.zero = 1 from rfl, mul_one] at he
[GOAL]
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝¹
[PROOFSTEP]
refine' (a.val_lt.not_le <| Nat.le_of_mul_le_mul_left _ zero_lt_two).elim
[GOAL]
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 * Nat.succ n✝¹ ≤ 2 * val a
[PROOFSTEP]
rw [he, mul_comm]
[GOAL]
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ Nat.succ n✝¹ * 2 ≤ Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)
[PROOFSTEP]
erw [Nat.succ_le_succ_iff, Nat.succ_le_succ_iff]
[GOAL]
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 0 ≤ n✝
[PROOFSTEP]
simp
[GOAL]
case succ.mpr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝ → Nat.succ n✝ ∣ 2 * val a
[PROOFSTEP]
rintro (rfl | h)
[GOAL]
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 2 * val 0
[PROOFSTEP]
rw [val_zero, mul_zero]
[GOAL]
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 0
[PROOFSTEP]
apply dvd_zero
[GOAL]
case succ.mpr.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
h : 2 * val a = Nat.succ n✝
⊢ Nat.succ n✝ ∣ 2 * val a
[PROOFSTEP]
rw [h]
[GOAL]
n a : ℕ
h : a < n
⊢ val ↑a = a
[PROOFSTEP]
rw [val_nat_cast, Nat.mod_eq_of_lt h]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) = val (-a) % n
[PROOFSTEP]
rw [Nat.mod_eq_of_lt (-a).val_lt]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) + ?m.561595 a ≡ n - val a + ?m.561595 a [MOD n]
[PROOFSTEP]
rw [Nat.ModEq, ← val_add, add_left_neg, tsub_add_cancel_of_le a.val_le, Nat.mod_self, val_zero]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) = if a = 0 then 0 else n - val a
[PROOFSTEP]
rw [neg_val']
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
[PROOFSTEP]
rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = if a = 0 then 0 else n - val a
[PROOFSTEP]
rw [if_neg h]
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - val a) % n = n - val a
[PROOFSTEP]
apply Nat.mod_eq_of_lt
[GOAL]
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - val a < n
[PROOFSTEP]
apply Nat.sub_lt (NeZero.pos n)
[GOAL]
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ 0 < val a
[PROOFSTEP]
contrapose! h
[GOAL]
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val a ≤ 0
⊢ a = 0
[PROOFSTEP]
rwa [le_zero_iff, val_eq_zero] at h
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ valMinAbs x = if val x ≤ n / 2 then ↑(val x) else ↑(val x) - ↑n
[PROOFSTEP]
cases n
[GOAL]
case zero
inst✝ : NeZero Nat.zero
x : ZMod Nat.zero
⊢ valMinAbs x = if val x ≤ Nat.zero / 2 then ↑(val x) else ↑(val x) - ↑Nat.zero
[PROOFSTEP]
cases NeZero.ne 0 rfl
[GOAL]
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
x : ZMod (Nat.succ n✝)
⊢ valMinAbs x = if val x ≤ Nat.succ n✝ / 2 then ↑(val x) else ↑(val x) - ↑(Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(valMinAbs x) = x
[PROOFSTEP]
rw [valMinAbs_def_pos]
[GOAL]
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if val x ≤ namedPattern k (n + 1) h✝ / 2 then ↑(val x) else ↑(val x) - ↑(namedPattern k (n + 1) h✝)) = x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑(val x) = x
[PROOFSTEP]
rw [Int.cast_ofNat, nat_cast_zmod_val]
[GOAL]
case neg
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑(val x) - ↑(namedPattern k (n + 1) h✝¹)) = x
[PROOFSTEP]
rw [Int.cast_sub, Int.cast_ofNat, nat_cast_zmod_val, Int.cast_ofNat, nat_cast_self, sub_zero]
[GOAL]
n m : ℕ
⊢ m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul, Nat.cast_two]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ 0 ≤ valMinAbs x ↔ val x ≤ n / 2
[PROOFSTEP]
rw [valMinAbs_def_pos]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if val x ≤ n / 2 then ↑(val x) else ↑(val x) - ↑n) ↔ val x ≤ n / 2
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : val x ≤ n / 2
⊢ 0 ≤ ↑(val x) ↔ val x ≤ n / 2
[PROOFSTEP]
exact iff_of_true (Nat.cast_nonneg _) h
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬val x ≤ n / 2
⊢ 0 ≤ ↑(val x) - ↑n ↔ val x ≤ n / 2
[PROOFSTEP]
exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_le h
[GOAL]
n : ℕ
a : ZMod n
⊢ valMinAbs a * 2 = ↑n ↔ 2 * val a = n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
a : ZMod Nat.zero
⊢ valMinAbs a * 2 = ↑Nat.zero ↔ 2 * val a = Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
[PROOFSTEP]
by_cases h : a.val ≤ n.succ / 2
[GOAL]
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
[PROOFSTEP]
dsimp [valMinAbs]
[GOAL]
case pos
n : ℕ
a : ZMod (Nat.succ n)
h : val a ≤ Nat.succ n / 2
⊢ (if val a ≤ Nat.succ n / 2 then ↑(val a) else ↑(val a) - ↑(Nat.succ n)) * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
[PROOFSTEP]
rw [if_pos h, ← Int.coe_nat_inj', Nat.cast_mul, Nat.cast_two, mul_comm]
[GOAL]
case neg
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ valMinAbs a * 2 = ↑(Nat.succ n) ↔ 2 * val a = Nat.succ n
[PROOFSTEP]
apply iff_of_false _ (mt _ h)
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ ¬valMinAbs a * 2 = ↑(Nat.succ n)
[PROOFSTEP]
intro he
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False
[PROOFSTEP]
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
h✝ : ¬0 ≤ valMinAbs a
h : ¬0 ≤ ↑(Nat.succ n)
he : valMinAbs a * 2 = ↑(Nat.succ n)
⊢ False
n : ℕ a : ZMod (Nat.succ n) h : ¬0 ≤ valMinAbs a he : valMinAbs a * 2 = ↑(Nat.succ n) ⊢ 0 < 2
[PROOFSTEP]
exacts [h (Nat.cast_nonneg _), zero_lt_two]
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ 2 * val a = Nat.succ n → val a ≤ Nat.succ n / 2
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n : ℕ
a : ZMod (Nat.succ n)
h : ¬val a ≤ Nat.succ n / 2
⊢ val a * 2 = Nat.succ n → val a ≤ Nat.succ n / 2
[PROOFSTEP]
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑(val x) * 2 ≤ ↑n then ↑(val x) else ↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
refine' ⟨(neg_lt_zero.2 <| by exact_mod_cast NeZero.pos n).trans_le (mul_nonneg _ _), h⟩
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 < ↑n
[PROOFSTEP]
exact_mod_cast NeZero.pos n
[GOAL]
case pos.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 ≤ ↑(val x)
case pos.refine'_2 n : ℕ inst✝ : NeZero n x : ZMod n h : ↑(val x) * 2 ≤ ↑n ⊢ 0 ≤ 2
[PROOFSTEP]
exacts [Nat.cast_nonneg _, zero_le_two]
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ (↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
refine' ⟨_, le_trans (mul_nonpos_of_nonpos_of_nonneg _ zero_le_two) <| Nat.cast_nonneg _⟩
[GOAL]
case neg.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ -↑n < (↑(val x) - ↑n) * 2
[PROOFSTEP]
linarith only [h]
[GOAL]
case neg.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) - ↑n ≤ 0
[PROOFSTEP]
rw [sub_nonpos, Int.ofNat_le]
[GOAL]
case neg.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ val x ≤ n
[PROOFSTEP]
exact x.val_lt.le
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
⊢ valMinAbs x = y → x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ x = ↑(valMinAbs x) ∧ valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n
[PROOFSTEP]
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x = y
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x - y = 0
[PROOFSTEP]
apply @Int.eq_zero_of_abs_lt_dvd n
[GOAL]
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ valMinAbs x - y
[PROOFSTEP]
rw [← int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
[GOAL]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |valMinAbs x - y| < ↑n
[PROOFSTEP]
rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)]
[GOAL]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |valMinAbs x - y| * 2 < ↑n * 2
[PROOFSTEP]
nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
[GOAL]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |valMinAbs x - y| * |2| < ↑n * 2
[PROOFSTEP]
rw [← abs_mul, sub_mul, abs_lt]
[GOAL]
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < valMinAbs x * 2 - y * 2 ∧ valMinAbs x * 2 - y * 2 < ↑n * 2
[PROOFSTEP]
constructor
[GOAL]
case h2.left
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < valMinAbs x * 2 - y * 2
[PROOFSTEP]
linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
[GOAL]
case h2.right
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ valMinAbs x * 2 - y * 2 < ↑n * 2
[PROOFSTEP]
linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ Int.natAbs (valMinAbs x) ≤ n / 2
[PROOFSTEP]
rw [Nat.le_div_two_iff_mul_two_le]
[GOAL]
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
[PROOFSTEP]
cases' x.valMinAbs.natAbs_eq with h h
[GOAL]
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
[PROOFSTEP]
rw [← h]
[GOAL]
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ valMinAbs x * 2 ≤ ↑n
[PROOFSTEP]
exact x.valMinAbs_mem_Ioc.2
[GOAL]
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
[PROOFSTEP]
rw [← neg_le_neg_iff, ← neg_mul, ← h]
[GOAL]
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ -↑n ≤ valMinAbs x * 2
[PROOFSTEP]
exact x.valMinAbs_mem_Ioc.1.le
[GOAL]
⊢ valMinAbs 0 = 0
[PROOFSTEP]
simp only [valMinAbs_def_zero]
[GOAL]
n : ℕ
⊢ valMinAbs 0 = 0
[PROOFSTEP]
simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]
[GOAL]
n : ℕ
x : ZMod n
⊢ valMinAbs x = 0 ↔ x = 0
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
x : ZMod Nat.zero
⊢ valMinAbs x = 0 ↔ x = 0
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = 0 ↔ x = 0
[PROOFSTEP]
rw [← valMinAbs_zero n.succ]
[GOAL]
case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = valMinAbs 0 ↔ x = 0
[PROOFSTEP]
apply injective_valMinAbs.eq_iff
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(Int.natAbs (valMinAbs a)) = if val a ≤ n / 2 then a else -a
[PROOFSTEP]
have : (a.val : ℤ) - n ≤ 0 := by
  erw [sub_nonpos, Int.ofNat_le]
  exact a.val_le
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) - ↑n ≤ 0
[PROOFSTEP]
erw [sub_nonpos, Int.ofNat_le]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val a ≤ n
[PROOFSTEP]
exact a.val_le
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (valMinAbs a)) = if val a ≤ n / 2 then a else -a
[PROOFSTEP]
rw [valMinAbs_def_pos]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n)) = if val a ≤ n / 2 then a else -a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : val a ≤ n / 2
⊢ ↑(Int.natAbs ↑(val a)) = a
[PROOFSTEP]
rw [Int.natAbs_ofNat, nat_cast_zmod_val]
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : ¬val a ≤ n / 2
⊢ ↑(Int.natAbs (↑(val a) - ↑n)) = -a
[PROOFSTEP]
rw [← Int.cast_ofNat, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub, Int.cast_ofNat, Int.cast_ofNat,
  nat_cast_self, sub_zero, nat_cast_zmod_val]
[GOAL]
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
⊢ valMinAbs (-a) = -valMinAbs a
[PROOFSTEP]
cases' eq_zero_or_neZero n with h h
[GOAL]
case inl
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : n = 0
⊢ valMinAbs (-a) = -valMinAbs a
[PROOFSTEP]
subst h
[GOAL]
case inl
a : ZMod 0
ha : 2 * val a ≠ 0
⊢ valMinAbs (-a) = -valMinAbs a
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs (-a) = -valMinAbs a
[PROOFSTEP]
refine' (valMinAbs_spec _ _).2 ⟨_, _, _⟩
[GOAL]
case inr.refine'_1
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -a = ↑(-valMinAbs a)
[PROOFSTEP]
rw [Int.cast_neg, coe_valMinAbs]
[GOAL]
case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -↑n < -valMinAbs a * 2
[PROOFSTEP]
rw [neg_mul, neg_lt_neg_iff]
[GOAL]
case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs a * 2 < ↑n
[PROOFSTEP]
exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
[GOAL]
case inr.refine'_3
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -valMinAbs a * 2 ≤ ↑n
[PROOFSTEP]
linarith only [a.valMinAbs_mem_Ioc.1]
[GOAL]
n : ℕ
a : ZMod n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
[PROOFSTEP]
by_cases h2a : 2 * a.val = n
[GOAL]
case pos
n : ℕ
a : ZMod n
h2a : 2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
[PROOFSTEP]
rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
[GOAL]
case neg
n : ℕ
a : ZMod n
h2a : ¬2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
[PROOFSTEP]
rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = valMinAbs a + ↑(if val a ≤ n / 2 then 0 else n)
[PROOFSTEP]
rw [valMinAbs_def_pos]
[GOAL]
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) + ↑(if val a ≤ n / 2 then 0 else n)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : val a ≤ n / 2
⊢ ↑(val a) = ↑(val a) + ↑0
[PROOFSTEP]
simp [add_zero, sub_add_cancel]
[GOAL]
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : ¬val a ≤ n / 2
⊢ ↑(val a) = ↑(val a) - ↑n + ↑n
[PROOFSTEP]
simp [add_zero, sub_add_cancel]
[GOAL]
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ ↑q ≠ 0
[PROOFSTEP]
rwa [← Nat.cast_zero, Ne.def, eq_iff_modEq_nat, Nat.modEq_zero_iff_dvd, ← hp.1.coprime_iff_not_dvd,
  Nat.coprime_primes hp.1 hq.1]
[GOAL]
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
⊢ Int.natAbs (valMinAbs a) = min (val a) (n - val a)
[PROOFSTEP]
rw [valMinAbs_def_pos]
[GOAL]
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
⊢ Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) = min (val a) (n - val a)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ Int.natAbs ↑(val a) = min (val a) (n - val a)
[PROOFSTEP]
rw [Int.natAbs_ofNat]
[GOAL]
case pos
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ val a = min (val a) (n - val a)
[PROOFSTEP]
symm
[GOAL]
case pos
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ min (val a) (n - val a) = val a
[PROOFSTEP]
apply min_eq_left (le_trans h (le_trans (Nat.half_le_of_sub_le_half _) (Nat.sub_le_sub_left n h)))
[GOAL]
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : val a ≤ n / 2
⊢ n - (n - n / 2) ≤ n / 2
[PROOFSTEP]
rw [Nat.sub_sub_self (Nat.div_le_self _ _)]
[GOAL]
case neg
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs (↑(val a) - ↑n) = min (val a) (n - val a)
[PROOFSTEP]
rw [← Int.natAbs_neg, neg_sub, ← Nat.cast_sub a.val_le]
[GOAL]
case neg
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ Int.natAbs ↑(n - val a) = min (val a) (n - val a)
[PROOFSTEP]
symm
[GOAL]
case neg
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ min (val a) (n - val a) = Int.natAbs ↑(n - val a)
[PROOFSTEP]
apply
  min_eq_right
    (le_trans (le_trans (Nat.sub_le_sub_left n (lt_of_not_ge h)) (Nat.le_half_of_half_lt_sub _)) (le_of_not_ge h))
[GOAL]
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < n - (n - Nat.succ (n / 2))
[PROOFSTEP]
rw [Nat.sub_sub_self (Nat.div_lt_self (lt_of_le_of_ne' (Nat.zero_le _) hpos.1) one_lt_two)]
[GOAL]
n✝ a✝ n : ℕ
hpos : NeZero n
a : ZMod n
h : ¬val a ≤ n / 2
⊢ n / 2 < Nat.succ (n / 2)
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
n a : ℕ
ha : a ≤ n / 2
⊢ valMinAbs ↑a = ↑a
[PROOFSTEP]
cases n
[GOAL]
case zero
a : ℕ
ha : a ≤ Nat.zero / 2
⊢ valMinAbs ↑a = ↑a
[PROOFSTEP]
simp
[GOAL]
case succ
a n✝ : ℕ
ha : a ≤ Nat.succ n✝ / 2
⊢ valMinAbs ↑a = ↑a
[PROOFSTEP]
simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0), ha]
[GOAL]
n a : ℕ
ha : n / 2 < a
ha' : a < n
⊢ valMinAbs ↑a = ↑a - ↑n
[PROOFSTEP]
cases n
[GOAL]
case zero
a : ℕ
ha : Nat.zero / 2 < a
ha' : a < Nat.zero
⊢ valMinAbs ↑a = ↑a - ↑Nat.zero
[PROOFSTEP]
cases not_lt_bot ha'
[GOAL]
case succ
a n✝ : ℕ
ha : Nat.succ n✝ / 2 < a
ha' : a < Nat.succ n✝
⊢ valMinAbs ↑a = ↑a - ↑(Nat.succ n✝)
[PROOFSTEP]
simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
[GOAL]
n a : ℕ
inst✝ : NeZero n
⊢ valMinAbs ↑a = ↑a ↔ a ≤ n / 2
[PROOFSTEP]
refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
[GOAL]
n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ a ≤ n / 2
[PROOFSTEP]
rw [← Int.natAbs_ofNat a, ← ha]
[GOAL]
n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ Int.natAbs (valMinAbs ↑a) ≤ n / 2
[PROOFSTEP]
exact natAbs_valMinAbs_le a
[GOAL]
n✝ a n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs y
[PROOFSTEP]
rw [int_cast_eq_int_cast_iff_dvd_sub] at he
[GOAL]
n✝ a n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs y
[PROOFSTEP]
obtain ⟨m, he⟩ := he
[GOAL]
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ Int.natAbs x ≤ Int.natAbs y
[PROOFSTEP]
rw [sub_eq_iff_eq_add] at he
[GOAL]
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ Int.natAbs x ≤ Int.natAbs y
[PROOFSTEP]
subst he
[GOAL]
case intro
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
[PROOFSTEP]
obtain rfl | hm := eq_or_ne m 0
[GOAL]
case intro.inl
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs (↑n * 0 + x)
[PROOFSTEP]
rw [mul_zero, zero_add]
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
[PROOFSTEP]
apply hl.trans
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ Int.natAbs (↑n * m + x)
[PROOFSTEP]
rw [← add_le_add_iff_right x.natAbs]
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + Int.natAbs x ≤ Int.natAbs (↑n * m + x) + Int.natAbs x
[PROOFSTEP]
refine' le_trans (le_trans ((add_le_add_iff_left _).2 hl) _) (Int.natAbs_sub_le _ _)
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ Int.natAbs (↑n * m + x - x)
[PROOFSTEP]
rw [add_sub_cancel, Int.natAbs_mul, Int.natAbs_ofNat]
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * Int.natAbs m
[PROOFSTEP]
refine' le_trans _ (Nat.le_mul_of_pos_right <| Int.natAbs_pos.2 hm)
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n
[PROOFSTEP]
rw [← mul_two]
[GOAL]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n
[PROOFSTEP]
apply Nat.div_mul_le_self
[GOAL]
n✝ a✝ n : ℕ
a b : ZMod n
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
n a✝ : ℕ
a b : ZMod Nat.zero
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
[PROOFSTEP]
apply natAbs_min_of_le_div_two n.succ
[GOAL]
case succ.he
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ ↑(valMinAbs (a + b)) = ↑(valMinAbs a + valMinAbs b)
[PROOFSTEP]
simp_rw [Int.cast_add, coe_valMinAbs]
[GOAL]
case succ.hl
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Nat.succ n / 2
[PROOFSTEP]
apply natAbs_valMinAbs_le
[GOAL]
n a✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
obtain ⟨k, rfl⟩ := nat_cast_zmod_surjective a
[GOAL]
case intro
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1
[PROOFSTEP]
apply coe_mul_inv_eq_one
[GOAL]
case intro.h
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime k p
[PROOFSTEP]
apply Nat.coprime.symm
[GOAL]
case intro.h.a
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime p k
[PROOFSTEP]
rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
[GOAL]
n a p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsDomain (ZMod p)
[PROOFSTEP]
cases p
[GOAL]
case zero
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : Fact (Nat.Prime Nat.zero)
⊢ IsDomain (ZMod Nat.zero)
[PROOFSTEP]
exact (Nat.not_prime_zero hp.out).elim
[GOAL]
case succ
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝ : ℕ
hp : Fact (Nat.Prime (Nat.succ n✝))
⊢ IsDomain (ZMod (Nat.succ n✝))
[PROOFSTEP]
exact @Field.isDomain (ZMod _) (inferInstanceAs (Field (ZMod _)))
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
a : ZMod n
⊢ ↑f a = ↑g a
[PROOFSTEP]
obtain ⟨k, rfl⟩ := ZMod.int_cast_surjective a
[GOAL]
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
⊢ ↑f ↑k = ↑g ↑k
[PROOFSTEP]
let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
[GOAL]
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
[PROOFSTEP]
let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
[GOAL]
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
[PROOFSTEP]
show φ k = ψ k
[GOAL]
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑φ k = ↑ψ k
[PROOFSTEP]
rw [φ.ext_int ψ]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g
[PROOFSTEP]
rw [RingEquiv.coe_ringHom_inj_iff]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ ↑f = ↑g
[PROOFSTEP]
apply RingHom.ext_zmod _ _
[GOAL]
n : ℕ
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod n
k : ZMod n
⊢ ↑f ↑k = k
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod Nat.zero
k : ZMod Nat.zero
⊢ ↑f ↑k = k
[PROOFSTEP]
dsimp [ZMod, ZMod.cast] at f k ⊢
[GOAL]
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ℤ
k : ℤ
⊢ ↑f ↑k = k
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
[PROOFSTEP]
dsimp [ZMod, ZMod.cast] at f k ⊢
[GOAL]
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* Fin (n✝ + 1)
k : Fin (n✝ + 1)
⊢ ↑f ↑(val k) = k
[PROOFSTEP]
erw [map_natCast, Fin.cast_val_eq_self]
[GOAL]
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
⊢ f = g
[PROOFSTEP]
have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
[GOAL]
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    ↑{ val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) }
⊢ f = g
[PROOFSTEP]
rw [Subtype.coe_mk] at this
[GOAL]
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this :
  RingHom.comp
      (↑(RingHom.liftOfRightInverse f cast (_ : Function.RightInverse cast ↑f))
        { val := g, property := (_ : RingHom.ker f ≤ RingHom.ker g) })
      f =
    g
⊢ f = g
[PROOFSTEP]
rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
[GOAL]
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
⊢ ∀ (x : ℤ →+ A), ↑x ↑n = 0 ↔ AddMonoidHom.ker (Int.castAddHom (ZMod n)) ≤ AddMonoidHom.ker x
[PROOFSTEP]
intro f
[GOAL]
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ ↑f ↑n = 0 ↔ AddMonoidHom.ker (Int.castAddHom (ZMod n)) ≤ AddMonoidHom.ker f
[PROOFSTEP]
rw [ker_int_castAddHom]
[GOAL]
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ ↑f ↑n = 0 ↔ AddSubgroup.zmultiples ↑n ≤ AddMonoidHom.ker f
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ ↑f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ AddMonoidHom.ker f
[PROOFSTEP]
rintro hf _ ⟨x, rfl⟩
[GOAL]
case mp.intro
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
hf : ↑f ↑n = 0
x : ℤ
⊢ (fun x => x • ↑n) x ∈ AddMonoidHom.ker f
[PROOFSTEP]
simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]
[GOAL]
case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ AddMonoidHom.ker f → ↑f ↑n = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
h : AddSubgroup.zmultiples ↑n ≤ AddMonoidHom.ker f
⊢ ↑f ↑n = 0
[PROOFSTEP]
refine' h (AddSubgroup.mem_zmultiples _)


[GOAL]
α : Type u
n : ℕ
⊢ map Fin.val (finRange n) = range n
[PROOFSTEP]
simp_rw [finRange, map_pmap, pmap_eq_map]
[GOAL]
α : Type u
n : ℕ
⊢ map (fun a => a) (range n) = range n
[PROOFSTEP]
exact List.map_id _
[GOAL]
α : Type u
n : ℕ
⊢ finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
[PROOFSTEP]
apply map_injective_iff.mpr Fin.val_injective
[GOAL]
case a
α : Type u
n : ℕ
⊢ map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
[PROOFSTEP]
rw [map_cons, map_coe_finRange, range_succ_eq_map, Fin.val_zero, ← map_coe_finRange, map_map, map_map]
[GOAL]
case a
α : Type u
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
[PROOFSTEP]
simp only [Function.comp, Fin.val_succ]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
[PROOFSTEP]
rw [pmap_eq_map_attach]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
[PROOFSTEP]
exact ext_get (by simp) fun i hi1 hi2 => by simp [get_ofFn f ⟨i, hi1⟩]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ length (ofFn f) = length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi1 : i < length (ofFn f)
hi2 : i < length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))
⊢ get (ofFn f) { val := i, isLt := hi1 } =
    get (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))) { val := i, isLt := hi2 }
[PROOFSTEP]
simp [get_ofFn f ⟨i, hi1⟩]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)
[PROOFSTEP]
rw [← ofFn_id, map_ofFn, Function.right_id]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (ofFn f)
[PROOFSTEP]
rw [ofFn_eq_pmap]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n))
[PROOFSTEP]
exact (nodup_range n).pmap fun _ _ _ _ H => Fin.veq_of_eq <| hf H
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) ↔ Function.Injective f
[PROOFSTEP]
refine' ⟨_, nodup_ofFn_ofInjective⟩
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) → Function.Injective f
[PROOFSTEP]
refine' Fin.consInduction _ (fun x₀ xs ih => _) f
[GOAL]
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
[PROOFSTEP]
intro _
[GOAL]
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
a✝ : Nodup (ofFn Fin.elim0)
⊢ Function.Injective Fin.elim0
[PROOFSTEP]
exact Function.injective_of_subsingleton _
[GOAL]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
⊢ Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ Function.Injective (Fin.cons x₀ xs)
[PROOFSTEP]
rw [Fin.cons_injective_iff]
[GOAL]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
[PROOFSTEP]
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
[GOAL]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : (¬x₀ ∈ Set.range fun i => xs i) ∧ Nodup (ofFn fun i => xs i)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
[PROOFSTEP]
exact h.imp_right ih
[GOAL]
n : ℕ
σ : Perm (Fin n)
⊢ map (↑σ) (finRange n) ~ finRange n
[PROOFSTEP]
rw [perm_ext ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
[GOAL]
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
[PROOFSTEP]
simpa [mem_map, mem_finRange, true_and_iff, iff_true_iff] using σ.surjective
[GOAL]
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ↑σ) ~ ofFn f
[PROOFSTEP]
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
[GOAL]
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (↑σ) (finRange n)) ~ map f (finRange n)
[PROOFSTEP]
exact σ.map_finRange_perm.map f


[GOAL]
α : Type u
n m i : ℕ
H : i < length (range' n m)
⊢ nthLe (range' n m) i H = n + i
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range n)
[PROOFSTEP]
simp only [range_eq_range', pairwise_lt_range']
[GOAL]
α : Type u
n : ℕ
⊢ Nodup (range n)
[PROOFSTEP]
simp only [range_eq_range', nodup_range']
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range (succ n)) ↔ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
rw [range_succ]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u
r : ℕ → ℕ → Prop
⊢ Chain' r (range zero ++ [zero]) ↔ ∀ (m : ℕ), m < zero → r m (succ m)
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range (succ n) ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
rw [range_succ]
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n] ++ [succ n]) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
simp only [append_assoc, singleton_append, chain'_append_cons_cons, chain'_singleton, and_true_iff]
[GOAL]
case succ
α : Type u
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (succ m)
⊢ Chain' r (range n ++ [n]) ∧ r n (succ n) ↔ ∀ (m : ℕ), m < succ n → r m (succ m)
[PROOFSTEP]
rw [hn, forall_lt_succ]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ Chain r a (range (succ n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m (succ m)
[PROOFSTEP]
rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]
[GOAL]
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' (fun m => r m) (0 :: map succ (range n)))
[PROOFSTEP]
exact fun _ => Iff.rfl
[GOAL]
α : Type u
n : ℕ
⊢ Pairwise (fun x x_1 => x > x_1) (iota n)
[PROOFSTEP]
simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range' 1 n
[GOAL]
α : Type u
n : ℕ
a : Fin n
⊢ { val := ↑a, isLt := (_ : ↑a < n) } = a
[PROOFSTEP]
cases a
[GOAL]
case mk
α : Type u
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < n) } =
    { val := val✝, isLt := isLt✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
n : ℕ
⊢ length (finRange n) = n
[PROOFSTEP]
rw [finRange, length_pmap, length_range]
[GOAL]
α : Type u
n : ℕ
⊢ finRange n = [] ↔ n = 0
[PROOFSTEP]
rw [← length_eq_zero, length_finRange]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ prod (map f (range (succ n))) = prod (map f (range n)) * f n
[PROOFSTEP]
rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ 1 * f 0 = f 0 * 1
[PROOFSTEP]
rw [one_mul, mul_one]
[GOAL]
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n x✝ : ℕ
hd : prod (map f (range (succ x✝))) = f 0 * prod (map (fun i => f (succ i)) (range x✝))
⊢ prod (map f (range (succ (succ x✝)))) = f 0 * prod (map (fun i => f (succ i)) (range (succ x✝)))
[PROOFSTEP]
rw [List.prod_range_succ, hd, mul_assoc, ← List.prod_range_succ]
[GOAL]
α : Type u
l : List α
⊢ unzip (enum l) = (range (length l), l)
[PROOFSTEP]
simp only [enum_eq_zip_range, unzip_zip, length_range]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ unzip (enumFrom n l) = (range' n (length l), l)
[PROOFSTEP]
simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
[GOAL]
α : Type u
n i : ℕ
h : i < length (finRange n)
⊢ get (finRange n) { val := i, isLt := h } = { val := i, isLt := (_ : i < n) }
[PROOFSTEP]
simp only [finRange, get_range, get_pmap]
  --Porting note: new theorem, corresponding theorem used to be in Data.List.FinRange
[GOAL]
α : Type u
l : List α
⊢ length (map (get l) (finRange (length l))) = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
⊢ ∀ (n : ℕ) (h₁ : n < length (map (get l) (finRange (length l)))) (h₂ : n < length l),
    get (map (get l) (finRange (length l))) { val := n, isLt := h₁ } = get l { val := n, isLt := h₂ }
[PROOFSTEP]
simp


[GOAL]
n : ℕ
⊢ Ico 0 n = range n
[PROOFSTEP]
rw [Ico, tsub_zero, range_eq_range']
[GOAL]
n m : ℕ
⊢ List.length (Ico n m) = m - n
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ List.length (range' n (m - n)) = m - n
[PROOFSTEP]
simp only [length_range']
[GOAL]
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (Ico n m)
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range' n (m - n))
[PROOFSTEP]
simp only [pairwise_lt_range']
[GOAL]
n m : ℕ
⊢ Nodup (Ico n m)
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ Nodup (range' n (m - n))
[PROOFSTEP]
simp only [nodup_range']
[GOAL]
n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m
[PROOFSTEP]
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
[GOAL]
n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m
[PROOFSTEP]
simp [Ico, this]
[GOAL]
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
cases' le_total n m with hnm hmn
[GOAL]
case inl
n m l : ℕ
hnm : n ≤ m
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
rw [add_tsub_cancel_of_le hnm]
[GOAL]
case inr
n m l : ℕ
hmn : m ≤ n
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr hmn, add_zero]
[GOAL]
case inr
n m l : ℕ
hmn : m ≤ n
⊢ n ≤ l ∧ l < n ↔ n ≤ l ∧ l < m
[PROOFSTEP]
exact and_congr_right fun hnl => Iff.intro (fun hln => (not_le_of_gt hln hnl).elim) fun hlm => lt_of_lt_of_le hlm hmn
[GOAL]
n m : ℕ
h : m ≤ n
⊢ Ico n m = []
[PROOFSTEP]
simp [Ico, tsub_eq_zero_iff_le.mpr h]
[GOAL]
n m k : ℕ
⊢ map ((fun x x_1 => x + x_1) k) (Ico n m) = Ico (n + k) (m + k)
[PROOFSTEP]
rw [Ico, Ico, map_add_range', add_tsub_add_eq_tsub_right m k, add_comm n k]
[GOAL]
n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x => x - k) (Ico n m) = Ico (n - k) (m - k)
[PROOFSTEP]
rw [Ico, Ico, tsub_tsub_tsub_cancel_right h₁, map_sub_range' _ _ _ h₁]
[GOAL]
n m : ℕ
h : Ico n m = []
⊢ m - n = 0
[PROOFSTEP]
rw [← length, h, List.length]
[GOAL]
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l
[PROOFSTEP]
dsimp only [Ico]
[GOAL]
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)
[PROOFSTEP]
convert range'_append n (m - n) (l - m) 1 using 2
[GOAL]
case h.e'_2.h.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
[PROOFSTEP]
rw [one_mul, add_tsub_cancel_of_le hnm]
[GOAL]
case h.e'_3.h.e'_2
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = l - m + (m - n)
[PROOFSTEP]
rw [tsub_add_tsub_cancel hml hnm]
[GOAL]
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []
[PROOFSTEP]
apply eq_nil_iff_forall_not_mem.2
[GOAL]
n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
[PROOFSTEP]
intro a
[GOAL]
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
[PROOFSTEP]
simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
[GOAL]
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a
[PROOFSTEP]
intro _ h₂ h₃
[GOAL]
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
[PROOFSTEP]
exfalso
[GOAL]
case h
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False
[PROOFSTEP]
exact not_lt_of_ge h₃ h₂
[GOAL]
n : ℕ
⊢ Ico n (n + 1) = [n]
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n : ℕ
⊢ range' n (n + 1 - n) = [n]
[PROOFSTEP]
simp [range', add_tsub_cancel_left]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]
[PROOFSTEP]
rwa [← succ_singleton, append_consecutive]
[GOAL]
case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
[PROOFSTEP]
exact Nat.le_succ _
[GOAL]
n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m
[PROOFSTEP]
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
[GOAL]
n m : ℕ
h : n < m
⊢ [n] ++ Ico (succ n) m = n :: Ico (n + 1) m
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]
[PROOFSTEP]
dsimp [Ico]
[GOAL]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (m - (m - 1)) = [m - 1]
[PROOFSTEP]
rw [tsub_tsub_cancel_of_le (succ_le_of_lt h)]
[GOAL]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (succ 0) = [m - 1]
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero]
[GOAL]
n m : ℕ
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
by_cases n < m
[GOAL]
n m : ℕ
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
by_cases n < m
[GOAL]
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
rw [eq_cons h]
[GOAL]
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (n :: Ico (n + 1) m)
[PROOFSTEP]
exact chain_succ_range' _ _ 1
[GOAL]
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
rw [eq_nil_of_le (le_of_not_gt h)]
[GOAL]
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) []
[PROOFSTEP]
trivial
[GOAL]
n m : ℕ
⊢ ¬m ∈ Ico n m
[PROOFSTEP]
simp
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true
[PROOFSTEP]
simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_True]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true
[PROOFSTEP]
simp only [decide_eq_true_eq, not_lt]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
[PROOFSTEP]
apply le_trans hln
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k
[PROOFSTEP]
exact (mem.1 hk).1
[GOAL]
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
cases' le_total n l with hnl hln
[GOAL]
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l), filter_lt_of_le_bot (le_refl l),
  append_nil]
[GOAL]
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]
[GOAL]
n m l : ℕ
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
cases' le_total m l with hml hlm
[GOAL]
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
rw [min_eq_left hml, filter_lt_of_top_le hml]
[GOAL]
case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
rw [min_eq_right hlm, filter_lt_of_ge hlm]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true
[PROOFSTEP]
rw [decide_eq_true_eq]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
[PROOFSTEP]
exact le_trans hln (mem.1 hk).1
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true
[PROOFSTEP]
rw [decide_eq_true_eq]
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
[PROOFSTEP]
exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)
[GOAL]
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
cases' le_total l m with hlm hml
[GOAL]
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l), filter_le_of_le_bot (le_refl l),
  nil_append]
[GOAL]
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
rw [eq_nil_of_le hml, filter_le_of_top_le hml]
[GOAL]
n m l : ℕ
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
cases' le_total n l with hnl hln
[GOAL]
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
rw [max_eq_right hnl, filter_le_of_le hnl]
[GOAL]
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
rw [max_eq_left hln, filter_le_of_le_bot hln]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
[PROOFSTEP]
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
[GOAL]
n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
[PROOFSTEP]
simp [filter_lt n m (n + 1), r]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = [n]
[PROOFSTEP]
rw [← filter_lt_of_succ_bot hnm]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
[PROOFSTEP]
exact
  filter_congr' fun _ _ => by
    rw [decide_eq_true_eq, decide_eq_true_eq]
    exact lt_succ_iff.symm
[GOAL]
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = true ↔ decide (x✝¹ < n + 1) = true
[PROOFSTEP]
rw [decide_eq_true_eq, decide_eq_true_eq]
[GOAL]
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ x✝¹ ≤ n ↔ x✝¹ < n + 1
[PROOFSTEP]
exact lt_succ_iff.symm
[GOAL]
n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
by_cases h₁ : n < a
[GOAL]
case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
left
[GOAL]
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a
[PROOFSTEP]
exact h₁
[GOAL]
case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
right
[GOAL]
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
by_cases h₂ : n ∈ Ico a b
[GOAL]
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
right
[GOAL]
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b
[PROOFSTEP]
exact h₂
[GOAL]
case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
left
[GOAL]
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n
[PROOFSTEP]
simp only [Ico.mem, not_and, not_lt] at *
[GOAL]
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n
[PROOFSTEP]
exact h₂ h₁