[GOAL]
⊢ φ 1 = 1
[PROOFSTEP]
simp [totient]
[GOAL]
n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
[PROOFSTEP]
let e : {m | m < n ∧ n.coprime m} ≃ Finset.filter n.coprime (Finset.range n) :=
  { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    left_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta]
    right_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta] }
[GOAL]
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ ↑m ∈ filter (coprime n) (range n)
[PROOFSTEP]
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
[GOAL]
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ ↑m ∈ {m | m < n ∧ coprime n m}
[PROOFSTEP]
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
[GOAL]
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ (fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) })
      ((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) =
    m
[PROOFSTEP]
simp only [Subtype.coe_mk, Subtype.coe_eta]
[GOAL]
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ (fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) })
      ((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) =
    m
[PROOFSTEP]
simp only [Subtype.coe_mk, Subtype.coe_eta]
[GOAL]
n : ℕ
e : ↑{m | m < n ∧ coprime n m} ≃ { x // x ∈ filter (coprime n) (range n) } :=
  { toFun := fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) },
    invFun := fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) },
    left_inv :=
      (_ :
        ∀ (m : ↑{m | m < n ∧ coprime n m}),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) < n ∧
                    coprime n ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m)) } =
            m),
    right_inv :=
      (_ :
        ∀ (m : { x // x ∈ filter (coprime n) (range n) }),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) ∈
                    filter (coprime n) (range n)) } =
            m) }
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
[PROOFSTEP]
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
[GOAL]
n : ℕ
hn : 1 < n
⊢ 0 ∈ range n ∧ ¬coprime n 0
[PROOFSTEP]
simp [hn.ne', pos_of_gt hn]
[GOAL]
⊢ 0 < 0 → 0 < φ 0
[PROOFSTEP]
decide
[GOAL]
⊢ 0 < 1 → 0 < φ 1
[PROOFSTEP]
simp [totient]
[GOAL]
n : ℕ
x✝ : 0 < n + 2
⊢ 1 < n + 2
[PROOFSTEP]
simp
[GOAL]
a n : ℕ
⊢ card (filter (coprime a) (Ico n (n + a))) = φ a
[PROOFSTEP]
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
[GOAL]
case pp
a n : ℕ
⊢ Function.Periodic (coprime a) a
[PROOFSTEP]
exact periodic_coprime a
[GOAL]
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
conv_lhs => rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
| card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
rw [← Nat.mod_add_div n a]
[GOAL]
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * (n / a))))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
induction' n / a with i ih
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ φ a * (zero + 1)
[PROOFSTEP]
rw [← filter_coprime_Ico_eq_totient a k]
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * zero)))) ≤ card (filter (coprime a) (Ico k (k + a))) * (zero + 1)
[PROOFSTEP]
simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos), Nat.zero_eq, zero_add]
  --Porting note: below line was `mono`
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ card (filter (coprime a) (Ico k (k + n % a))) ≤ card (filter (coprime a) (Ico k (k + a)))
[PROOFSTEP]
refine Finset.card_mono ?_
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ filter (coprime a) (Ico k (k + n % a)) ≤ filter (coprime a) (Ico k (k + a))
[PROOFSTEP]
refine' monotone_filter_left a.coprime _
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ≤ Ico k (k + a)
[PROOFSTEP]
simp only [Finset.le_eq_subset]
[GOAL]
case zero
a k n : ℕ
a_pos : 0 < a
⊢ Ico k (k + n % a) ⊆ Ico k (k + a)
[PROOFSTEP]
exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k)
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + a * succ i)))) ≤ φ a * (succ i + 1)
[PROOFSTEP]
simp only [mul_succ]
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + (n % a + a * i)))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + (n % a + (a * i + a))))) ≤ φ a * i + φ a + φ a
[PROOFSTEP]
simp_rw [← add_assoc] at ih ⊢
[GOAL]
case succ
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) ≤ φ a * i + φ a + φ a
[PROOFSTEP]
calc
  (filter a.coprime (Ico k (k + n % a + a * i + a))).card =
      (filter a.coprime (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card :=
    by
    congr
    rw [Ico_union_Ico_eq_Ico]
    rw [add_assoc]
    exact le_self_add
    exact le_self_add
  _ ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + a.totient :=
    by
    rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
    apply card_union_le
  _ ≤ a.totient * i + a.totient + a.totient := add_le_add_right ih (totient a)
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i + a))) =
    card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)))
[PROOFSTEP]
congr
[GOAL]
case e_s.e_s
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) = Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)
[PROOFSTEP]
rw [Ico_union_Ico_eq_Ico]
[GOAL]
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + n % a + a * i
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case e_s.e_s.hab
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k ≤ k + (n % a + a * i)
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
exact le_self_add
[GOAL]
case e_s.e_s.hbc
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ k + n % a + a * i ≤ k + n % a + a * i + a
[PROOFSTEP]
exact le_self_add
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card (filter (coprime a) (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) + φ a
[PROOFSTEP]
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
[GOAL]
a k n : ℕ
a_pos : 0 < a
i : ℕ
ih : card (filter (coprime a) (Ico k (k + n % a + a * i))) ≤ φ a * (i + 1)
⊢ card
      (filter (coprime a) (Ico k (k + n % a + a * i)) ∪
        filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a))) ≤
    card (filter (coprime a) (Ico k (k + n % a + a * i))) +
      card (filter (coprime a) (Ico (k + n % a + a * i) (k + n % a + a * i + a)))
[PROOFSTEP]
apply card_union_le
[GOAL]
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) n } = φ n
[PROOFSTEP]
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
[GOAL]
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) (m + 1) } = φ (m + 1)
[PROOFSTEP]
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ← Fin.sum_univ_eq_sum_range,
  @Nat.coprime_comm (m + 1)]
[GOAL]
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if coprime (ZMod.val a) (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if coprime (↑i) (m + 1) then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : 2 < n
⊢ Even (φ n)
[PROOFSTEP]
haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
[GOAL]
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
[PROOFSTEP]
haveI : NeZero n := NeZero.of_gt hn
[GOAL]
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
[PROOFSTEP]
suffices 2 = orderOf (-1 : (ZMod n)ˣ)
  by
  rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
  exact orderOf_dvd_card_univ
[GOAL]
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)
[PROOFSTEP]
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
[GOAL]
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ
[PROOFSTEP]
exact orderOf_dvd_card_univ
[GOAL]
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)
[PROOFSTEP]
rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
cases' Nat.mul_eq_zero.1 hmn0 with h h
[GOAL]
case inl
m n : ℕ
h✝ : coprime m n
hmn0 : m * n = 0
h : m = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [totient_zero, mul_zero, zero_mul, h]
[GOAL]
case inr
m n : ℕ
h✝ : coprime m n
hmn0 : m * n = 0
h : n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [totient_zero, mul_zero, zero_mul, h]
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero (m * n) := ⟨hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
[PROOFSTEP]
simp only [← ZMod.card_units_eq_totient]
[GOAL]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
[PROOFSTEP]
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
  Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]
