[GOAL]
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p
[PROOFSTEP]
obtain ⟨n, hn⟩ := hm
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p
[PROOFSTEP]
have := pp.isUnit_or_isUnit hn
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p
[PROOFSTEP]
rw [Nat.isUnit_iff, Nat.isUnit_iff] at this
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p
[PROOFSTEP]
apply Or.imp_right _ this
[GOAL]
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p
[PROOFSTEP]
rw [hn, mul_one]
[GOAL]
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
[PROOFSTEP]
refine'
  ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => _⟩
    -- Porting note: needed to make ℕ explicit
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
[PROOFSTEP]
have h1 := (@one_lt_two ℕ ..).trans_le h.1
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
[PROOFSTEP]
refine' ⟨mt Nat.isUnit_iff.mp h1.ne', fun a b hab => _⟩
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
simp only [Nat.isUnit_iff]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1
[PROOFSTEP]
apply Or.imp_right _ (h.2 a _)
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1
[PROOFSTEP]
rintro rfl
[GOAL]
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1
[PROOFSTEP]
rw [← mul_right_inj' (pos_of_gt h1).ne', ← hab, mul_one]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p
[PROOFSTEP]
rw [hab]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1
[PROOFSTEP]
rcases m with (_ | _ | m)
[GOAL]
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
[PROOFSTEP]
rw [eq_zero_of_zero_dvd d] at p2
[GOAL]
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
[PROOFSTEP]
revert p2
[GOAL]
case zero
p : ℕ
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ 2 ≤ 0 → zero = 1
[PROOFSTEP]
decide
[GOAL]
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ succ zero → succ zero < p → ¬succ zero ∣ p
l : succ zero < p
d : succ zero ∣ p
⊢ succ zero = 1
[PROOFSTEP]
rfl
[GOAL]
case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ succ (succ m) → succ (succ m) < p → ¬succ (succ m) ∣ p
l : succ (succ m) < p
d : succ (succ m) ∣ p
⊢ succ (succ m) = 1
[PROOFSTEP]
exact (h le_add_self l).elim d
[GOAL]
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
⊢ False
[PROOFSTEP]
cases' le_total m k with mk km
[GOAL]
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False
[PROOFSTEP]
exact this mk m2 e
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False
[PROOFSTEP]
rw [mul_comm] at e
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False
[PROOFSTEP]
refine' this km (lt_of_mul_lt_mul_right _ (zero_le m)) e
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m
[PROOFSTEP]
rwa [one_mul, ← e]
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
⊢ Prime n
[PROOFSTEP]
refine' prime_def_lt.mpr ⟨h1, fun m mlt mdvd => _⟩
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
[PROOFSTEP]
have hm : m ≠ 0 := by
  rintro rfl
  rw [zero_dvd_iff] at mdvd
  exact mlt.ne' mdvd
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
[PROOFSTEP]
rw [zero_dvd_iff] at mdvd
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : n = 0
⊢ False
[PROOFSTEP]
exact mlt.ne' mdvd
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1
[PROOFSTEP]
exact (h m mlt hm).symm.eq_one_of_dvd mdvd
[GOAL]
⊢ Prime 2
[PROOFSTEP]
decide
[GOAL]
⊢ Prime 3
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p
[PROOFSTEP]
by_contra' h
[GOAL]
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
[PROOFSTEP]
revert h_two h_three hp
[GOAL]
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False
[PROOFSTEP]
match p with
| 0 => decide
| 1 => decide
| 2 => decide
| 3 => decide
| 4 => decide
| n + 5 => exact (h.not_le le_add_self).elim
[GOAL]
p : ℕ
h : 0 < 5
⊢ Prime 0 → 0 ≠ 2 → 0 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 1 < 5
⊢ Prime 1 → 1 ≠ 2 → 1 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 2 < 5
⊢ Prime 2 → 2 ≠ 2 → 2 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 3 < 5
⊢ Prime 3 → 3 ≠ 2 → 3 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 4 < 5
⊢ Prime 4 → 4 ≠ 2 → 4 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p n : ℕ
h : n + 5 < 5
⊢ Prime (n + 5) → n + 5 ≠ 2 → n + 5 ≠ 3 → False
[PROOFSTEP]
exact (h.not_le le_add_self).elim
[GOAL]
a b : ℕ
a1 : 1 < a
b1 : 1 < b
h : Prime (a * b)
⊢ a * 1 = a * b
[PROOFSTEP]
simpa using (dvd_prime_two_le h a1).1 (dvd_mul_right _ _)
[GOAL]
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime n
[PROOFSTEP]
rw [← h]
[GOAL]
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime (a * b)
[PROOFSTEP]
exact not_prime_mul h₁ h₂
[GOAL]
a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
[PROOFSTEP]
simp only [iff_self_iff, irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a
[PROOFSTEP]
refine'
  ⟨_, by
    rintro rfl
    rfl⟩
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p
[PROOFSTEP]
rfl
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
[PROOFSTEP]
rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
[GOAL]
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a
[PROOFSTEP]
exact mul_one _
[GOAL]
case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1
[PROOFSTEP]
exact (a1 rfl).elim
[GOAL]
n k : ℕ
h : ¬n < k * k
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n (minFacAux n x✝)
[PROOFSTEP]
rw [minFacAux]
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
by_cases h : n < k * k
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n n
[PROOFSTEP]
have pp : Prime n := prime_def_le_sqrt.2 ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ Nat.minFacProp n n
[PROOFSTEP]
exact ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
have k2 : 2 ≤ k := by
  subst e
  apply Nat.le_add_left
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
[PROOFSTEP]
subst e
[GOAL]
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
by_cases dk : k ∣ n
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [dk]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [dk]
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n x✝
[PROOFSTEP]
exact ⟨k2, dk, a⟩
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (minFacAux n (x✝ + 2))
[PROOFSTEP]
refine'
  have := minFac_lemma n k h
  minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [e, left_distrib]) fun m m2 d => _
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3
[PROOFSTEP]
simp [e, left_distrib]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m
[PROOFSTEP]
cases' Nat.eq_or_lt_of_le (a m m2 d) with me ml
[GOAL]
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
me : x✝ = m
⊢ k + 2 ≤ m
[PROOFSTEP]
subst me
[GOAL]
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝
[PROOFSTEP]
contradiction
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m
[PROOFSTEP]
apply (Nat.eq_or_lt_of_le ml).resolve_left
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬succ x✝ = m
[PROOFSTEP]
intro me
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
[PROOFSTEP]
rw [← me, e] at d
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
[PROOFSTEP]
have d' : 2 * (i + 2) ∣ n := d
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
⊢ False
[PROOFSTEP]
have := a _ le_rfl (dvd_of_mul_right_dvd d')
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False
[PROOFSTEP]
rw [e] at this
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False
[PROOFSTEP]
exact absurd this (by contradiction)
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
n1 : n ≠ 1
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
by_cases n0 : n = 0
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
simp [n0, minFacProp, GE.ge]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
have n2 : 2 ≤ n := by
  revert n0 n1
  rcases n with (_ | _ | _) <;> simp [succ_le_succ]
[GOAL]
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n
[PROOFSTEP]
revert n0 n1
[GOAL]
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n
[PROOFSTEP]
rcases n with (_ | _ | _)
[GOAL]
case zero
⊢ zero ≠ 1 → ¬zero = 0 → 2 ≤ zero
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case succ.zero
⊢ succ zero ≠ 1 → ¬succ zero = 0 → 2 ≤ succ zero
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case succ.succ
n✝ : ℕ
⊢ succ (succ n✝) ≠ 1 → ¬succ (succ n✝) = 0 → 2 ≤ succ (succ n✝)
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
simp [minFac_eq]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
by_cases d2 : 2 ∣ n
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
simp [d2]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
simp [d2]
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2
[PROOFSTEP]
exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (minFacAux n 3)
[PROOFSTEP]
refine' minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt _ d2)
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n
[PROOFSTEP]
exact fun e => e.symm ▸ d
[GOAL]
n : ℕ
n1 : n = 1
⊢ minFac n ∣ n
[PROOFSTEP]
simp [n1]
[GOAL]
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m
[PROOFSTEP]
by_cases n1 : n = 1 <;> [exact fun m2 _ => n1.symm ▸ le_trans (by decide) m2; apply (minFac_has_prop n1).2.2]
[GOAL]
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m
[PROOFSTEP]
by_cases n1 : n = 1
[GOAL]
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → minFac n ≤ m✝
[PROOFSTEP]
exact fun m2 _ => n1.symm ▸ le_trans (by decide) m2
[GOAL]
n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2
[PROOFSTEP]
decide
[GOAL]
case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → minFac n ≤ m✝
[PROOFSTEP]
apply (minFac_has_prop n1).2.2
[GOAL]
n : ℕ
⊢ 0 < minFac n
[PROOFSTEP]
by_cases n1 : n = 1 <;> [exact n1.symm ▸ (by decide); exact (minFac_prime n1).pos]
[GOAL]
n : ℕ
⊢ 0 < minFac n
[PROOFSTEP]
by_cases n1 : n = 1
[GOAL]
case pos
n : ℕ
n1 : n = 1
⊢ 0 < minFac n
[PROOFSTEP]
exact n1.symm ▸ (by decide)
[GOAL]
n : ℕ
n1 : n = 1
⊢ 0 < minFac 1
[PROOFSTEP]
decide
[GOAL]
case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < minFac n
[PROOFSTEP]
exact (minFac_prime n1).pos
[GOAL]
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : Prime p
d : p ∣ n
⊢ n = 1 → m ≤ p
[PROOFSTEP]
rintro rfl
[GOAL]
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
[PROOFSTEP]
cases pp.not_dvd_one d
[GOAL]
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : 1 < p
d : p ∣ n
⊢ n = 1 → m ≤ p
[PROOFSTEP]
rintro rfl
[GOAL]
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
[PROOFSTEP]
cases not_le_of_lt pp (le_of_dvd (by decide) d)
[GOAL]
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < n
[PROOFSTEP]
rw [h0, mul_zero]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n * 1
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [mul_one] at h1
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, or_false_iff, not_le] at np
[GOAL]
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
conv_rhs =>
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n
case a n : ℕ pos : 0 < n np : ¬Prime n x : ℕ hx : n = minFac n * (x + 2) | minFac n
[PROOFSTEP]
rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ minFac n * (x + 2) / minFac n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ x + 2
[PROOFSTEP]
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ n = (x + 2) * minFac n
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
n : ℕ
⊢ minFac n = 1 ↔ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ minFac n = 1 → n = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : minFac n = 1
⊢ n = 1
[PROOFSTEP]
by_contra hn
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
⊢ False
[PROOFSTEP]
have := minFac_prime hn
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime (minFac n)
⊢ False
[PROOFSTEP]
rw [h] at this
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime 1
⊢ False
[PROOFSTEP]
exact not_prime_one this
[GOAL]
case mpr
n : ℕ
⊢ n = 1 → minFac n = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
⊢ minFac 1 = 1
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ minFac n = 2 ↔ 2 ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ minFac n = 2 → 2 ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : minFac n = 2
⊢ 2 ∣ n
[PROOFSTEP]
rw [← h]
[GOAL]
case mp
n : ℕ
h : minFac n = 2
⊢ minFac n ∣ n
[PROOFSTEP]
exact minFac_dvd n
[GOAL]
case mpr
n : ℕ
⊢ 2 ∣ n → minFac n = 2
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
⊢ minFac n = 2
[PROOFSTEP]
have ub := minFac_le_of_dvd (le_refl 2) h
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
⊢ minFac n = 2
[PROOFSTEP]
have lb := minFac_pos n
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
⊢ minFac n = 2
[PROOFSTEP]
refine ub.eq_or_lt.resolve_right fun h' => ?_
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
⊢ False
[PROOFSTEP]
have := le_antisymm (Nat.succ_le_of_lt lb) (lt_succ_iff.mp h')
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : succ 0 = minFac n
⊢ False
[PROOFSTEP]
rw [eq_comm, Nat.minFac_eq_one_iff] at this
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : n = 1
⊢ False
[PROOFSTEP]
subst this
[GOAL]
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False
[PROOFSTEP]
exact not_lt_of_le (le_of_dvd zero_lt_one h) one_lt_two
[GOAL]
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 1
[GOAL]
case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b
[PROOFSTEP]
apply one_dvd
[GOAL]
case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b
[PROOFSTEP]
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
[GOAL]
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b
[PROOFSTEP]
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)
[GOAL]
⊢ ¬BddAbove {p | Prime p}
[PROOFSTEP]
rw [not_bddAbove_iff]
[GOAL]
⊢ ∀ (x : ℕ), ∃ y, y ∈ {p | Prime p} ∧ x < y
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
[PROOFSTEP]
obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
[GOAL]
case intro.intro
n p : ℕ
hi : succ n ≤ p
hp : Prime p
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
[PROOFSTEP]
exact ⟨p, hp, hi⟩
[GOAL]
p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬2 = 1
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2
[PROOFSTEP]
rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
[GOAL]
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n
[PROOFSTEP]
rw [hn, Nat.add_sub_cancel, two_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
⊢ p % 2 = 1 ↔ p ≠ 2
[PROOFSTEP]
refine' ⟨fun h hf => _, (Nat.Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left⟩
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
h : p % 2 = 1
hf : p = 2
⊢ False
[PROOFSTEP]
rw [hf] at h
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
h : 2 % 2 = 1
hf : p = 2
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ coprime m n
[PROOFSTEP]
rw [coprime_iff_gcd_eq_one]
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ gcd m n = 1
[PROOFSTEP]
by_contra g2
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
⊢ False
[PROOFSTEP]
obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
[GOAL]
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ False
[PROOFSTEP]
apply H p hp
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ p ∣ m
[PROOFSTEP]
apply dvd_trans hpdvd
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ p ∣ n
[PROOFSTEP]
apply dvd_trans hpdvd
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ m
[PROOFSTEP]
exact gcd_dvd_left _ _
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_right _ _
[GOAL]
k : ℕ
⊢ k + 2 ≠ 1
[PROOFSTEP]
apply Nat.ne_of_gt
[GOAL]
case h
k : ℕ
⊢ 1 < k + 2
[PROOFSTEP]
apply Nat.succ_lt_succ
[GOAL]
case h.a
k : ℕ
⊢ 0 < k + 1
[PROOFSTEP]
apply Nat.zero_lt_succ
[GOAL]
p n : ℕ
pp : Prime p
co : coprime p n
d : p ∣ n
⊢ p ∣ n * 1
[PROOFSTEP]
simp [d]
[GOAL]
m n : ℕ
⊢ ¬coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m n : ℕ
⊢ ¬coprime m n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ
h : ¬coprime m n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
exact
  ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
    (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
[GOAL]
case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬coprime m n
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬coprime m n
[PROOFSTEP]
cases' h with p hp
[GOAL]
case mpr.intro
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬coprime m n
[PROOFSTEP]
apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2
[GOAL]
p m n : ℕ
pp : Prime p
Hm : ¬p ∣ m
Hn : ¬p ∣ n
⊢ ¬(p ∣ m ∨ p ∣ n)
[PROOFSTEP]
simp [Hm, Hn]
[GOAL]
p m n : ℕ
pp : Prime p
h : p ∣ m ^ n
⊢ p ∣ m
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
p m n : ℕ
pp : Prime p
h✝ : p ∣ m ^ n
h : p ∣ m ^ zero
⊢ p ∣ m
[PROOFSTEP]
exact pp.not_dvd_one.elim h
[GOAL]
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ succ n
⊢ p ∣ m
[PROOFSTEP]
rw [pow_succ] at h
[GOAL]
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ n * m
⊢ p ∣ m
[PROOFSTEP]
exact (pp.dvd_mul.1 h).elim IH id
[GOAL]
p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [h.1, h.2, pow_one]⟩
[GOAL]
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p
[PROOFSTEP]
rw [h.1, h.2, pow_one]
[GOAL]
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1
[PROOFSTEP]
rw [← h] at hp
[GOAL]
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
[PROOFSTEP]
rw [← h, hp.eq_one_of_pow, eq_self_iff_true, and_true_iff, pow_one]
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
rcases eq_or_ne n 1 with (rfl | hn)
[GOAL]
case inl
k : ℕ
hk : k ≠ 0
⊢ minFac (1 ^ k) = minFac 1
[PROOFSTEP]
simp
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac n ≤ minFac (n ^ k)
[PROOFSTEP]
apply minFac_le_of_dvd (minFac_prime hnk).two_le ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))
[GOAL]
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ minFac (p ^ k) = p
[PROOFSTEP]
rw [Nat.pow_minFac hk, hp.minFac_eq]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
⊢ x * y = p ^ 2 ↔ x = p ∧ y = p
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ x = p ∧ y = p
[PROOFSTEP]
have pdvdxy : p ∣ x * y := by rw [h];
  simp [sq]
    -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ x * y
