awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
hn1 : n ≠ 0
hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
P : Set ℕ :=
  {m : ℕ |
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)}
⊢ P.Nonempty

Tactic:
have hP : P.Nonempty :=
    ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
hn1 : n ≠ 0
hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
P : Set ℕ :=
  {m : ℕ |
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)}
hP : P.Nonempty
⊢ ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m

Tactic:
⟨sInf P, Nat.sInf_mem hP, fun m hm ↦ Nat.sInf_le hm⟩

Premises used: Nat.sInf_mem, Nat.sInf_le, And.intro, Exists.intro, InfSet.sInf
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
hn1 : n ≠ 0
hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
P : Set ℕ :=
  {m : ℕ |
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)}
hP : P.Nonempty
⊢ ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m

Tactic:
exact ⟨sInf P, Nat.sInf_mem hP, fun m hm ↦ Nat.sInf_le hm⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
not_isUnit : ¬IsUnit p
isUnit_or_isUnit : ∀ ⦃a b : ℕ⦄, p = a * b → IsUnit a ∨ IsUnit b
⊢ Irreducible p

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
not_isUnit : ¬p = 1
⊢ ¬IsUnit p

Tactic:
rw [Nat.isUnit_iff]

Premises used: Nat.isUnit_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      1 ≤ m
⊢ False

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

Premises used: map_one, lt_self_iff_false, Nat.cast_one
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
isUnit_or_isUnit : a = 1 ∨ b = 1
⊢ IsUnit a ∨ IsUnit b

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

Premises used: Nat.isUnit_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
isUnit_or_isUnit : ∀ (ha₁ : a ≠ 1) (hb₁ : b ≠ 1), False
⊢ a = 1 ∨ b = 1

Tactic:
by_contra! ⟨ha₁, hb₁⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
mul_ne_zero_iff.mp fun h ↦ ?_

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
refine : ∀ (h : a * b = 0), False
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
refine mul_ne_zero_iff.mp fun h ↦ ?_

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
rwa :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₁ :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) 0 : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₂ :
  ∀ (hp0 : LT.lt (α := ℝ) 0 0) (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hp0 : False) (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
⊢ False

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

Premises used: map_zero, lt_self_iff_false, Nat.cast_zero
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ a ≠ 0

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
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
⊢ b ≠ 0

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
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ 0 < a

Tactic:
lia
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ 1 < b

Tactic:
lia
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ a < a * b

Tactic:
have hap : a < a * b := lt_mul_of_one_lt_right (by lia) (by lia)
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ 0 < b

Tactic:
lia
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ 1 < a

Tactic:
lia
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ b < a * b

Tactic:
have hbp : b < a * b := lt_mul_of_one_lt_left (by lia) (by lia)
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)

Tactic:
have ha :=
      le_of_not_gt <| not_and.mp ((hmin a).mt hap.not_ge) (map_pos_of_ne_zero f (mod_cast ha₀))
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)

Tactic:
have hb :=
      le_of_not_gt <| not_and.mp ((hmin b).mt hbp.not_ge) (map_pos_of_ne_zero f (mod_cast hb₀))
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
⊢ ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
⊢ a ≠ 1

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₂ : a ≠ 1
⊢ b ≠ 1

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₂ : a ≠ 1
hb₂ : b ≠ 1
⊢ a ≠ 0

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₂ : a ≠ 1
hb₂ : b ≠ 1
ha₃ : a ≠ 0
⊢ b ≠ 0

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₂ : a ≠ 1
hb₂ : b ≠ 1
ha₃ : a ≠ 0
hb₃ : b ≠ 0
⊢ a < a * b

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₂ : a ≠ 1
hb₂ : b ≠ 1
ha₃ : a ≠ 0
hb₃ : b ≠ 0
hap₁ : a < a * b
⊢ b < a * b

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin₁ :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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₄ : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)

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

Premises used: map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
⊢ False

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

Premises used: LT.lt.false, LE.le.trans_lt, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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 : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
⊢ False

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

Premises used: LT.lt.false, LE.le.trans_lt, one_le_mul_of_one_le_of_one_le