[GOAL]
n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
rcases d.eq_zero_or_pos with (rfl | hd0)
[GOAL]
case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = Finset.card (filter (fun k => gcd n k = 0) (range n))
[PROOFSTEP]
simp [eq_zero_of_zero_dvd hnd]
[GOAL]
case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
rcases hnd with ⟨x, rfl⟩
[GOAL]
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
[PROOFSTEP]
rw [Nat.mul_div_cancel_left x hd0]
[GOAL]
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
[PROOFSTEP]
apply Finset.card_congr fun k _ => d * k
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a ∈ filter (coprime x) (range x) → d * a ∈ filter (fun k => gcd (d * x) k = d) (range (d * x))
[PROOFSTEP]
simp only [mem_filter, mem_range, and_imp, coprime]
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a < x → gcd x a = 1 → d * a < d * x ∧ gcd (d * x) (d * a) = d
[PROOFSTEP]
refine' fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, _⟩
[GOAL]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : gcd x a = 1
⊢ gcd (d * x) (d * a) = d
[PROOFSTEP]
rw [gcd_mul_left, ha2, mul_one]
[GOAL]
case inr.intro.h₂
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a b : ℕ), a ∈ filter (coprime x) (range x) → b ∈ filter (coprime x) (range x) → d * a = d * b → a = b
[PROOFSTEP]
simp [hd0.ne']
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b ∈ filter (fun k => gcd (d * x) k = d) (range (d * x)) → ∃ a ha, d * a = b
[PROOFSTEP]
simp only [mem_filter, mem_range, exists_prop, and_imp]
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b < d * x → gcd (d * x) b = d → ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
refine' fun b hb1 hb2 => _
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
have : d ∣ b := by
  rw [← hb2]
  apply gcd_dvd_right
[GOAL]
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ d ∣ b
[PROOFSTEP]
rw [← hb2]
[GOAL]
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ gcd (d * x) b ∣ b
[PROOFSTEP]
apply gcd_dvd_right
[GOAL]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
[PROOFSTEP]
rcases this with ⟨q, rfl⟩
[GOAL]
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = d * q
[PROOFSTEP]
refine' ⟨q, ⟨⟨(mul_lt_mul_left hd0).1 hb1, _⟩, rfl⟩⟩
[GOAL]
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ coprime x q
[PROOFSTEP]
rwa [gcd_mul_left, mul_right_eq_self_iff hd0] at hb2
[GOAL]
n : ℕ
⊢ Finset.sum (divisors n) φ = n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
⊢ Finset.sum (divisors 0) φ = 0
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
hn : n > 0
⊢ Finset.sum (divisors n) φ = n
[PROOFSTEP]
rw [← sum_div_divisors n φ]
[GOAL]
case inr
n : ℕ
hn : n > 0
⊢ ∑ d in divisors n, φ (n / d) = n
[PROOFSTEP]
have : n = ∑ d : ℕ in n.divisors, (filter (fun k : ℕ => n.gcd k = d) (range n)).card :=
  by
  nth_rw 1 [← card_range n]
  refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
  apply gcd_dvd_left
[GOAL]
n : ℕ
hn : n > 0
⊢ n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
nth_rw 1 [← card_range n]
[GOAL]
n : ℕ
hn : n > 0
⊢ Finset.card (range n) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
[GOAL]
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ gcd n x ∣ n
[PROOFSTEP]
apply gcd_dvd_left
[GOAL]
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = n
[PROOFSTEP]
nth_rw 3 [this]
[GOAL]
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
[PROOFSTEP]
exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)
[GOAL]
n : ℕ
⊢ ∑ m in filter (fun x => x ∣ n) (range (succ n)), φ m = n
[PROOFSTEP]
convert sum_totient _ using 1
[GOAL]
case h.e'_2
n : ℕ
⊢ ∑ m in filter (fun x => x ∣ n) (range (succ n)), φ m = Finset.sum (divisors n) φ
[PROOFSTEP]
simp only [Nat.divisors, sum_filter, range_eq_Ico]
[GOAL]
case h.e'_2
n : ℕ
⊢ (∑ a in Ico 0 (succ n), if a ∣ n then φ a else 0) = ∑ a in Ico 1 (n + 1), if a ∣ n then φ a else 0
[PROOFSTEP]
rw [sum_eq_sum_Ico_succ_bot]
[GOAL]
case h.e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k in Ico (0 + 1) (succ n), if k ∣ n then φ k else 0) =
    ∑ a in Ico 1 (n + 1), if a ∣ n then φ a else 0
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.hab
n : ℕ
⊢ 0 < succ n
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) = range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))
[PROOFSTEP]
rw [sdiff_eq_filter]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) =
    filter (fun x => ¬x ∈ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))
[PROOFSTEP]
apply filter_congr
[GOAL]
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (p ^ (n + 1)) → (coprime (p ^ (n + 1)) x ↔ ¬x ∈ image (fun x => x * p) (range (p ^ n)))
[PROOFSTEP]
simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos, mem_image, not_exists, hp.coprime_iff_not_dvd]
[GOAL]
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x < p ^ (n + 1) → (¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x))
[PROOFSTEP]
intro a ha
[GOAL]
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
[PROOFSTEP]
constructor
[GOAL]
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
[PROOFSTEP]
intro hap b h
[GOAL]
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
[PROOFSTEP]
rcases h with ⟨_, rfl⟩
[GOAL]
case H.mp.intro
p : ℕ
hp : Prime p
n b : ℕ
left✝ : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False
[PROOFSTEP]
exact hap (dvd_mul_left _ _)
[GOAL]
case H.mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
[PROOFSTEP]
rintro h ⟨b, rfl⟩
[GOAL]
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
[PROOFSTEP]
rw [pow_succ'] at ha
[GOAL]
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
[PROOFSTEP]
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a =>
  by
  simp only [mem_image, mem_range, exists_imp]
  rintro b ⟨h, rfl⟩
  rw [pow_succ]
  exact (mul_lt_mul_right hp.pos).2 h
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ a ∈ image (fun x => x * p) (range (p ^ n)) → a ∈ range (p ^ (n + 1))
[PROOFSTEP]
simp only [mem_image, mem_range, exists_imp]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
[PROOFSTEP]
rintro b ⟨h, rfl⟩
[GOAL]
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p
[PROOFSTEP]
exact (mul_lt_mul_right hp.pos).2 h
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
h2 : image (fun x => x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
[PROOFSTEP]
rw [card_sdiff h2, card_image_of_injOn (h1.injOn _), card_range, card_range, ← one_mul (p ^ n), pow_succ', ← tsub_mul,
  one_mul, mul_comm]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)
[PROOFSTEP]
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
[GOAL]
case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < succ m
⊢ φ (p ^ succ m) = p ^ (succ m - 1) * (p - 1)
[PROOFSTEP]
exact totient_prime_pow_succ hp _
[GOAL]
p : ℕ
hp : Prime p
⊢ φ p = p - 1
[PROOFSTEP]
rw [← pow_one p, totient_prime_pow hp]
[GOAL]
p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
⊢ 0 < 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p
[PROOFSTEP]
refine' ⟨fun h => _, totient_prime⟩
[GOAL]
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
[PROOFSTEP]
replace hp : 1 < p
[GOAL]
case hp
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p
[PROOFSTEP]
apply lt_of_le_of_ne
[GOAL]
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p
[PROOFSTEP]
rwa [succ_le_iff]
[GOAL]
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p
[PROOFSTEP]
rintro rfl
[GOAL]
case hp.a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False
[PROOFSTEP]
rw [totient_one, tsub_self] at h
[GOAL]
case hp.a
hp : 0 < 1
h✝ : 1 = 1 - 1
h : 1 = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p
[PROOFSTEP]
rw [totient_eq_card_coprime, range_eq_Ico, ← Ico_insert_succ_left hp.le, Finset.filter_insert,
  if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ← Nat.card_Ico 1 p] at h
[GOAL]
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
⊢ Prime p
[PROOFSTEP]
refine' p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨_, hn⟩
[GOAL]
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n
[PROOFSTEP]
rwa [succ_le_iff, pos_iff_ne_zero]
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
[PROOFSTEP]
haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
[PROOFSTEP]
rw [ZMod.card_units_eq_totient p]
[GOAL]
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1
[PROOFSTEP]
exact Nat.le_pred_of_lt (Nat.totient_lt p hp)
[GOAL]
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
cases' eq_zero_or_neZero p with hp hp
[GOAL]
case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
subst hp
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1
[PROOFSTEP]
simp only [ZMod, not_prime_zero, false_iff_iff, zero_tsub]
  -- the subst created a non-defeq but subsingleton instance diamond; resolve it
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0
[PROOFSTEP]
suffices Fintype.card ℤˣ ≠ 0 by convert this
[GOAL]
inst✝ : Fintype (ZMod 0)ˣ
this : Fintype.card ℤˣ ≠ 0
⊢ ¬Fintype.card ℤˣ = 0
[PROOFSTEP]
convert this
[GOAL]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]
[GOAL]
⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2
[PROOFSTEP]
simp
[GOAL]
⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2
[PROOFSTEP]
simp
[GOAL]
⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
[PROOFSTEP]
have : 3 ≤ n + 3 := le_add_self
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
[PROOFSTEP]
simp only [succ_succ_ne_one, false_or_iff]
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2
[PROOFSTEP]
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩
[GOAL]
n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ φ n = Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
rw [multiplicative_factorization φ (@totient_mul) totient_one hn]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (factorization n) fun p k => φ (p ^ k)) =
    Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