[PROOFSTEP]
rw [h]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ p ^ 2
[PROOFSTEP]
simp [sq]
  -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
⊢ x = p ∧ y = p
[PROOFSTEP]
suffices ∀ x' y' : ℕ, x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p by
  obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]] <;> [skip; rw [mul_comm] at h pdvdxy ] <;>
      apply this <;>
    assumption
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]] <;> [skip; rw [mul_comm] at h pdvdxy ]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
skip
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x = p ∧ y = p
[PROOFSTEP]
rw [And.comm]
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
skip
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
[PROOFSTEP]
rw [mul_comm] at h pdvdxy
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
apply this
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
[PROOFSTEP]
apply this
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ y ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x * y = p ^ 2
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ p ∣ x
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y * x = p ^ 2
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ p ∣ y
[PROOFSTEP]
assumption
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
⊢ ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
[PROOFSTEP]
rintro x y hx hy h ⟨a, ha⟩
[GOAL]
case intro
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ x = p ∧ y = p
[PROOFSTEP]
have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h ⟩
[GOAL]
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y
[PROOFSTEP]
rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h
[GOAL]
case intro
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain ha1 | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
ha1 : a = 1
⊢ x = p ∧ y = p
[PROOFSTEP]
subst ha1
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p * 1
this : 1 ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
rw [mul_one] at ha
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p
this : 1 ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
subst ha
[GOAL]
case intro.inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
h : x * y = x ^ 2
this : 1 ∣ x
⊢ x = x ∧ y = x
[PROOFSTEP]
simp only [sq, mul_right_inj' hp.ne_zero] at h
[GOAL]
case intro.inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
this : 1 ∣ x
h : y = x
⊢ x = x ∧ y = x
[PROOFSTEP]
subst h
[GOAL]
case intro.inl
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy hx : y ≠ 1
hp : Prime y
h : x * y✝ = y ^ 2
pdvdxy : y ∣ x * y✝
this : 1 ∣ y
⊢ y = y ∧ y = y
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
case intro.inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p
[PROOFSTEP]
refine' (hy ?_).elim
[GOAL]
case intro.inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ y = 1
[PROOFSTEP]
subst hap
[GOAL]
case intro.inr
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x✝ * y✝ = a ^ 2
pdvdxy : a ∣ x✝ * y✝
h : x * y = a ^ 2
ha : x = a * a
this : a ∣ a
⊢ y = 1
[PROOFSTEP]
subst ha
[GOAL]
case intro.inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : a * a * y = a ^ 2
⊢ y = 1
[PROOFSTEP]
rw [sq, Nat.mul_right_eq_self_iff (Nat.mul_pos hp.pos hp.pos : 0 < a * a)] at h
[GOAL]
case intro.inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : y = 1
⊢ y = 1
[PROOFSTEP]
exact h
[GOAL]
n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1
[PROOFSTEP]
rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
[GOAL]
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
[PROOFSTEP]
exact
  ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
    (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
[GOAL]
n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
pp : Prime p
i : ℕ
⊢ coprime p i ∨ p ∣ i
[PROOFSTEP]
rw [pp.dvd_iff_not_coprime]
[GOAL]
p : ℕ
pp : Prime p
i : ℕ
⊢ coprime p i ∨ ¬coprime p i
[PROOFSTEP]
apply em
[GOAL]
p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k
[PROOFSTEP]
simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]
[GOAL]
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)
[PROOFSTEP]
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
[GOAL]
case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)
[PROOFSTEP]
congr
[GOAL]
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1
[PROOFSTEP]
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))
[GOAL]
⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0
[PROOFSTEP]
simpa using Exists.intro 2 Nat.prime_two
[GOAL]
⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1
[PROOFSTEP]
simp [Nat.not_prime_one]
[GOAL]
n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
let a := n + 2
[GOAL]
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
let ha : a ≠ 1 := Nat.succ_succ_ne_one n
[GOAL]
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
simp only [true_iff_iff, Ne.def, not_false_iff, ha]
[GOAL]
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩
[GOAL]
n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n
[PROOFSTEP]
simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd : p ^ (k + l) * p ∣ m * n :=
  by
  let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
  rwa [pow_succ'] at hpmn'
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n
[PROOFSTEP]
let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p ^ succ (k + l) ∣ m * n := hpmn
⊢ p ^ (k + l) * p ∣ m * n
[PROOFSTEP]
rwa [pow_succ'] at hpmn'
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ∣ m * n / (p ^ k * p ^ l)
[PROOFSTEP]
simpa [pow_add] using hpd2
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)
[PROOFSTEP]
simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l := (Prime.dvd_mul p_prime).1 hpd4
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ', _root_.pow_succ']
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
rwa [_root_.pow_succ', _root_.pow_succ']
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ k * p ∣ m ∨ p ^ l * p ∣ n
[PROOFSTEP]
exact
  hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h) fun h : p ∣ n / p ^ l =>
    Or.inr <| mul_dvd_of_dvd_div hpn h
