awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
rw : a * b⁻¹ * c = a * (b⁻¹ * c)
ha : b ≠ 0 ∨ c⁻¹ ≠ ∞
hb : b ≠ ∞ ∨ c⁻¹ ≠ 0
⊢ a * b⁻¹ * c = a * (b * c⁻¹)⁻¹

Tactic:
rw [ENNReal.mul_inv, inv_inv]

Premises used: inv_inv, ENNReal.mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a * b⁻¹ * c = a * (b⁻¹ * c)

Tactic:
ring
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
hc : c ≠ 0 ∨ d ≠ ∞
hd : c ≠ ∞ ∨ d ≠ 0
simp : a * b * (c⁻¹ * d⁻¹) = a * c⁻¹ * (b * d⁻¹)
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
simp only [div_eq_mul_inv, ENNReal.mul_inv hc hd]

Premises used: div_eq_mul_inv, ENNReal.mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
hc : c ≠ 0 ∨ d ≠ ∞
hd : c ≠ ∞ ∨ d ≠ 0
⊢ a * b * (c⁻¹ * d⁻¹) = a * c⁻¹ * (b * d⁻¹)

Tactic:
ring
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a ≠ 0
⊢ 0 < a / 2

Tactic:
ENNReal.div_pos h ofNat_ne_top

Premises used: ENNReal.ofNat_ne_top, ENNReal.div_pos
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ LT.lt (α := ℝ≥0∞) 2⁻¹ 1

Tactic:
ENNReal.inv_lt_one.2 <| one_lt_two

Premises used: ENNReal.one_lt_two, Iff.mpr, ENNReal.inv_lt_one
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
⊢ a ≠ ∞

Tactic:
ht
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
lift : ∀ (a : ℝ≥0) (hz : (↑a : ℝ≥0∞) ≠ 0), (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)
⊢ a / 2 < a

Tactic:
lift a to ℝ≥0 using ht
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
hz : (↑a : ℝ≥0∞) ≠ 0
⊢ a ≠ 0

Tactic:
rw [coe_ne_zero] at hz

Premises used: ENNReal.coe_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
hz : a ≠ 0
rw : a / 2 < a
rw₁ : Ne (α := ℝ≥0) 2 0
⊢ (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)

Tactic:
rw [← coe_two, ← coe_div, coe_lt_coe]

Premises used: ENNReal.coe_lt_coe, ENNReal.coe_two, ENNReal.coe_div
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

Tactic:
NNReal.half_lt_self hz

Premises used: NNReal.half_lt_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
hz : a ≠ 0
⊢ Ne (α := ℝ≥0) 2 0

Tactic:
two_ne_zero' _

Premises used: two_ne_zero'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

Tactic:
exacts [NNReal.half_lt_self hz, two_ne_zero' _]

Premises used: two_ne_zero', NNReal.half_lt_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a / 2 ≤ a

Tactic:
le_add_self.trans_eq <| ENNReal.add_halves _

Premises used: LE.le.trans_eq, ENNReal.add_halves, le_add_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a ≠ ∞
⊢ a - a / 2 = a / 2

Tactic:
ENNReal.sub_eq_of_eq_add' h a.add_halves.symm

Premises used: ENNReal.add_halves, Eq.symm, ENNReal.sub_eq_of_eq_add'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
rw : 1 - 1 / 2 = 1 / 2
rw₁ rw₂ : 1 / 2 = 1 / 2
⊢ HSub.hSub (α := ℝ≥0∞) 1 2⁻¹ = 2⁻¹

Tactic:
rw [← one_div, sub_half one_ne_top]

Premises used: ENNReal.sub_half, one_div, ENNReal.one_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc : c < a * b
obtain : ∀ (a' : ℝ≥0∞) (hc : c / b < a') (ha' : a' < a), ∃ a' < a, c < a' * b
⊢ ∃ a' < a, c < a' * b

Tactic:
obtain ⟨a', hc, ha'⟩ := exists_between (ENNReal.div_lt_of_lt_mul hc)

Premises used: exists_between, ENNReal.div_lt_of_lt_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c a' : ℝ≥0∞
ha' : a' < a
hc_1 : c < a * 0
hc : c / 0 < a'
⊢ False

Tactic:
simp at *
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b a' : ℝ≥0∞
ha' : a' < a
hc_1 : ∞ < a * b
hc : ∞ / b < a'
⊢ False

Tactic:
simp at *
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc_1 : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' * b

Tactic:
exact ⟨_, ha', (ENNReal.div_lt_iff (.inl <| by rintro rfl; simp at *)
    (.inr <| by rintro rfl; simp at *)).1 hc⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc : c < a * b