apply Finsupp.prod_congr _
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ ∀ (x : ℕ), x ∈ (factorization n).support → φ (x ^ ↑(factorization n) x) = x ^ (↑(factorization n) x - 1) * (x - 1)
[PROOFSTEP]
intro p hp
[GOAL]
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ φ (p ^ ↑(factorization n) p) = p ^ (↑(factorization n) p - 1) * (p - 1)
[PROOFSTEP]
have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
[GOAL]
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ (factorization n).support
h : 0 < ↑(factorization n) p
⊢ φ (p ^ ↑(factorization n) p) = p ^ (↑(factorization n) p - 1) * (p - 1)
[PROOFSTEP]
rw [totient_prime_pow (prime_of_mem_factorization hp) h]
[GOAL]
n : ℕ
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
rw [totient_eq_prod_factorization hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    n * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
nth_rw 3 [← factorization_prod_pow_eq_self hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
simp only [← prod_factorization_eq_prod_factors, ← Finsupp.prod_mul]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun a b => a ^ (b - 1) * (a - 1) * a) =
    Finsupp.prod (factorization n) fun a b => a ^ b * (a - 1)
[PROOFSTEP]
refine' Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => _
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
[PROOFSTEP]
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < ↑(factorization n) p
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
[PROOFSTEP]
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
[GOAL]
n : ℕ
⊢ φ n = (n / ∏ p in List.toFinset (factors n), p) * ∏ p in List.toFinset (factors n), (p - 1)
[PROOFSTEP]
rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm, Nat.mul_div_assoc _ (prod_prime_factors_dvd n),
  mul_comm]
[GOAL]
n : ℕ
⊢ 0 < ∏ p in List.toFinset (factors n), p
[PROOFSTEP]
have := prod_pos (fun p => pos_of_mem_factorization (n := n))
[GOAL]
n : ℕ
this : 0 < ∏ i in (factorization n).support, i
⊢ 0 < ∏ p in List.toFinset (factors n), p
[PROOFSTEP]
simpa [prod_factorization_eq_prod_factors] using this
[GOAL]
n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
have hn' : (n : ℚ) ≠ 0 := by simp [hn]
[GOAL]
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
have hpQ : (∏ p in n.factors.toFinset, (p : ℚ)) ≠ 0 :=
  by
  rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
  exact prod_pos fun p hp => pos_of_mem_factorization hp
[GOAL]
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p in List.toFinset (factors n), ↑p ≠ 0
[PROOFSTEP]
rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
[GOAL]
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < Finsupp.prod (factorization n) fun p x => p
[PROOFSTEP]
exact prod_pos fun p hp => pos_of_mem_factorization hp
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
[PROOFSTEP]
simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod, cast_div_charZero, mul_comm_div,
  mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ∏ i in List.toFinset (factors n), ↑(i - 1) = ∏ x in List.toFinset (factors n), (1 - (↑x)⁻¹) * ↑x
[PROOFSTEP]
refine' prod_congr rfl fun p hp => _
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp : p ∈ List.toFinset (factors n)
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
have hp := pos_of_mem_factors (List.mem_toFinset.mp hp)
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
[PROOFSTEP]
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel hp', cast_pred hp]
[GOAL]
a b : ℕ
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
[PROOFSTEP]
have shuffle :
  ∀ a1 a2 b1 b2 c1 c2 : ℕ, b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2) :=
  by
  intro a1 a2 b1 b2 c1 c2 h1 h2
  calc
    a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
    _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
      congr 1
      exact div_mul_div_comm h1 h2
[GOAL]
a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
intro a1 a2 b1 b2 c1 c2 h1 h2
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
calc
  a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
  _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
    congr 1
    exact div_mul_div_comm h1 h2
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)
[PROOFSTEP]
apply mul_mul_mul_comm
[GOAL]
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
[PROOFSTEP]
exact div_mul_div_comm h1 h2
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
[PROOFSTEP]
simp only [totient_eq_div_factors_mul]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ((gcd a b / ∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (gcd a b)), (p - 1)) *
      ((a * b / ∏ p in List.toFinset (factors (a * b)), p) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    ((a / ∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors a), (p - 1)) *
        ((b / ∏ p in List.toFinset (factors b), p) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
rw [shuffle, shuffle]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
[PROOFSTEP]
rotate_left
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
repeat' apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors a), p ∣ a
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors b), p ∣ b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (gcd a b)), p ∣ gcd a b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p in List.toFinset (factors (a * b)), p ∣ a * b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
apply prod_prime_factors_dvd
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
simp only [prod_factors_gcd_mul_prod_factors_mul]
[GOAL]
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
      ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