[GOAL]
p : ℕ
hp : Prime p
a b : ℤ
h : ↑p ∣ a * b
⊢ ↑p ∣ a ∨ ↑p ∣ b
[PROOFSTEP]
rw [← Int.dvd_natAbs, Int.coe_nat_dvd, Int.natAbs_mul, hp.dvd_mul] at h
[GOAL]
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ Int.natAbs a ∨ p ∣ Int.natAbs b
⊢ ↑p ∣ a ∨ ↑p ∣ b
[PROOFSTEP]
rwa [← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
[GOAL]
p : ℕ
hp : _root_.Prime ↑p
h : p = 1
⊢ False
[PROOFSTEP]
simp [h, not_prime_one] at hp
[GOAL]
p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
simpa only [Int.coe_nat_dvd, (Int.ofNat_mul _ _).symm] using hp.2.2 a b


[GOAL]
x y : ℝ≥0
⊢ 0 ^ 2 = x ↔ x = 0
[PROOFSTEP]
rw [eq_comm, sq, zero_mul]
[GOAL]
x✝ y x : ℝ≥0
⊢ ↑sqrt x * ↑sqrt x = x
[PROOFSTEP]
rw [← sq, sq_sqrt]
[GOAL]
x✝ y x : ℝ≥0
⊢ ↑sqrt (x * x) = x
[PROOFSTEP]
rw [← sq, sqrt_sq x]
[GOAL]
x✝ y✝ x y : ℝ≥0
⊢ ↑sqrt (x * y) = ↑sqrt x * ↑sqrt y
[PROOFSTEP]
rw [sqrt_eq_iff_sq_eq, mul_pow, sq_sqrt, sq_sqrt]
[GOAL]
x y : ℝ≥0
⊢ 0 < ↑sqrt x ↔ 0 < x
[PROOFSTEP]
simp [pos_iff_ne_zero]
[GOAL]
f : CauSeq ℚ abs
⊢ 0 ≤ sqrtAux f 0
[PROOFSTEP]
rw [sqrtAux, Rat.mkRat_eq, Rat.divInt_eq_div]
[GOAL]
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num)) / ↑↑(Nat.sqrt (↑f 0).den)
[PROOFSTEP]
apply div_nonneg
[GOAL]
case ha
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num))
[PROOFSTEP]
exact Int.cast_nonneg.2 (Int.ofNat_nonneg _)
[GOAL]
case hb
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (↑f 0).den)
[PROOFSTEP]
exact Int.cast_nonneg.2 (Int.ofNat_nonneg _)
[GOAL]
x✝ y : ℝ
x : ℝ≥0
⊢ ↑(↑NNReal.sqrt x) = sqrt ↑x
[PROOFSTEP]
rw [Real.sqrt, Real.toNNReal_coe]
[GOAL]
x y : ℝ
h : x ≤ 0
⊢ sqrt x = 0
[PROOFSTEP]
simp [sqrt, Real.toNNReal_eq_zero.2 h]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
[GOAL]
x y : ℝ
⊢ sqrt x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : ℝ
⊢ sqrt x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
x : ℝ
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
cases' le_or_lt 0 x with hle hlt
[GOAL]
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
[GOAL]
case mp.inr
x : ℝ
hlt : x < 0
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
[GOAL]
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → sqrt x = y
[PROOFSTEP]
rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
[GOAL]
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ sqrt (y * y) = y
case mpr.inr.intro x : ℝ hx : x < 0 ⊢ sqrt x = 0
[PROOFSTEP]
exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : sqrt x = y
⊢ y * y = x
[PROOFSTEP]
rw [← h, mul_self_sqrt hx]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : y * y = x
⊢ sqrt x = y
[PROOFSTEP]
rw [← h, sqrt_mul_self hy]
[GOAL]
x y : ℝ
h : 0 < y
⊢ sqrt x = y ↔ y * y = x
[PROOFSTEP]
simp [sqrt_eq_cases, h.ne', h.le]
[GOAL]
x y : ℝ
⊢ 1 * 1 = x ↔ x = 1
[PROOFSTEP]
rw [eq_comm, mul_one]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x ^ 2 = x
[PROOFSTEP]
rw [sq, mul_self_sqrt h]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt (x ^ 2) = x
[PROOFSTEP]
rw [sq, sqrt_mul_self h]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x = y ↔ y ^ 2 = x
[PROOFSTEP]
rw [sq, sqrt_eq_iff_mul_self_eq hx hy]
[GOAL]
x✝ y x : ℝ
⊢ sqrt (x * x) = |x|
[PROOFSTEP]
rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]
[GOAL]
x✝ y x : ℝ
⊢ sqrt (x ^ 2) = |x|
[PROOFSTEP]
rw [sq, sqrt_mul_self_eq_abs]
[GOAL]
x y : ℝ
⊢ sqrt 0 = 0
[PROOFSTEP]
simp [sqrt]
[GOAL]
x y : ℝ
⊢ sqrt 1 = 1
[PROOFSTEP]
simp [sqrt]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt x ≤ sqrt y ↔ x ≤ y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt_iff, Real.toNNReal_le_toNNReal_iff hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ sqrt x < sqrt y ↔ x < y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt_iff, toNNReal_lt_toNNReal_iff hy]
[GOAL]
x y : ℝ
h : x ≤ y
⊢ sqrt x ≤ sqrt y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt_iff]
[GOAL]
x y : ℝ
h : x ≤ y
⊢ toNNReal x ≤ toNNReal y
[PROOFSTEP]
exact toNNReal_le_toNNReal h
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt x ≤ y ↔ x ≤ y ^ 2
[PROOFSTEP]
rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff, sq, ← Real.toNNReal_mul hy,
  Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