simp_rw : ∀ (hc : c < b * a), ∃ b' < b, c < b' * a
⊢ ∃ b' < b, c < a * b'

Tactic:
simp_rw [mul_comm a] at hc ⊢

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc : c < b * a
⊢ ∃ b' < b, c < b' * a

Tactic:
exists_lt_mul_left hc

Premises used: _private.0.ENNReal.exists_lt_mul_left
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc : c < b * a
⊢ ∃ b' < b, c < b' * a

Tactic:
exact exists_lt_mul_left hc

Premises used: _private.0.ENNReal.exists_lt_mul_left
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
refine : ∀ (d : ℝ≥0∞) (hd : d < a * b), d ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd : d < a * b
obtain : ∀ (a' : ℝ≥0∞) (ha' : a' < a) (hd : d < a' * b), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd

Premises used: _private.0.ENNReal.exists_lt_mul_left
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd_1 : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd : d < a' * b
obtain : ∀ (b' : ℝ≥0∞) (hb' : b' < b) (hd : d < a' * b'), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd

Premises used: _private.0.ENNReal.exists_lt_mul_right
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd_1 : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd_2 : d < a' * b
b' : ℝ≥0∞
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
le_trans hd.le <| h _ ha' _ hb'

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd_1 : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd_2 : d < a' * b
b' : ℝ≥0∞
hb' : b' < b
hd : d < a' * b'
⊢ d ≤ c

Tactic:
exact le_trans hd.le <| h _ ha' _ hb'

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
rw : a⁻¹ * b⁻¹ ≤ c⁻¹
⊢ c ≤ a * b

Tactic:
rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]

Premises used: ENNReal.inv_le_inv, ENNReal.mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹

Tactic:
mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

Premises used: LE.le.trans_eq, LT.lt.ne_top, ENNReal.le_inv_iff_le_inv, ENNReal.lt_inv_iff_lt_inv, Inv.inv, Iff.mp, Or.inl, Eq.symm, ENNReal.mul_inv, Or.inr, ENNReal.mul_le_of_forall_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹

Tactic:
exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

Premises used: LE.le.trans_eq, LT.lt.ne_top, ENNReal.le_inv_iff_le_inv, ENNReal.lt_inv_iff_lt_inv, Inv.inv, Iff.mp, Or.inl, Eq.symm, ENNReal.mul_inv, Or.inr, ENNReal.mul_le_of_forall_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
refine_1 :
  ∀ (x y : ℝ≥0∞) (hxy : x < y),
    LT.lt (α := (↑(Iic 1) : Type))
      ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) x)
      ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) y)
refine_2 :
  ∀ (x : (↑(Iic 1) : Type)),
    (↑((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯)
            ((fun (x : (↑(Iic 1) : Type)) ↦ ((↑x : ℝ≥0∞)⁻¹ - 1)⁻¹) x)) :
        ℝ≥0∞) =
      (↑x : ℝ≥0∞)
⊢ ℝ≥0∞ ≃o (↑(Iic 1) : Type)

Tactic:
refine StrictMono.orderIsoOfRightInverse
    (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩)
    (fun x y hxy => ?_) (fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_

Premises used: HSub.hSub, Inv.inv, StrictMono.orderIsoOfRightInverse, OfNat.ofNat, Subtype.ext
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ LT.lt (α := (↑(Iic 1) : Type))
    ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) x)
    ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) y)

Tactic:
simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]

Premises used: Subtype.mk_lt_mk, ENNReal.add_lt_add_iff_right, ENNReal.inv_lt_inv, ENNReal.one_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : (↑(Iic 1) : Type)
⊢ 1 ≤ (↑x : ℝ≥0∞)⁻¹