[PROOFSTEP]
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
[GOAL]
case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p ∣ a * b
[PROOFSTEP]
exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b)
[GOAL]
a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
let d := a.gcd b
[GOAL]
a b : ℕ
d : ℕ := gcd a b
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
rcases(zero_le a).eq_or_lt with (rfl | ha0)
[GOAL]
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)
[PROOFSTEP]
simp
[GOAL]
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
[GOAL]
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)
[PROOFSTEP]
apply le_of_mul_le_mul_right _ hd0
[GOAL]
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
[PROOFSTEP]
rw [← totient_gcd_mul_totient_mul a b, mul_comm]
[GOAL]
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (gcd a b) ≤ φ (a * b) * d
[PROOFSTEP]
apply mul_le_mul_left' (Nat.totient_le d)
[GOAL]
a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha0)
[GOAL]
case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b
[PROOFSTEP]
simp [zero_dvd_iff.1 h]
[GOAL]
case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb0)
[GOAL]
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b
[PROOFSTEP]
have hab' : a.factorization.support ⊆ b.factorization.support :=
  by
  intro p
  simp only [support_factorization, List.mem_toFinset]
  apply factors_subset_of_dvd h hb0
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (factorization a).support ⊆ (factorization b).support
[PROOFSTEP]
intro p
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ (factorization a).support → p ∈ (factorization b).support
[PROOFSTEP]
simp only [support_factorization, List.mem_toFinset]
[GOAL]
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ factors a → p ∈ factors b
[PROOFSTEP]
apply factors_subset_of_dvd h hb0
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ φ a ∣ φ b
[PROOFSTEP]
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ (Finsupp.prod (factorization a) fun p k => p ^ (k - 1) * (p - 1)) ∣
    Finsupp.prod (factorization b) fun p k => p ^ (k - 1) * (p - 1)
[PROOFSTEP]
refine' Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul _ dvd_rfl
[GOAL]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
p : ℕ
x✝ : p ∈ (factorization a).support
⊢ p ^ (↑(factorization a) p - 1) ∣ p ^ (↑(factorization b) p - 1)
[PROOFSTEP]
exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
have h1 := totient_gcd_mul_totient_mul p n
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (gcd p n) * φ (p * n) = φ p * φ n * gcd p n
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
rw [gcd_eq_left h, mul_assoc] at h1
[GOAL]
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
[PROOFSTEP]
simpa [(totient_pos hp.pos).ne', mul_comm] using h1
[GOAL]
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n
[PROOFSTEP]
rw [totient_mul _, totient_prime hp]
[GOAL]
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ coprime p n
[PROOFSTEP]
simpa [h] using coprime_or_dvd_of_prime hp n


[GOAL]
k x y : ℕ
h : x ≤ y / k
⊢ x * k ≤ y
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
case neg k x y : ℕ h : x ≤ y / k hk : ¬k = 0 ⊢ x * k ≤ y
[PROOFSTEP]
case pos => rw [hk, mul_zero]; exact zero_le _
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case pos => rw [hk, mul_zero]; exact zero_le _
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
[PROOFSTEP]
rw [hk, mul_zero]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ 0 ≤ y
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case neg => rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case neg => rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
a b c d : ℕ
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
case neg a b c d : ℕ hb : ¬b = 0 ⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hb]
[GOAL]
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hb]
[GOAL]
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
simp [hb]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
by_cases hd : d = 0
[GOAL]
case pos
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
case neg a b c d : ℕ hb : ¬b = 0 hd : ¬d = 0 ⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hd]
[GOAL]
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hd]
[GOAL]
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
simp [hd]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
have hbd : b * d ≠ 0 := mul_ne_zero hb hd
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a * c
[PROOFSTEP]
transitivity ((a / b) * b) * ((c / d) * d)
[GOAL]
case neg.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a / b * b * (c / d * d)
[PROOFSTEP]
apply le_of_eq
[GOAL]
case neg.a.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) = a / b * b * (c / d * d)
[PROOFSTEP]
simp only [mul_assoc, mul_left_comm]
[GOAL]
case neg.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b * (c / d * d) ≤ a * c
[PROOFSTEP]
apply Nat.mul_le_mul
[GOAL]
case neg.a.h₁
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b ≤ a
[PROOFSTEP]
apply div_mul_le_self
[GOAL]
case neg.a.h₂
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ c / d * d ≤ c
[PROOFSTEP]
apply div_mul_le_self
[GOAL]
n k : ℕ
⊢ let iter_next := fun n guess => (guess + n / guess) / 2;
  sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
[PROOFSTEP]
intro iter_next
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
by_cases h : (k + n / k) / 2 < k
[GOAL]
case pos
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
case neg
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case pos => simp [if_pos h]; exact iter_fp_bound _ _
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case pos => simp [if_pos h]; exact iter_fp_bound _ _
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
simp [if_pos h]
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ sqrt.iter n ((k + n / k) / 2) ≤ (sqrt.iter n ((k + n / k) / 2) + n / sqrt.iter n ((k + n / k) / 2)) / 2
[PROOFSTEP]
exact iter_fp_bound _ _
[GOAL]
case neg
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case neg => simp [if_neg h]; exact Nat.le_of_not_lt h
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case neg => simp [if_neg h]; exact Nat.le_of_not_lt h
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
simp [if_neg h]
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ k ≤ (k + n / k) / 2
[PROOFSTEP]
exact Nat.le_of_not_lt h
[GOAL]
x✝ : ℕ
⊢ 4 * 0 * x✝ ≤ (0 + x✝) * (0 + x✝)
[PROOFSTEP]
rw [mul_zero, zero_mul]
[GOAL]
x✝ : ℕ
⊢ 0 ≤ (0 + x✝) * (0 + x✝)
[PROOFSTEP]
exact zero_le _
[GOAL]
x✝ : ℕ
⊢ 4 * x✝ * 0 ≤ (x✝ + 0) * (x✝ + 0)
[PROOFSTEP]
rw [mul_zero]
[GOAL]
x✝ : ℕ
⊢ 0 ≤ (x✝ + 0) * (x✝ + 0)
[PROOFSTEP]
exact zero_le _
[GOAL]
a b : ℕ
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))
[PROOFSTEP]
have ih := add_le_add_right (@AM_GM a b) 4
[GOAL]
a b : ℕ
ih : 4 * a * b + 4 ≤ (a + b) * (a + b) + 4
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))
[PROOFSTEP]
simp only [mul_add, add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, one_mul, mul_one] at ih ⊢
[GOAL]
a b : ℕ
ih : a * b + a * b + a * b + a * b + (1 + 1 + 1 + 1) ≤ a * a + b * a + (a * b + b * b) + (1 + 1 + 1 + 1)
⊢ a * b + a * b + a * b + a * b + (b + b + b + b) + (a + a + a + a + (1 + 1 + 1 + 1)) ≤
    a * a + a + (b * a + a) + (a + 1 + (b + 1)) + (a * b + b + (b * b + b) + (a + 1 + (b + 1)))
[PROOFSTEP]
simp only [add_assoc, add_left_comm, add_le_add_iff_left] at ih ⊢
[GOAL]
a b : ℕ
ih :
  a * b + (a * b + (a * b + (a * b + (1 + (1 + (1 + 1)))))) ≤ a * a + (a * b + (b * a + (b * b + (1 + (1 + (1 + 1))))))
