-- Mathlib/NumberTheory/Ostrowski.lean
/-- The minimal positive integer with absolute value smaller than 1 is a prime number. -/
lemma is_prime_of_minimal_nat_zero_lt_and_lt_one : p.Prime

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ 1 < a

Tactic:
omega

Result:
no goals

Proof state:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [Nat.isUnit_iff, Nat.isUnit_iff]

Result:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
⊢ a = 1 ∨ b = 1

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
⊢ False

Tactic:
have ha :=
  le_of_not_lt <| not_and.mp ((hmin a).mt hap.not_le) (map_pos_of_ne_zero f (mod_cast ha₀))

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
⊢ False

Proof state:
case isUnit_or_isUnit'.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ False

Tactic:
obtain ⟨ha₀, hb₀⟩ : a ≠ 0 ∧ b ≠ 0 := by
  refine mul_ne_zero_iff.mp fun h ↦ ?_
  rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Nat.Prime p

Tactic:
rw [← Nat.irreducible_iff_nat_prime]

Result:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Irreducible p

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ 0 < b

Tactic:
omega

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ 0 < a

Tactic:
omega

Result:
no goals

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
hb : 1 ≤ f ↑b
⊢ False

Tactic:
rw [Nat.cast_mul, map_mul] at hp1

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑a * f ↑b < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
hb : 1 ≤ f ↑b
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
refine mul_ne_zero_iff.mp fun h ↦ ?_

Result:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
⊢ False

Proof state:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
con : a ≠ 1 ∧ b ≠ 1
⊢ False

Tactic:
obtain ⟨ha₁, hb₁⟩ := con

Result:
case isUnit_or_isUnit'.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ False

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑a * f ↑b < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
hb : 1 ≤ f ↑b
⊢ False

Tactic:
exact ((one_le_mul_of_one_le_of_one_le ha hb).trans_lt hp1).false

Result:
no goals

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
⊢ False

Tactic:
have hb :=
  le_of_not_lt <| not_and.mp ((hmin b).mt hbp.not_le) (map_pos_of_ne_zero f (mod_cast hb₀))

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : 1 ≤ f ↑a
hb : 1 ≤ f ↑b
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Irreducible p

Tactic:
constructor

Result:
case not_unit
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ¬IsUnit p

case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∀ (a b : ℕ), p = a * b → IsUnit a ∨ IsUnit b

Proof state:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
⊢ a = 1 ∨ b = 1

Tactic:
by_contra! con

Result:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
con : a ≠ 1 ∧ b ≠ 1
⊢ False

Proof state:
case not_unit
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ¬IsUnit p

Tactic:
rw [Nat.isUnit_iff]

Result:
case not_unit
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ¬p = 1

Proof state:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ False

Tactic:
have hap : a < a * b := lt_mul_of_one_lt_right (by omega) (by omega)

Result:
case isUnit_or_isUnit'.intro.intro
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
⊢ False

Tactic:
rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0

Result:
no goals

Proof state:
case not_unit
f : AbsoluteValue ℚ ℝ
hp0 : 0 < f ↑1
hp1 : f ↑1 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 1 ≤ m
⊢ False

Tactic:
simp only [Nat.cast_one, map_one, lt_self_iff_false] at hp1

Result:
no goals

Proof state:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∀ (a b : ℕ), p = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro a b rfl

Result:
case isUnit_or_isUnit'
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
⊢ IsUnit a ∨ IsUnit b