Tactic:
have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : (↑(Iic 1) : Type)
this : 1 ≤ (↑x : ℝ≥0∞)⁻¹
⊢ (↑((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯)
          ((fun (x : (↑(Iic 1) : Type)) ↦ ((↑x : ℝ≥0∞)⁻¹ - 1)⁻¹) x)) :
      ℝ≥0∞) =
    (↑x : ℝ≥0∞)

Tactic:
simp only [inv_inv, tsub_add_cancel_of_le this]

Premises used: tsub_add_cancel_of_le, inv_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : (↑(Iic 1) : Type)
⊢ (orderIsoIicOneBirational.symm : (a : (↑(Iic 1) : Type)) → ℝ≥0∞) x = ((↑x : ℝ≥0∞)⁻¹ - 1)⁻¹

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q a : ℝ≥0
x x_1 : (↑(Iic a) : Type)
⊢ LE.le (α := (↑(Iic (↑a : ℝ≥0∞)) : Type))
      (({
              toFun := fun (x : (↑(Iic a) : Type)) ↦
                Subtype.mk (p := fun (x : ℝ≥0∞) ↦ x ∈ Iic (↑a : ℝ≥0∞)) (↑(↑x : ℝ≥0) : ℝ≥0∞) ⋯,
              invFun := fun (x : (↑(Iic (↑a : ℝ≥0∞)) : Type)) ↦
                Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Iic a) (↑x : ℝ≥0∞).toNNReal ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_2 : (↑(Iic a) : Type)) → (↑(Iic (↑a : ℝ≥0∞)) : Type))
          x :
        (↑(Iic (↑a : ℝ≥0∞)) : Type))
      (({
              toFun := fun (x : (↑(Iic a) : Type)) ↦
                Subtype.mk (p := fun (x : ℝ≥0∞) ↦ x ∈ Iic (↑a : ℝ≥0∞)) (↑(↑x : ℝ≥0) : ℝ≥0∞) ⋯,
              invFun := fun (x : (↑(Iic (↑a : ℝ≥0∞)) : Type)) ↦
                Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Iic a) (↑x : ℝ≥0∞).toNNReal ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_2 : (↑(Iic a) : Type)) → (↑(Iic (↑a : ℝ≥0∞)) : Type))
          x_1 :
        (↑(Iic (↑a : ℝ≥0∞)) : Type)) ↔
    x ≤ x_1

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, coe_le_coe, Subtype.coe_le_coe]

Premises used: Subtype.coe_le_coe, ENNReal.coe_le_coe, Equiv.coe_fn_mk, Subtype.mk_le_mk
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
b : (↑(Iic a) : Type)
⊢ (↑(((orderIsoIicCoe a).symm : (a_1 : (↑(Iic a) : Type)) → (↑(Iic (↑a : ℝ≥0∞)) : Type)) b) : ℝ≥0∞) =
    (↑(↑b : ℝ≥0) : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
⊢ (↑((orderIsoUnitIntervalBirational : (a : ℝ≥0∞) → (↑(Icc 0 1) : Type)) x) : ℝ) = (x⁻¹ + 1)⁻¹.toReal

Tactic:
rfl

Premises used: NNReal, ENNReal.toReal, NNReal.toReal, rfl, WithTop
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a ≠ 0
⊢ ∃ (n : ℕ), (↑n : ℝ≥0∞)⁻¹ < a⁻¹⁻¹

Tactic:
simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]

Premises used: Iff.mpr, ENNReal.exists_nat_gt, ENNReal.inv_ne_top, ENNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ∞
n : ℕ
hn rwa rwa₁ rwa₂ rwa₃ : b / a < (↑n : ℝ≥0∞)
⊢ b < (↑n : ℝ≥0∞) * a

Tactic:
rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]

Premises used: Or.inl, ENNReal.div_lt_iff, Or.inr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ∞
⊢ ∃ (n : ℕ), b < (↑n : ℝ≥0∞) * a

Tactic:
(exists_nat_pos_mul_gt ha hb).imp fun _ => And.right