⊢ a * b + (a * b + (a * b + (a * b + (1 + (1 + (1 + 1)))))) ≤ a * a + (a * b + (b * a + (b * b + (1 + (1 + (1 + 1))))))
[PROOFSTEP]
exact ih
[GOAL]
n guess : ℕ
⊢ iter n guess * iter n guess ≤ n
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n guess : ℕ
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
let next := (guess + n / guess) / 2
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
by_cases h : next < guess
[GOAL]
case pos
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
case neg
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case pos => simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case pos => simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
case neg
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case neg =>
  simp only [dif_neg h]
  apply Nat.mul_le_of_le_div
  apply le_of_add_le_add_left (a := guess)
  rw [← mul_two, ← le_div_iff_mul_le]
  · exact le_of_not_lt h
  · exact zero_lt_two
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case neg =>
  simp only [dif_neg h]
  apply Nat.mul_le_of_le_div
  apply le_of_add_le_add_left (a := guess)
  rw [← mul_two, ← le_div_iff_mul_le]
  · exact le_of_not_lt h
  · exact zero_lt_two
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
simp only [dif_neg h]
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess * guess ≤ n
[PROOFSTEP]
apply Nat.mul_le_of_le_div
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ n / guess
[PROOFSTEP]
apply le_of_add_le_add_left (a := guess)
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess + guess ≤ guess + n / guess
[PROOFSTEP]
rw [← mul_two, ← le_div_iff_mul_le]
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ (guess + n / guess) / 2
[PROOFSTEP]
exact le_of_not_lt h
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n < (iter n guess + 1) * (iter n guess + 1)
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
let m := (guess + n / guess) / 2
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
by_cases h : m < guess
[GOAL]
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case pos =>
  suffices : n < (m + 1) * (m + 1)
  · simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
  refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
  apply lt_of_le_of_lt AM_GM
  rw [show (4 : ℕ) = 2 * 2 from rfl]
  rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
  refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
  rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
    show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
  have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
    rw [mul_comm]
    exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
  refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
  rw [add_assoc, mul_add]
  exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case pos =>
  suffices : n < (m + 1) * (m + 1)
  · simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
  refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
  apply lt_of_le_of_lt AM_GM
  rw [show (4 : ℕ) = 2 * 2 from rfl]
  rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
  refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
  rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
    show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
  have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
    rw [mul_comm]
    exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
  refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
  rw [add_assoc, mul_add]
  exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
suffices : n < (m + 1) * (m + 1)
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
this : n < (m + 1) * (m + 1)
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n < (m + 1) * (m + 1)
[PROOFSTEP]
refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
apply lt_of_le_of_lt AM_GM
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
rw [show (4 : ℕ) = 2 * 2 from rfl]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * 2 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))
[PROOFSTEP]
refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ guess * guess + n < 2 * guess * succ ((guess + n / guess) / 2)
[PROOFSTEP]
rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
  show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
[PROOFSTEP]
have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
  rw [mul_comm]
  exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
a : ℕ
⊢ a ≤ 2 * ((a + 1) / 2)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
a : ℕ
⊢ a ≤ (a + 1) / 2 * 2
[PROOFSTEP]
exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
[PROOFSTEP]
refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (guess + n / guess + 1)
[PROOFSTEP]
rw [add_assoc, mul_add]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * guess + guess * (n / guess + 1)
[PROOFSTEP]
exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case neg => simpa only [dif_neg h] using hn
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case neg => simpa only [dif_neg h] using hn
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
simpa only [dif_neg h] using hn


[GOAL]
⊢ factors 0 = []
[PROOFSTEP]
rw [factors]
[GOAL]
⊢ factors 1 = []
[PROOFSTEP]
rw [factors]
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors n → Prime p
[PROOFSTEP]
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
  intro p h
  let m := minFac (k + 2)
  have : (k + 2) / m < (k + 2) := factors_lemma
  have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) := List.mem_cons.1 (by rwa [factors] at h )
  exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 0 → Prime p
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 1 → Prime p
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors (k + 2) → Prime p
[PROOFSTEP]
intro p h
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
⊢ Prime p
[PROOFSTEP]
let m := minFac (k + 2)
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
⊢ Prime p
[PROOFSTEP]
have : (k + 2) / m < (k + 2) := factors_lemma
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ Prime p
[PROOFSTEP]
have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) := List.mem_cons.1 (by rwa [factors] at h )
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ p ∈ m :: factors ((k + 2) / m)
[PROOFSTEP]
rwa [factors] at h
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
⊢ Prime p
[PROOFSTEP]
exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
h₂ : p = m
⊢ k + 2 ≠ 1
[PROOFSTEP]
simp
[GOAL]
⊢ 0 ≠ 0 → List.prod (factors 0) = 0
[PROOFSTEP]
simp
[GOAL]
⊢ 1 ≠ 0 → List.prod (factors 1) = 1
[PROOFSTEP]
simp
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.prod (factors (k + 2)) = k + 2
[PROOFSTEP]
have h₁ : (k + 2) / m ≠ 0 := fun h =>
  by
  have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
  rw [zero_mul] at this ; exact (show k + 2 ≠ 0 by simp) this
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False
[PROOFSTEP]
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False
[PROOFSTEP]
rw [zero_mul] at this
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
[PROOFSTEP]
exact (show k + 2 ≠ 0 by simp) this
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ List.prod (factors (k + 2)) = k + 2
[PROOFSTEP]
rw [factors, List.prod_cons, prod_factors h₁, Nat.mul_div_cancel' (minFac_dvd _)]
[GOAL]
p : ℕ
hp : Prime p
⊢ factors p = [p]
[PROOFSTEP]
have : p = p - 2 + 2 := (tsub_eq_iff_eq_add_of_le hp.two_le).mp rfl
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ factors p = [p]
[PROOFSTEP]
rw [this, Nat.factors]
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (let m := minFac (p - 2 + 2);
    let_fun this := (_ : (p - 2 + 2) / minFac (p - 2 + 2) < p - 2 + 2);
    m :: factors ((p - 2 + 2) / m)) =
    [p - 2 + 2]
[PROOFSTEP]
simp only [Eq.symm this]
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ minFac p :: factors (p / minFac p) = [p]
[PROOFSTEP]
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
[GOAL]
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : minFac p = p
⊢ minFac p :: factors (p / minFac p) = [p]
[PROOFSTEP]
simp only [this, Nat.factors, Nat.div_self (Nat.Prime.pos hp)]
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors n)
[PROOFSTEP]
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
  intro a h
  let m := minFac (k + 2)
  have : (k + 2) / m < (k + 2) := factors_lemma
  rw [factors]
  refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
  exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 0)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 1)
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
intro a h
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
let m := minFac (k + 2)
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
have : (k + 2) / m < (k + 2) := factors_lemma
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
rw [factors]
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a
    (let m := minFac (k + 2);
    let_fun this := (_ : (k + 2) / minFac (k + 2) < k + 2);
    m :: factors ((k + 2) / m))