[GOAL]
x y : ℝ
⊢ sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
[PROOFSTEP]
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
[GOAL]
x y : ℝ
⊢ 0 ≤ y → (sqrt x ≤ y ↔ x ≤ y ^ 2)
[PROOFSTEP]
exact sqrt_le_left
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x < y ↔ x < y ^ 2
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ sqrt x < y ↔ x < y ^ 2
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]
[GOAL]
x y : ℝ
h : x ^ 2 ≤ y
⊢ |x| ≤ sqrt y
[PROOFSTEP]
rw [← sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
h : x ^ 2 ≤ y
⊢ sqrt (x ^ 2) ≤ sqrt y
[PROOFSTEP]
exact sqrt_le_sqrt h
[GOAL]
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y ↔ -sqrt y ≤ x ∧ x ≤ sqrt y
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -sqrt y ≤ x ∧ x ≤ sqrt y
[PROOFSTEP]
simpa only [abs_le] using abs_le_sqrt
[GOAL]
case mpr
x y : ℝ
h : 0 ≤ y
⊢ -sqrt y ≤ x ∧ x ≤ sqrt y → x ^ 2 ≤ y
[PROOFSTEP]
rw [← abs_le, ← sq_abs]
[GOAL]
case mpr
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ sqrt y → |x| ^ 2 ≤ y
[PROOFSTEP]
exact (le_sqrt (abs_nonneg x) h).mp
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x = sqrt y ↔ x = y
[PROOFSTEP]
simp [le_antisymm_iff, hx, hy]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x = 0 ↔ x = 0
[PROOFSTEP]
simpa using sqrt_inj h le_rfl
[GOAL]
x y : ℝ
⊢ sqrt x = 0 ↔ x ≤ 0
[PROOFSTEP]
rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
rw [not_iff_not, sqrt_eq_zero h]
[GOAL]
x y : ℝ
⊢ sqrt x ≠ 0 ↔ 0 < x
[PROOFSTEP]
rw [← not_le, not_iff_not, sqrt_eq_zero']
[GOAL]
x y : ℝ
⊢ sqrt x ≤ 0 ↔ sqrt x = 0
[PROOFSTEP]
simp [le_antisymm_iff, sqrt_nonneg]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ sqrt (x * y) = sqrt x * sqrt y
[PROOFSTEP]
simp_rw [sqrt, ← NNReal.coe_mul, NNReal.coe_eq, Real.toNNReal_mul hx, NNReal.sqrt_mul]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt (x * y) = sqrt x * sqrt y
[PROOFSTEP]
rw [mul_comm, sqrt_mul hy, mul_comm]
[GOAL]
x : ℝ
⊢ sqrt x⁻¹ = (sqrt x)⁻¹
[PROOFSTEP]
rw [sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, sqrt]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ sqrt (x / y) = sqrt x / sqrt y
[PROOFSTEP]
rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt (x / y) = sqrt x / sqrt y
[PROOFSTEP]
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
[GOAL]
x : ℝ
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
cases' le_or_lt x 0 with h h
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
rw [sqrt_eq_zero'.mpr h, div_zero]
[GOAL]
case inr
x : ℝ
h : 0 < x
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le]
[GOAL]
x : ℝ
⊢ sqrt x / x = 1 / sqrt x
[PROOFSTEP]
rw [← div_sqrt, one_div_div, div_sqrt]
[GOAL]
x : ℝ
⊢ sqrt x / x = (sqrt x)⁻¹
[PROOFSTEP]
rw [sqrt_div_self', one_div]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ x < sqrt y ↔ x ^ 2 < y
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]
[GOAL]
x y : ℝ
⊢ x ^ 2 < y ↔ -sqrt y < x ∧ x < sqrt y
[PROOFSTEP]
rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]
[GOAL]
x y : ℝ
h : sqrt x < y
⊢ x < y ^ 2
[PROOFSTEP]
have hy := x.sqrt_nonneg.trans_lt h
[GOAL]
x y : ℝ
h : sqrt x < y
hy : 0 < y
⊢ x < y ^ 2
[PROOFSTEP]
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]
[GOAL]
a : ℕ
⊢ ↑(Nat.sqrt a) ≤ sqrt ↑a
[PROOFSTEP]
rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
[GOAL]
a : ℕ
⊢ ↑(Nat.sqrt a) ^ 2 ≤ ↑a
[PROOFSTEP]
norm_cast
[GOAL]
a : ℕ
⊢ Nat.sqrt a ^ 2 ≤ a
[PROOFSTEP]
exact Nat.sqrt_le' a
[GOAL]
a : ℕ
⊢ sqrt ↑a ≤ ↑(Nat.sqrt a) + 1
[PROOFSTEP]
rw [Real.sqrt_le_iff]
[GOAL]
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1 ∧ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
[PROOFSTEP]
constructor
[GOAL]
case left
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1
[PROOFSTEP]
norm_cast
[GOAL]
case left
a : ℕ
⊢ 0 ≤ Nat.sqrt a + 1
[PROOFSTEP]
apply zero_le
[GOAL]
case right
a : ℕ
⊢ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
case right
a : ℕ
⊢ a ≤ (Nat.sqrt a + 1) ^ 2
[PROOFSTEP]
exact le_of_lt (Nat.lt_succ_sqrt' a)
[GOAL]
r : ℝ
⊢ 0 ≤ r ↔ ∃ s, r = star s * s
[PROOFSTEP]
refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩
[GOAL]
r : ℝ
⊢ (∃ s, r = star s * s) → 0 ≤ r
[PROOFSTEP]
rintro ⟨s, rfl⟩
[GOAL]
case intro
s : ℝ
⊢ 0 ≤ star s * s
[PROOFSTEP]
exact mul_self_nonneg s


[GOAL]
x : ℝ
h : 0 < x
⊢ sin x < x
[PROOFSTEP]
cases' lt_or_le 1 x with h' h'
[GOAL]
case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x
[PROOFSTEP]
exact (sin_le_one x).trans_lt h'
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x
[PROOFSTEP]
have hx : |x| = x := abs_of_nonneg h.le
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ sin x < x
[PROOFSTEP]
have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1
[PROOFSTEP]
rwa [hx]
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x - (x - x ^ 3 / 6) ≤ |x| ^ 4 * (5 / 96)
⊢ sin x < x
[PROOFSTEP]
rw [sub_le_iff_le_add', hx] at this
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x
[PROOFSTEP]
apply this.trans_lt
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x
[PROOFSTEP]
rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹
[PROOFSTEP]
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 5 / 96 < 6⁻¹
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 0 ≤ 5 / 96
[PROOFSTEP]
norm_num
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3
[PROOFSTEP]
apply pow_le_pow_of_le_one h.le h'
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
have hx : |x| = x := abs_of_nonneg h.le
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1
[PROOFSTEP]
rwa [hx]
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(|x| ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
rw [le_sub_iff_add_le, hx] at this
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
refine' lt_of_lt_of_le _ this
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
[PROOFSTEP]
have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by ring
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
[PROOFSTEP]
ring
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
[PROOFSTEP]
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 12⁻¹
[PROOFSTEP]
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 5 / 96 < 12⁻¹
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 0 ≤ 5 / 96
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 ≤ x ^ 3
[PROOFSTEP]
apply pow_le_pow_of_le_one h.le h'
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 3 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun y => tan y - y) (↑1 / cos x ^ 2 - 1) x
[PROOFSTEP]
simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
⊢ x < tan x
[PROOFSTEP]
let U := Ico 0 (π / 2)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
⊢ x < tan x
[PROOFSTEP]
have intU : interior U = Ioo 0 (π / 2) := interior_Ico
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
⊢ x < tan x
[PROOFSTEP]
have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
⊢ x < tan x
[PROOFSTEP]
have cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y := by
  intro y hy
  exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
⊢ ∀ {y : ℝ}, y ∈ U → 0 < cos y
[PROOFSTEP]
intro y hy
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
y : ℝ
hy : y ∈ U
⊢ 0 < cos y
[PROOFSTEP]
exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
⊢ x < tan x
[PROOFSTEP]
have sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y :=
  by
  intro y hy
  rw [intU] at hy
  exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
⊢ ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
[PROOFSTEP]
intro y hy
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
y : ℝ
hy : y ∈ interior U
⊢ 0 < sin y
[PROOFSTEP]
rw [intU] at hy
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
y : ℝ
hy : y ∈ Ioo 0 (π / 2)
⊢ 0 < sin y
[PROOFSTEP]
exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ x < tan x
[PROOFSTEP]
have tan_cts_U : ContinuousOn tan U := by
  apply ContinuousOn.mono continuousOn_tan
  intro z hz
  simp only [mem_setOf_eq]
  exact (cos_pos hz).ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ ContinuousOn tan U
[PROOFSTEP]
apply ContinuousOn.mono continuousOn_tan
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ U ⊆ {x | cos x ≠ 0}
[PROOFSTEP]
intro z hz
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ z ∈ {x | cos x ≠ 0}
[PROOFSTEP]
simp only [mem_setOf_eq]
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ cos z ≠ 0
[PROOFSTEP]
exact (cos_pos hz).ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
⊢ x < tan x
[PROOFSTEP]
have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
⊢ x < tan x
[PROOFSTEP]
have deriv_pos : ∀ y : ℝ, y ∈ interior U → 0 < deriv (fun y' : ℝ => tan y' - y') y :=
  by
  intro y hy
  have := cos_pos (interior_subset hy)
  simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
  norm_cast
  have bd2 : cos y ^ 2 < 1 := by
    apply lt_of_le_of_ne y.cos_sq_le_one
    rw [cos_sq']
    simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
  rwa [one_div, lt_inv, inv_one]
  · exact zero_lt_one
  simpa only [sq, mul_self_pos] using this.ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
⊢ ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
intro y hy
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
⊢ 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
have := cos_pos (interior_subset hy)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < ↑1 / cos y ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < 1 / cos y ^ 2
[PROOFSTEP]
have bd2 : cos y ^ 2 < 1 := by
  apply lt_of_le_of_ne y.cos_sq_le_one
  rw [cos_sq']
  simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 < 1
[PROOFSTEP]
apply lt_of_le_of_ne y.cos_sq_le_one
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 ≠ 1
[PROOFSTEP]
rw [cos_sq']
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 - sin y ^ 2 ≠ 1
[PROOFSTEP]
simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 1 < 1 / cos y ^ 2
[PROOFSTEP]
rwa [one_div, lt_inv, inv_one]
[GOAL]
case ha
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case hb
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 0 < cos y ^ 2
[PROOFSTEP]
simpa only [sq, mul_self_pos] using this.ne'
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
⊢ x < tan x
[PROOFSTEP]
have mono := Convex.strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
⊢ x < tan x
[PROOFSTEP]
have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
⊢ 0 ∈ U
[PROOFSTEP]
rwa [left_mem_Ico]
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
zero_in_U : 0 ∈ U
⊢ x < tan x
[PROOFSTEP]
have x_in_U : x ∈ U := ⟨h1.le, h2⟩
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
zero_in_U : 0 ∈ U
x_in_U : x ∈ U
⊢ x < tan x
[PROOFSTEP]
simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1
[GOAL]
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x
[PROOFSTEP]
rcases eq_or_lt_of_le h1 with (rfl | h1')
[GOAL]
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0
[PROOFSTEP]
rw [tan_zero]
[GOAL]
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
[PROOFSTEP]
exact le_of_lt (lt_tan h1' h2)
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
suffices ∀ {y : ℝ} (_ : 0 < y) (_ : y ≤ 3 * π / 2), cos y < ↑1 / sqrt (y ^ 2 + 1)
  by
  rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
  · exact this h hx2
  · convert this (by linarith : 0 < -x) (by linarith) using 1
    · rw [cos_neg]
    · rw [neg_sq]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h : 0 < x
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
exact this h hx2
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
convert this (by linarith : 0 < -x) (by linarith) using 1
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ -x ≤ 3 * π / 2
[PROOFSTEP]
linarith
[GOAL]
case h.e'_3
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ cos x = cos (-x)
[PROOFSTEP]
rw [cos_neg]
[GOAL]
case h.e'_4
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ 1 / sqrt (x ^ 2 + 1) = 1 / sqrt ((-x) ^ 2 + 1)
[PROOFSTEP]
rw [neg_sq]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
intro y hy1 hy2
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
have hy3 : ↑0 < y ^ 2 + 1 := by linarith [sq_nonneg y]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ 0 < y ^ 2 + 1
[PROOFSTEP]
linarith [sq_nonneg y]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
rcases lt_or_le y (π / 2) with (hy2' | hy1')
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ -(π / 2) < y
[PROOFSTEP]
linarith
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
rw [← abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨by linarith, hy2'.le⟩), ←
  abs_of_nonneg (one_div_nonneg.mpr (sqrt_nonneg _)), ← sq_lt_sq, div_pow, one_pow, sq_sqrt hy3.le,
  lt_one_div (pow_pos hy4 _) hy3, ← inv_one_add_tan_sq hy4.ne', one_div, inv_inv, add_comm, add_lt_add_iff_left,
  sq_lt_sq, abs_of_pos hy1, abs_of_nonneg (tan_nonneg_of_nonneg_of_le_pi_div_two hy1.le hy2'.le)]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ -(π / 2) ≤ y
[PROOFSTEP]
linarith
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y < tan y
[PROOFSTEP]
exact Real.lt_tan hy1 hy2'
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
refine' lt_of_le_of_lt _ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y ≤ 0
[PROOFSTEP]
exact cos_nonpos_of_pi_div_two_le_of_le hy1' (by linarith [pi_pos])
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ y ≤ π + π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx3)
[GOAL]
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / sqrt (0 ^ 2 + 1)
[PROOFSTEP]
simp
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le


[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
w : E
⊢ w ∈ sphere 0 r → -w ∈ sphere 0 r
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ ball 0 r → -w ∈ ball 0 r
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
i : SeminormedAddCommGroup E
r✝ r : ℝ
w : E
⊢ w ∈ closedBall 0 r → -w ∈ closedBall 0 r
[PROOFSTEP]
simp


[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ α₂ : Type u₀
β : Type u₁
f : α₀ → α₁
f' : α₁ → α₂
x : F α₀ β
⊢ fst f' (fst f x) = fst (f' ∘ f) x
[PROOFSTEP]
simp [fst, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ fst f (snd f' x) = bimap f f' x
[PROOFSTEP]
simp [fst, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ snd f' (fst f x) = bimap f f' x
[PROOFSTEP]
simp [snd, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
β₀ β₁ β₂ : Type u₁
g : β₀ → β₁
g' : β₁ → β₂
x : F α β₀
⊢ snd g' (snd g x) = snd (g' ∘ g) x
[PROOFSTEP]
simp [snd, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Prod
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.3875} {β : Type ?u.3874} (x : α × β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.3875} {β₀ β₁ β₂ : Type ?u.3874} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : α₀ × β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α✝ : Type ?u.3875
β✝ : Type ?u.3874
x✝ : α✝ × β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α₀✝ α₁✝ α₂✝ : Type ?u.3875
β₀✝ β₁✝ β₂✝ : Type ?u.3874
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : α₀✝ × β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Const
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.4176} {β : Type ?u.4177} (x : Const α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.4176} {β₀ β₁ β₂ : Type ?u.4177} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : Const α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α✝ : Type ?u.4176
β✝ : Type ?u.4177
x✝ : Const α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α₀✝ α₁✝ α₂✝ : Type ?u.4176
β₀✝ β₁✝ β₂✝ : Type ?u.4177
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : Const α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (_root_.flip F)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u₁} {β : Type u₀} (x : _root_.flip F α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₁} {β₀ β₁ β₂ : Type u₀} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : _root_.flip F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α✝ : Type u₁
β✝ : Type u₀
x✝ : _root_.flip F α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₁
β₀✝ β₁✝ β₂✝ : Type u₀
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : _root_.flip F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Sum
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.4990} {β : Type ?u.4989} (x : α ⊕ β), bimap id id x = x
[PROOFSTEP]
aesop
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.4990} {β₀ β₁ β₂ : Type ?u.4989} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : α₀ ⊕ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
aesop
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ LawfulFunctor (F α)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β : Type u₁}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 : Type u₁} (x : F α α_1), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β γ : Type u₁} (g : α_1 → β) (h : β → γ) (x : F α α_1), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ β✝ : Type u₁
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ : Type u₁
x✝ : F α α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
case refine'_3
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ β✝ γ✝ : Type u₁
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : F α α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompl F G H)
[PROOFSTEP]
constructor
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u_1} {β : Type u_2} (x : bicompl F G H α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u_1} {β₀ β₁ β₂ : Type u_2} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : bicompl F G H α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α✝ : Type u_1
β✝ : Type u_2
x✝ : bicompl F G H α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, map_id, map_comp_map, functor_norm]
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u_1
β₀✝ β₁✝ β₂✝ : Type u_2
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompl F G H α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, map_id, map_comp_map, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompr G F)
[PROOFSTEP]
constructor
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u₀} {β : Type u₁} (x : bicompr G F α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : bicompr G F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α✝ : Type u₀
β✝ : Type u₁
x✝ : bicompr G F α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, functor_norm]