Premises used: ENNReal.exists_nat_pos_mul_gt, Exists.imp, And.right
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
rcases : ∀ (n : ℕ) (npos : n > 0) (hn : a < (↑n : ℝ≥0∞) * b), ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b
⊢ ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b

Tactic:
rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩

Premises used: ENNReal.exists_nat_pos_mul_gt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
right : (↑n : ℝ≥0∞)⁻¹ * a < b
⊢ ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b

Tactic:
use n, npos
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
right : a / (↑n : ℝ≥0∞) < b
⊢ (↑n : ℝ≥0∞)⁻¹ * a < b

Tactic:
rw [← ENNReal.div_eq_inv_mul]

Premises used: ENNReal.div_eq_inv_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
⊢ a / (↑n : ℝ≥0∞) < b

Tactic:
div_lt_of_lt_mul' hn

Premises used: ENNReal.div_lt_of_lt_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
⊢ a / (↑n : ℝ≥0∞) < b

Tactic:
exact div_lt_of_lt_mul' hn

Premises used: ENNReal.div_lt_of_lt_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
rcases : ∀ (n : ℕ) (npos : 0 < n) (hn : (↑n : ℝ≥0∞)⁻¹ * a < b), ∃ n > 0, (↑n : ℝ≥0∞) * a < b
⊢ ∃ n > 0, (↑n : ℝ≥0∞) * a < b

Tactic:
rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩

Premises used: ENNReal.exists_nat_pos_inv_mul_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n : ℝ≥0∞)⁻¹ * a < b
h : GT.gt (α := ℝ≥0) (↑n : ℝ≥0)⁻¹ 0 ∧ (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) * a < b
⊢ ∃ n > 0, (↑n : ℝ≥0∞) * a < b

Tactic:
use (n : ℝ≥0)⁻¹

Premises used: Nat.cast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n : ℝ≥0∞)⁻¹ * a < b
⊢ GT.gt (α := ℝ≥0) (↑n : ℝ≥0)⁻¹ 0 ∧ (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) * a < b

Tactic:
simp [*, npos.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
rcases : ∀ (n : ℕ) (hn : (↑n : ℝ≥0∞)⁻¹ < a), ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a
⊢ ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a

Tactic:
rcases exists_inv_nat_lt ha with ⟨n, hn⟩

Premises used: ENNReal.exists_inv_nat_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a

Tactic:
⟨n, lt_trans ?_ hn⟩

Premises used: lt_trans, Exists.intro
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
refine : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < (↑n : ℝ≥0∞)⁻¹
⊢ ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a

Tactic:
refine ⟨n, lt_trans ?_ hn⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
rw : (↑n : ℝ≥0∞) < HPow.hPow (α := ℝ≥0∞) 2 n
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < (↑n : ℝ≥0∞)⁻¹

Tactic:
rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]

Premises used: ENNReal.inv_pow, ENNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
norm_cast : n < HPow.hPow (α := ℕ) 2 n
⊢ (↑n : ℝ≥0∞) < HPow.hPow (α := ℝ≥0∞) 2 n

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ n < HPow.hPow (α := ℕ) 2 n

Tactic:
n.lt_two_pow_self

Premises used: Nat.lt_two_pow_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ n < HPow.hPow (α := ℕ) 2 n

Tactic:
exact n.lt_two_pow_self