[PROOFSTEP]
refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1
[PROOFSTEP]
simp
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / minFac (k + 2) → minFac (k + 2) ≤ p
[PROOFSTEP]
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
[GOAL]
n : ℕ
⊢ factors (n + 2) = minFac (n + 2) :: factors ((n + 2) / minFac (n + 2))
[PROOFSTEP]
rw [factors]
[GOAL]
n : ℕ
⊢ factors n = [] ↔ n = 0 ∨ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ factors n = [] → n = 0 ∨ n = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → factors n = []
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : factors n = []
⊢ n = 0 ∨ n = 1
[PROOFSTEP]
rcases n with (_ | _ | n)
[GOAL]
case mp.zero
h : factors zero = []
⊢ zero = 0 ∨ zero = 1
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case mp.succ.zero
h : factors (succ zero) = []
⊢ succ zero = 0 ∨ succ zero = 1
[PROOFSTEP]
exact Or.inr rfl
[GOAL]
case mp.succ.succ
n : ℕ
h : factors (succ (succ n)) = []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
[PROOFSTEP]
rw [factors] at h
[GOAL]
case mp.succ.succ
n : ℕ
h :
  (let m := minFac (n + 2);
    let_fun this := (_ : (n + 2) / minFac (n + 2) < n + 2);
    m :: factors ((n + 2) / m)) =
    []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
[PROOFSTEP]
injection h
[GOAL]
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ factors n = []
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case mpr.inl
⊢ factors 0 = []
[PROOFSTEP]
exact factors_zero
[GOAL]
case mpr.inr
⊢ factors 1 = []
[PROOFSTEP]
exact factors_one
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : factors a ~ factors b
⊢ a = b
[PROOFSTEP]
simpa [prod_factors ha, prod_factors hb] using List.Perm.prod_eq h
[GOAL]
n p : ℕ
h : p ∈ factors n
⊢ p ∣ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ∣ 0
[PROOFSTEP]
exact dvd_zero p
[GOAL]
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ∣ n
[PROOFSTEP]
rwa [← mem_factors_iff_dvd hn.ne' (prime_of_mem_factors h)]
[GOAL]
n p : ℕ
h : p ∈ factors n
⊢ p ≤ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ≤ 0
[PROOFSTEP]
rw [factors_zero] at h
[GOAL]
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
[PROOFSTEP]
cases h
[GOAL]
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ≤ n
[PROOFSTEP]
exact le_of_dvd hn (dvd_of_mem_factors h)
[GOAL]
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ factors n
[PROOFSTEP]
refine' perm_of_prod_eq_prod _ _ _
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ prod l = prod (factors n)
[PROOFSTEP]
rw [h₁]
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = prod (factors n)
[PROOFSTEP]
refine' (prod_factors _).symm
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : prod l = 0
⊢ False
[PROOFSTEP]
rw [prod_eq_zero_iff] at h₁
[GOAL]
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
[PROOFSTEP]
exact Prime.ne_zero (h₂ 0 h₁) rfl
[GOAL]
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p
[PROOFSTEP]
simp_rw [← prime_iff]
[GOAL]
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p
[PROOFSTEP]
exact h₂
[GOAL]
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → _root_.Prime p
[PROOFSTEP]
simp_rw [← prime_iff]
[GOAL]
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → Prime p
[PROOFSTEP]
exact fun p => prime_of_mem_factors
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ factors (p ^ n) = replicate n p
[PROOFSTEP]
symm
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = factors (p ^ n)
[PROOFSTEP]
rw [← List.replicate_perm]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ factors (p ^ n)
[PROOFSTEP]
apply Nat.factors_unique (List.prod_replicate n p)
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
[PROOFSTEP]
intro q hq
[GOAL]
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q
[PROOFSTEP]
rwa [eq_of_mem_replicate hq]
[GOAL]
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ length (factors n)
[PROOFSTEP]
set k := n.factors.length
[GOAL]
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := length (factors n)
⊢ n = p ^ k
[PROOFSTEP]
rw [← prod_factors hpos, ← prod_replicate k p,
  eq_replicate_of_mem fun d hd => h (prime_of_mem_factors hd) (dvd_of_mem_factors hd)]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
refine' (factors_unique _ _).symm
[GOAL]
case refine'_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ prod (factors a ++ factors b) = a * b
[PROOFSTEP]
rw [List.prod_append, prod_factors ha, prod_factors hb]
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ factors a ++ factors b → Prime p
[PROOFSTEP]
intro p hp
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ++ factors b
⊢ Prime p
[PROOFSTEP]
rw [List.mem_append] at hp
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ∨ p ∈ factors b
⊢ Prime p
[PROOFSTEP]
cases' hp with hp' hp'
[GOAL]
case refine'_2.inl
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ factors a
⊢ Prime p
[PROOFSTEP]
exact prime_of_mem_factors hp'
[GOAL]
case refine'_2.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ factors b
⊢ Prime p
[PROOFSTEP]
exact prime_of_mem_factors hp'
[GOAL]
a b : ℕ
hab : coprime a b
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
rcases a.eq_zero_or_pos with (rfl | ha)
[GOAL]
case inl
b : ℕ
hab : coprime 0 b
⊢ factors (0 * b) ~ factors 0 ++ factors b
[PROOFSTEP]
simp [(coprime_zero_left _).mp hab]
[GOAL]
case inr
a b : ℕ
hab : coprime a b
ha : a > 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inr.inl
a : ℕ
ha : a > 0
hab : coprime a 0
⊢ factors (a * 0) ~ factors a ++ factors 0
[PROOFSTEP]
simp [(coprime_zero_right _).mp hab]
[GOAL]
case inr.inr
a b : ℕ
hab : coprime a b
ha : a > 0
hb : b > 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
exact perm_factors_mul ha.ne' hb.ne'
[GOAL]
n k : ℕ
h : k ≠ 0
⊢ factors n <+ factors (n * k)
[PROOFSTEP]
cases' n with hn
[GOAL]
case zero
k : ℕ
h : k ≠ 0
⊢ factors zero <+ factors (zero * k)
[PROOFSTEP]
simp [zero_mul]
[GOAL]
case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+ factors (succ hn * k)
[PROOFSTEP]
apply sublist_of_subperm_of_sorted _ (factors_sorted _) (factors_sorted _)
[GOAL]
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn * k)
[PROOFSTEP]
simp [(perm_factors_mul (Nat.succ_ne_zero _) h).subperm_left]
[GOAL]
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn) ++ factors k
[PROOFSTEP]
exact (sublist_append_left _ _).subperm
[GOAL]
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ factors n <+ factors k
[PROOFSTEP]
obtain ⟨a, rfl⟩ := h
[GOAL]
case intro
n a : ℕ
h' : n * a ≠ 0
⊢ factors n <+ factors (n * a)
[PROOFSTEP]
exact factors_sublist_right (right_ne_zero_of_mul h')
[GOAL]
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
⊢ a ∣ b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inl
a : ℕ
ha : a ≠ 0
h : factors a <+~ factors 0
⊢ a ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case inr
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
hb : b > 0
⊢ a ∣ b
[PROOFSTEP]
rcases a with (_ | _ | a)
[GOAL]
case inr.zero
b : ℕ
hb : b > 0
ha : zero ≠ 0
h : factors zero <+~ factors b
⊢ zero ∣ b
[PROOFSTEP]
exact (ha rfl).elim
[GOAL]
case inr.succ.zero
b : ℕ
hb : b > 0
ha : succ zero ≠ 0
h : factors (succ zero) <+~ factors b
⊢ succ zero ∣ b
[PROOFSTEP]
exact
  one_dvd
    _
      --Porting note: previous proof
        --use (b.factors.diff a.succ.succ.factors).prod
[GOAL]
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ succ (succ a) ∣ b
[PROOFSTEP]
use(@List.diff _ instBEq b.factors a.succ.succ.factors).prod
[GOAL]
case h
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = succ (succ a) * prod (List.diff (factors b) (factors (succ (succ a))))
[PROOFSTEP]
nth_rw 1 [← Nat.prod_factors ha]
[GOAL]
case h
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = prod (factors (succ (succ a))) * prod (List.diff (factors b) (factors (succ (succ a))))
[PROOFSTEP]
rw [← List.prod_append, List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
  Nat.prod_factors hb.ne']
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∨ p ∈ factors b
[PROOFSTEP]
rw [mem_factors (mul_ne_zero ha hb), mem_factors ha, mem_factors hb, ← and_or_left]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
[PROOFSTEP]
simpa only [and_congr_right_iff] using Prime.dvd_mul
[GOAL]
a b : ℕ
hab : coprime a b
⊢ List.Disjoint (factors a) (factors b)
[PROOFSTEP]
intro q hqa hqb
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ False
[PROOFSTEP]
apply not_prime_one
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime 1
[PROOFSTEP]
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_factors hqa) (dvd_of_mem_factors hqb)]
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime q
[PROOFSTEP]
exact prime_of_mem_factors hqa
[GOAL]
a b : ℕ
hab : coprime a b
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rcases a.eq_zero_or_pos with (rfl | ha)
[GOAL]
case inl
b p : ℕ
hab : coprime 0 b
⊢ p ∈ factors (0 * b) ↔ p ∈ factors 0 ∪ factors b
[PROOFSTEP]
simp [(coprime_zero_left _).mp hab]
[GOAL]
case inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inr.inl
a p : ℕ
ha : a > 0
hab : coprime a 0
⊢ p ∈ factors (a * 0) ↔ p ∈ factors a ∪ factors 0
[PROOFSTEP]
simp [(coprime_zero_right _).mp hab]
[GOAL]
case inr.inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rw [mem_factors_mul ha.ne' hb.ne', List.mem_union_iff]
[GOAL]
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ factors 0
⊢ p ∈ factors (0 * b)
[PROOFSTEP]
simp at hpa
[GOAL]
case inr
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
apply (mem_factors_mul ha hb).2 (Or.inl hpa)
[GOAL]
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (b * a)
[PROOFSTEP]
exact mem_factors_mul_left hpb ha


[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
m n : ℕ
n_dvd : n ∣ m
n_nonzero : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases n_dvd with ⟨k, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
have : n ≠ 0 := by
  rintro rfl
  simp at n_nonzero
[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
k : ℕ
n_nonzero : ↑0 ≠ 0
⊢ False
[PROOFSTEP]
simp at n_nonzero
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ this.bot_lt, mul_comm n k, cast_mul, mul_div_cancel _ n_nonzero]
[GOAL]
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd)
[GOAL]
case inl
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n : ℕ
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n
[PROOFSTEP]
simp [zero_dvd_iff.mp hm]
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
replace hd : (d : α) ≠ 0
[GOAL]
case hd
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
rw [cast_div hm, cast_div hn, div_div_div_cancel_right _ hd]
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
exact hd
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
exact hd
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / zero) ≤ ↑m / ↑zero
[PROOFSTEP]
rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / succ n✝) ≤ ↑m / ↑(succ n✝)
[PROOFSTEP]
rw [le_div_iff, ← Nat.cast_mul, @Nat.cast_le]
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / succ n✝ * succ n✝ ≤ m
case succ α : Type u_1 inst✝ : LinearOrderedSemifield α m n✝ : ℕ ⊢ 0 < ↑(succ n✝)
[PROOFSTEP]
exact (Nat.div_mul_le_self m _)
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
[PROOFSTEP]
exact Nat.cast_pos.2 (Nat.succ_pos _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < 1 / (↑n + 1)
[PROOFSTEP]
rw [one_div]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹
[PROOFSTEP]
exact inv_pos_of_nat
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)
[PROOFSTEP]
refine' one_div_le_one_div_of_le _ _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1
case refine'_2 α : Type u_1 inst✝ : LinearOrderedSemifield α n m : ℕ h : n ≤ m ⊢ ↑n + 1 ≤ ↑m + 1
[PROOFSTEP]
exact Nat.cast_add_one_pos _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 1 / (↑m + 1) < 1 / (↑n + 1)
[PROOFSTEP]
refine' one_div_lt_one_div_of_lt _ _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 0 < ↑n + 1
case refine'_2 α : Type u_1 inst✝ : LinearOrderedSemifield α n m : ℕ h : n < m ⊢ ↑n + 1 < ↑m + 1
[PROOFSTEP]
exact Nat.cast_add_one_pos _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1
[PROOFSTEP]
simpa


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).fst = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑Nat.zero).fst = ↑Nat.zero
[PROOFSTEP]
simp [*]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
n_ih✝ : (↑n✝).fst = ↑n✝
⊢ (↑(Nat.succ n✝)).fst = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).snd = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑Nat.zero).snd = ↑Nat.zero
[PROOFSTEP]
simp [*]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
n_ih✝ : (↑n✝).snd = ↑n✝
⊢ (↑(Nat.succ n✝)).snd = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*]


[GOAL]
a b m n k : ℕ
S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S
[PROOFSTEP]
rintro rfl
[GOAL]
a b m n k : ℕ
⊢ 0 ∈ Set.univ ∧ ∀ (k : ℕ), k ∈ Set.univ → k + 1 ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
⊢ a < n / d ↔ d * a < n
[PROOFSTEP]
rcases d.eq_zero_or_pos with (rfl | hd0)
[GOAL]
case inl
a✝ b m n✝ k n a : ℕ
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n
[PROOFSTEP]
simp [zero_dvd_iff.mp hnd]
[GOAL]
case inr
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
[PROOFSTEP]
rw [← mul_lt_mul_left hd0, ← Nat.eq_mul_of_div_eq_right hnd rfl]
[GOAL]
a b m n✝ k n d : ℕ
⊢ d * (n / d) = n ↔ d * (n / d) = d * (n / d) + n % d
[PROOFSTEP]
rw [div_add_mod]
[GOAL]
a b m n✝ k n d : ℕ
⊢ d * (n / d) = d * (n / d) + n % d ↔ d ∣ n
[PROOFSTEP]
rw [self_eq_add_right, dvd_iff_mod_eq_zero]
  -- porting note: new lemma