Premises used: Nat.lt_two_pow_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℤ
ofNat : ∀ (n : ℕ), (↑(r ^ Int.ofNat n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.ofNat n
negSucc : ∀ (n : ℕ), (↑(r ^ Int.negSucc n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.negSucc n
⊢ (↑(r ^ n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ n

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ (↑(r ^ Int.ofNat n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.ofNat n

Tactic:
simp only [Int.ofNat_eq_natCast, coe_pow, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast, ENNReal.coe_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ r ^ n.succ ≠ 0

Tactic:
have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ n.succ ≠ 0
⊢ (↑(r ^ Int.negSucc n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.negSucc n

Tactic:
simp only [zpow_negSucc, coe_inv this, coe_pow]

Premises used: ENNReal.coe_inv, zpow_negSucc, ENNReal.coe_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℤ
ofNat : HPow.hPow (α := ℝ≥0∞) 0 (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞
ofNat₁ :
  ∀ (n : ℕ),
    HPow.hPow (α := ℝ≥0∞) 0 (Int.ofNat (n + 1)) =
      if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞
negSucc :
  ∀ (n : ℕ),
    HPow.hPow (α := ℝ≥0∞) 0 (Int.negSucc n) = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 n = if n = 0 then 1 else if 0 < n then 0 else ∞

Tactic:
obtain ((_ | n) | n) := n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ HPow.hPow (α := ℝ≥0∞) 0 (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) 0 (Int.ofNat (n + 1)) =
    if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) 0 (Int.negSucc n) = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℤ
ofNat : HPow.hPow (α := ℝ≥0∞) ∞ (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0
ofNat₁ :
  ∀ (n : ℕ),
    HPow.hPow (α := ℝ≥0∞) ∞ (Int.ofNat (n + 1)) =
      if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0
negSucc :
  ∀ (n : ℕ),
    HPow.hPow (α := ℝ≥0∞) ∞ (Int.negSucc n) = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ n = if n = 0 then 1 else if 0 < n then ∞ else 0

Tactic:
obtain ((_ | n) | n) := n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (Int.ofNat (n + 1)) =
    if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ (Int.negSucc n) = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

Premises used: Int.natCast_add, Nat.cast_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
ofNat : ∀ (a_1 : ℕ), 0 < a ^ Int.ofNat a_1
negSucc : ∀ (a_1 : ℕ), 0 < a ^ Int.negSucc a_1
⊢ 0 < a ^ n

Tactic:
cases n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a_1 : ℕ
⊢ 0 < a ^ Int.ofNat a_1

Tactic:
simpa using ENNReal.pow_pos ha.bot_lt _

Premises used: ENNReal.pow_pos, Ne.bot_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a_1 : ℕ
⊢ 0 < a ^ Int.negSucc a_1

Tactic:
simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and,
      not_false_eq_true]

Premises used: zpow_negSucc, false_and, Ne, not_false_eq_true, ENNReal.inv_pos, ENNReal.pow_eq_top_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
ofNat : ∀ (a_1 : ℕ), a ^ Int.ofNat a_1 < ∞
negSucc : ∀ (a_1 : ℕ), a ^ Int.negSucc a_1 < ∞
⊢ a ^ n < ∞

Tactic:
cases n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a_1 : ℕ
⊢ a ^ Int.ofNat a_1 < ∞

Tactic:
simpa using ENNReal.pow_lt_top h'a.lt_top

Premises used: ENNReal.pow_lt_top, Ne.lt_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a_1 : ℕ
⊢ a ^ Int.negSucc a_1 < ∞

Tactic:
simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]

Premises used: zpow_negSucc, ENNReal.pow_pos, ENNReal.inv_lt_top, Ne.bot_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ a ^ n ≠ ∞

Tactic:
(ENNReal.zpow_lt_top ha h'a n).ne

Premises used: ENNReal.zpow_lt_top, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ x ≠ ∞

Tactic:
h'x
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
lift x to ℝ≥0 using h'x
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
⊢ y ≠ ∞

Tactic:
h'y
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
lift : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
lift y to ℝ≥0 using h'y
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ y ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

Premises used: Ne, ENNReal.coe_eq_zero, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ y ≠ 0

Tactic:
have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)

Premises used: Set.Mem, setOf, Set.Ico, Iff.mp, NNReal.exists_mem_Ico_zpow, ENNReal.one_lt_coe_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
refine : x ≠ 0
⊢ ∃ (n : ℤ), y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)

Premises used: Iff.mp, NNReal.exists_mem_Ico_zpow, ENNReal.one_lt_coe_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ x ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using hx

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
obtain :
  ∀ (n : ℤ) (hn : y ^ n ≤ x) (h'n : x < y ^ (n + 1)),
    ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))

Tactic:
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) := by
    refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))

Tactic:
⟨n, ?_, ?_⟩

Premises used: And.intro, Exists.intro