[GOAL]
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y → x = y
[PROOFSTEP]
intro h
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ x = y
[PROOFSTEP]
rw [← mul_right_inj' hn]
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x = n * y
[PROOFSTEP]
apply Nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_left hy x)
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x / y = n
[PROOFSTEP]
rw [eq_comm, mul_comm, Nat.mul_div_assoc _ hy]
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n = x * (n / y)
[PROOFSTEP]
exact Nat.eq_mul_of_div_eq_right hx h
[GOAL]
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ x = y → n / x = n / y
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : x = y
⊢ n / x = n / y
[PROOFSTEP]
rw [h]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a < b
[PROOFSTEP]
rw [← mod_add_div a b, h, mul_zero, add_zero]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a % b < b
[PROOFSTEP]
exact mod_lt _ hb
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a < b
⊢ a / b = 0
[PROOFSTEP]
rw [← mul_right_inj' hb.ne', ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div, mod_eq_of_lt h, mul_zero, add_zero]
[GOAL]
a b m n✝ k n : ℕ
⊢ ¬2 ∣ bit1 n
[PROOFSTEP]
rw [bit1, Nat.dvd_add_right two_dvd_bit0, Nat.dvd_one]
  -- Porting note: was `cc`
[GOAL]
a b m n✝ k n : ℕ
⊢ ¬2 = 1
[PROOFSTEP]
decide
[GOAL]
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
⊢ k ∣ m - n
[PROOFSTEP]
cases' le_total n m with H H
[GOAL]
case inl
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n
[PROOFSTEP]
exact dvd_sub H h₁ h₂
[GOAL]
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr H]
[GOAL]
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0
[PROOFSTEP]
exact dvd_zero k
[GOAL]
a✝ b m n k a : ℕ
⊢ (a + 1) / 0 = a / 0 + if 0 ∣ a + 1 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
a b m n k : ℕ
⊢ (0 + 1) / 1 = 0 / 1 + if 1 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
a b✝ m n k b : ℕ
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
have hb2 : b + 2 > 1 := by simp
[GOAL]
a b✝ m n k b : ℕ
⊢ b + 2 > 1
[PROOFSTEP]
simp
[GOAL]
a b✝ m n k b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
simp [ne_of_gt hb2, div_eq_of_lt hb2]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (a + 1 + 1) / (b + 1) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
conv_rhs => rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
by_cases hb_eq_a : b = a + 1
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [hb_eq_a, le_refl]
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
by_cases hb_le_a1 : b ≤ a + 1
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hb_le_a : b ≤ a := le_of_lt_succ (lt_of_le_of_ne hb_le_a1 hb_eq_a)
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a1⟩
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a⟩
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1 := by
  rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b, add_comm (_ - _), add_assoc,
    tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
[PROOFSTEP]
rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b, add_comm (_ - _), add_assoc,
  tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have wf : a - b < a + 1 := lt_succ_of_le tsub_le_self
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [if_pos h₁, if_pos h₂, @add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a,
  have := wf
  succ_div (a - b),
  @add_tsub_add_eq_tsub_right]
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [dvd_iff, succ_eq_add_one, add_comm 1, add_assoc]
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hba : ¬b ≤ a := not_le_of_gt (lt_trans (lt_succ_self a) (lt_of_not_ge hb_le_a1))
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hb_dvd_a : ¬b + 1 ∣ a + 2 := fun h => hb_le_a1 (le_of_succ_le_succ (le_of_dvd (succ_pos _) h))
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [hba, hb_le_a1, hb_dvd_a]
[GOAL]
a✝ b✝ m n k a b : ℕ
hba : b ∣ a + 1
⊢ (a + 1) / b = a / b + 1
[PROOFSTEP]
rw [succ_div, if_pos hba]
[GOAL]
a✝ b✝ m n k a b : ℕ
hba : ¬b ∣ a + 1
⊢ (a + 1) / b = a / b
[PROOFSTEP]
rw [succ_div, if_neg hba, add_zero]
[GOAL]
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha : a = 0
⊢ b ∣ c / a
[PROOFSTEP]
simp [ha]
[GOAL]
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha✝ : ¬a = 0
ha : 0 < a
h1 : ∃ d, c = a * b * d
d : ℕ
hd : c = a * b * d
⊢ c = a * (b * d)
[PROOFSTEP]
simpa [mul_assoc] using hd
[GOAL]
a✝ b✝ m n k a b c x✝¹ x✝ : ℕ
dvd : x✝¹ ∣ 0
dvd2 : 0 ∣ x✝
⊢ x✝ / (0 / x✝¹) / x✝¹ = x✝ / 0
[PROOFSTEP]
simp
[GOAL]
a✝¹ b✝ m n k a✝ b c a x✝ : ℕ
dvd : 0 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / 0) / 0 = x✝ / (a + 1)
[PROOFSTEP]
simp at dvd
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
have a_split : a + 1 ≠ 0 := succ_ne_zero a
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
have c_split : c + 1 ≠ 0 := succ_ne_zero c
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
rcases dvd2 with ⟨k, rfl⟩
[GOAL]
case intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
dvd : c + 1 ∣ a + 1
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k : ℕ
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
rcases dvd with ⟨k2, pr⟩
[GOAL]
case intro.intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr
[GOAL]
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_zero : k2 = 0
⊢ False
[PROOFSTEP]
simp [k2_zero] at pr
[GOAL]
case intro.intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_nonzero : k2 ≠ 0
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr, Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split),
  Nat.mul_comm ((c + 1) * k2) k, ← Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
  Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]
[GOAL]
a b m n k : ℕ
h : a < b + n
⊢ n ∣ a → n ∣ b → a ≤ b
[PROOFSTEP]
rintro ⟨a, rfl⟩
  ⟨b, rfl⟩
      -- porting note: Needed to give an explicit argument to `mul_add_one`
[GOAL]
case intro.intro
m n k a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b
[PROOFSTEP]
rw [← mul_add_one n] at h
[GOAL]
case intro.intro
m n k a b : ℕ
h : n * a < n * (b + 1)
⊢ n * a ≤ n * b
[PROOFSTEP]
exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % n / n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
a b m✝ n k m : ℕ
⊢ m % zero / zero = 0
[PROOFSTEP]
exact (m % 0).div_zero
[GOAL]
case succ
a b m✝ n k m n✝ : ℕ
⊢ m % succ n✝ / succ n✝ = 0
[PROOFSTEP]
case succ n => exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % succ n / succ n = 0
[PROOFSTEP]
case succ n => exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % succ n / succ n = 0
[PROOFSTEP]
exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a✝ b m n✝ k n a : ℕ
ha : 0 < a
⊢ (∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n
[PROOFSTEP]
refine'
  ⟨fun ⟨k, hk1, hk2⟩ => not_dvd_of_between_consec_multiples hk1 hk2, fun han =>
    ⟨n / a, ⟨lt_of_le_of_ne (mul_div_le n a) _, lt_mul_div_succ _ ha⟩⟩⟩
[GOAL]
a✝ b m n✝ k n a : ℕ
ha : 0 < a
han : ¬a ∣ n
⊢ a * (n / a) ≠ n
[PROOFSTEP]
exact mt (Dvd.intro (n / a)) han
[GOAL]
a b m✝ n✝¹ k m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n
[PROOFSTEP]
rw [h]
[GOAL]
a b m✝ n✝¹ k m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝
[PROOFSTEP]
rw [h]
[GOAL]
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ a / d < b / d
[PROOFSTEP]
rw [Nat.lt_div_iff_mul_lt hdb]
[GOAL]
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b
[PROOFSTEP]
exact lt_of_le_of_lt (mul_div_le a d) h