awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
refine_1 : (↑y : ℝ≥0∞) ^ n ≤ (↑x : ℝ≥0∞)
refine_2 : (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞) ^ (n + 1)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))

Tactic:
refine ⟨n, ?_, ?_⟩
-- 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)
refine_1 : (↑(y ^ n) : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : y ^ n ≤ x
⊢ (↑y : ℝ≥0∞) ^ n ≤ (↑x : ℝ≥0∞)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_zpow, ENNReal.coe_le_coe
-- 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)
refine_2 : (↑x : ℝ≥0∞) < (↑(y ^ (n + 1)) : ℝ≥0∞)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : x < y ^ (n + 1)
⊢ (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞) ^ (n + 1)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

Premises used: ENNReal.coe_zpow, ENNReal.coe_lt_coe
-- 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∞) ∈ Ioc (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ioc (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
lift : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc (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∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), y ^ n < x ∧ x ≤ y ^ (n + 1)

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

Premises used: Set.Ioc, Set.Mem, setOf, Iff.mp, ENNReal.one_lt_coe_iff, NNReal.exists_mem_Ioc_zpow
-- 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_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)

Premises used: Iff.mp, ENNReal.one_lt_coe_iff, NNReal.exists_mem_Ioc_zpow
-- 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∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑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_Ioc_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∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))

Tactic:
⟨n, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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)
refine_1 : (↑y : ℝ≥0∞) ^ n < (↑x : ℝ≥0∞)
refine_2 : (↑x : ℝ≥0∞) ≤ (↑y : ℝ≥0∞) ^ (n + 1)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))

Tactic:
refine ⟨n, ?_, ?_⟩
-- 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)
refine_1 : (↑(y ^ n) : ℝ≥0∞) < (↑x : ℝ≥0∞)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : y ^ n < x
⊢ (↑y : ℝ≥0∞) ^ n < (↑x : ℝ≥0∞)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

Premises used: ENNReal.coe_zpow, ENNReal.coe_lt_coe
-- 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)
refine_2 : (↑x : ℝ≥0∞) ≤ (↑(y ^ (n + 1)) : ℝ≥0∞)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : x ≤ y ^ (n + 1)
⊢ (↑x : ℝ≥0∞) ≤ (↑y : ℝ≥0∞) ^ (n + 1)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_zpow, ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
h :
  ∀ (x : ℝ≥0∞),
    Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) x ↔ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))) x
⊢ Eq (α := Set ℝ≥0∞) (Ioo 0 ∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1)))

Tactic:
ext x
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
h : 0 < x ∧ x < ∞ ↔ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
⊢ Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) x ↔ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))) x

Tactic:
simp only [mem_iUnion, mem_Ioo, mem_Ico]

Premises used: Set.mem_Ioo, Set.mem_Ico, Set.mem_iUnion
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
h : 0 < x ∧ x < ∞ → ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
h₁ : (∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞
⊢ 0 < x ∧ x < ∞ ↔ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
constructor
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
hx : 0 < x
h'x : x < ∞
⊢ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y

Premises used: Set.Mem, setOf, Set.Ico, LT.lt.ne', ENNReal.exists_mem_Ico_zpow, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
hx : 0 < x
h'x : x < ∞
⊢ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y

Premises used: LT.lt.ne', ENNReal.exists_mem_Ico_zpow, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
h : 0 < x
h₁ : x < ∞
⊢ 0 < x ∧ x < ∞

Tactic:
constructor
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
apply : 0 < y ^ n
⊢ 0 < x

Tactic:
apply lt_of_lt_of_le _ hn

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n

Tactic:
ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _

Premises used: ENNReal.zpow_pos, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n

Tactic:
exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _

Premises used: ENNReal.zpow_pos, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
apply : y ^ (n + 1) < ∞
⊢ x < ∞

Tactic:
apply lt_trans h'n _

Premises used: lt_trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ∞

Tactic:
ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

Premises used: ENNReal.zpow_lt_top, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ∞

Tactic:
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

Premises used: ENNReal.zpow_lt_top, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
ofNat : ∀ (a : ℕ) (h : Int.ofNat a ≤ b), x ^ Int.ofNat a ≤ x ^ b
negSucc : ∀ (a : ℕ) (h : Int.negSucc a ≤ b), x ^ Int.negSucc a ≤ x ^ b
⊢ x ^ a ≤ x ^ b

Tactic:
obtain a | a := a
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.ofNat a ≤ b
ofNat : ∀ (b : ℕ) (h : Int.ofNat a ≤ Int.ofNat b), x ^ Int.ofNat a ≤ x ^ Int.ofNat b
ofNat₁ : ∀ (b : ℕ) (h : Int.ofNat a ≤ Int.negSucc b), x ^ Int.ofNat a ≤ x ^ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ b

Tactic:
obtain b | b := b
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.negSucc a ≤ b
negSucc : ∀ (b : ℕ) (h : Int.negSucc a ≤ Int.ofNat b), x ^ Int.negSucc a ≤ x ^ Int.ofNat b
negSucc₁ : ∀ (b : ℕ) (h : Int.negSucc a ≤ Int.negSucc b), x ^ Int.negSucc a ≤ x ^ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ b

Tactic:
obtain b | b := b
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
ofNat : x ^ a ≤ x ^ b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

Tactic:
simp only [Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b

Tactic:
pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)

Premises used: pow_right_mono₀, Int.le_of_ofNat_le_ofNat
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b

Tactic:
exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)

Premises used: pow_right_mono₀, Int.le_of_ofNat_le_ofNat
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
apply : Int.negSucc b < Int.ofNat a
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

Tactic:
apply absurd h (not_le_of_gt _)

Premises used: absurd, not_le_of_gt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.negSucc b < Int.ofNat a

Tactic:
lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)

Premises used: Int.negSucc_lt_zero, lt_of_lt_of_le, Int.natCast_nonneg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.negSucc b < Int.ofNat a

Tactic:
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)

Premises used: Int.negSucc_lt_zero, lt_of_lt_of_le, Int.natCast_nonneg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
negSucc : (x ^ (a + 1))⁻¹ ≤ x ^ b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

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

Premises used: zpow_natCast, zpow_negSucc, Int.ofNat_eq_natCast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b

Tactic:
(ENNReal.inv_le_one.2 ?_).trans ?_

Premises used: Iff.mpr, LE.le.trans, ENNReal.inv_le_one
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
negSucc : 1 ≤ x ^ (a + 1)
negSucc₁ : 1 ≤ x ^ b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b

Tactic:
refine (ENNReal.inv_le_one.2 ?_).trans ?_

Premises used: Iff.mpr, LE.le.trans, ENNReal.inv_le_one
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)

Tactic:
one_le_pow_of_one_le' hx _

Premises used: one_le_pow_of_one_le'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)

Tactic:
exact one_le_pow_of_one_le' hx _

Premises used: one_le_pow_of_one_le'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b

Tactic:
one_le_pow_of_one_le' hx _

Premises used: one_le_pow_of_one_le'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b

Tactic:
exact one_le_pow_of_one_le' hx _

Premises used: one_le_pow_of_one_le'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
negSucc : x ^ (b + 1) ≤ x ^ (a + 1)
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b

Tactic:
simp only [zpow_negSucc, ENNReal.inv_le_inv]

Premises used: zpow_negSucc, ENNReal.inv_le_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
negSucc : b + 1 ≤ a + 1
⊢ x ^ (b + 1) ≤ x ^ (a + 1)

Tactic:
apply pow_right_mono₀ hx

Premises used: pow_right_mono₀
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1

Tactic:
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using h

Premises used: Int.natCast_add, Int.ofNat_one, Int.ofNat_le, neg_le_neg_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
⊢ Monotone (β := ℝ≥0∞) fun (x_1 : ℤ) ↦ x ^ x_1

Tactic:
fun _ _ h =>
  zpow_le_of_le hx h

Premises used: Monotone, ENNReal.zpow_le_of_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
⊢ x ≠ ∞

Tactic:
h'x
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0), (↑x : ℝ≥0∞) ^ (m + n) = (↑x : ℝ≥0∞) ^ m * (↑x : ℝ≥0∞) ^ n
⊢ x ^ (m + n) = x ^ m * x ^ n

Tactic:
lift x to ℝ≥0 using h'x
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
m n : ℤ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 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:
m n : ℤ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
⊢ x ≠ 0

Tactic:
replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ (↑x : ℝ≥0∞) ^ (m + n) = (↑x : ℝ≥0∞) ^ m * (↑x : ℝ≥0∞) ^ n

Tactic:
simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]

Premises used: ENNReal.coe_zpow, ENNReal.coe_mul, zpow_add₀
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
inl : ∀ (hx₀ : x = 0), x ^ (-m) = (x ^ m)⁻¹
inr : ∀ (hx₀ : x ≠ 0), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hx₀ | hx₀ := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
inl : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
inl₁ : ∀ (hm : m = 0), x ^ (-m) = (x ^ m)⁻¹
inl₂ : ∀ (hm : 0 < m), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hm | hm | hm := lt_trichotomy m 0

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ENNReal.zero_zpow_def, ne_of_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ENNReal.zero_zpow_def, ne_of_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ENNReal.zero_zpow_def, ne_of_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
inr : ∀ (hx : x = ∞), x ^ (-m) = (x ^ m)⁻¹
inr₁ : ∀ (hx : x ≠ ∞), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hx | hx := eq_or_ne x ⊤

Premises used: eq_or_ne, Top.top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
inr : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
inr₁ : ∀ (hm : m = 0), x ^ (-m) = (x ^ m)⁻¹
inr₂ : ∀ (hm : 0 < m), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hm | hm | hm := lt_trichotomy m 0

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ne_of_lt, ENNReal.top_zpow_def
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ne_of_lt, ENNReal.top_zpow_def
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

Premises used: lt_asymm, ne_of_gt, ne_of_lt, ENNReal.top_zpow_def
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x ≠ ∞
⊢ x ^ (-m) * x ^ m = 1

Tactic:
simp [← ENNReal.zpow_add hx₀ hx]

Premises used: ENNReal.zpow_add
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x ≠ ∞
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])

Premises used: ENNReal.eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
rw : x ^ (m + -n) = x ^ m * (x ^ n)⁻¹
rw₁ : x ^ m * x ^ (-n) = x ^ m * (x ^ n)⁻¹
rw₂ rw₃ : x ^ m * (x ^ n)⁻¹ = x ^ m * (x ^ n)⁻¹
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹

Tactic:
rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]

Premises used: sub_eq_add_neg, ENNReal.zpow_add, ENNReal.zpow_neg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
n : ℤ
ofNat : ∀ (a : ℕ), x⁻¹ ^ Int.ofNat a = (x ^ Int.ofNat a)⁻¹
negSucc : ∀ (a : ℕ), x⁻¹ ^ Int.negSucc a = (x ^ Int.negSucc a)⁻¹
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
cases n
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
a : ℕ
⊢ x⁻¹ ^ Int.ofNat a = (x ^ Int.ofNat a)⁻¹

Tactic:
simp [ENNReal.inv_pow]

Premises used: ENNReal.inv_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
a : ℕ
⊢ x⁻¹ ^ Int.negSucc a = (x ^ Int.negSucc a)⁻¹

Tactic:
simp [ENNReal.inv_pow]

Premises used: ENNReal.inv_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
n : ℤ
rw : x⁻¹ ^ n = (x ^ n)⁻¹
rw₁ rw₂ : (x ^ n)⁻¹ = (x ^ n)⁻¹
⊢ x⁻¹ ^ n = x ^ (-n)

Tactic:
rw [ENNReal.zpow_neg, ENNReal.inv_zpow]

Premises used: ENNReal.inv_zpow, ENNReal.zpow_neg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℤ
hn : n ≤ 0
x : ℝ≥0∞
hx : 1 ≤ x
obtain : ∀ (m : ℤ) (hn : -m ≤ 0), x ^ (-m) ≤ 1
⊢ x ^ n ≤ 1

Tactic:
obtain ⟨m, rfl⟩ := neg_surjective n

Premises used: neg_surjective, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ 0 ≤ m

Tactic:
simpa using hn
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
lift : ∀ (m : ℕ) (hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0), HPow.hPow (β := ℤ) x (-(↑m : ℤ)) ≤ 1
⊢ x ^ (-m) ≤ 1

Tactic:
lift m to ℕ using by simpa using hn
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℕ
hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0
rw : 1 ≤ HPow.hPow (β := ℤ) x (↑m : ℤ)
⊢ HPow.hPow (β := ℤ) x (-(↑m : ℤ)) ≤ 1

Tactic:
rw [← ENNReal.inv_zpow', ENNReal.inv_zpow, ENNReal.inv_le_one]

Premises used: ENNReal.inv_zpow, ENNReal.inv_zpow', ENNReal.inv_le_one
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℕ
hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0
⊢ 1 ≤ HPow.hPow (β := ℤ) x (↑m : ℤ)

Tactic:
mod_cast one_le_pow₀ hx

Premises used: zpow_natCast, congrArg, cast, one_le_pow₀, LE.le, Nat.cast, HPow.hPow, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℕ
hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0
⊢ 1 ≤ HPow.hPow (β := ℤ) x (↑m : ℤ)

Tactic:
exact mod_cast one_le_pow₀ hx

Premises used: one_le_pow₀
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
    fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩

Premises used: ENNReal.mul_inv_cancel, Inv.inv, And.right, And.left, And.intro, Iff.intro, Units.mk, Exists.intro, IsUnit.ne_zero, ENNReal.inv_mul_cancel, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
refine : ∀ (ha : IsUnit a), a ≠ ∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
    fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : IsUnit a
obtain : ∀ (u : ℝ≥0∞ˣ), (↑u : ℝ≥0∞) ≠ ∞
⊢ a ≠ ∞

Tactic:
obtain ⟨u, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
u : ℝ≥0∞ˣ
hu : (↑u : ℝ≥0∞) = ∞
⊢ (↑u : ℝ≥0∞) * (↑u⁻¹ : ℝ≥0∞) = ∞ * (↑u⁻¹ : ℝ≥0∞)

Tactic:
have := congr($hu * u⁻¹)
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
u : ℝ≥0∞ˣ
hu : (↑u : ℝ≥0∞) = ∞
this : (↑u : ℝ≥0∞) * (↑u⁻¹ : ℝ≥0∞) = ∞ * (↑u⁻¹ : ℝ≥0∞)
⊢ False

Tactic:
simp at this
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : IsUnit a
⊢ ∀ {a_2 b : ℝ≥0∞},
    LE.le (α := ℝ≥0∞) ((ha.unit.mulLeft : (a : ℝ≥0∞) → ℝ≥0∞) a_2 : ℝ≥0∞)
        ((ha.unit.mulLeft : (a : ℝ≥0∞) → ℝ≥0∞) b : ℝ≥0∞) ↔
      a_2 ≤ b

Tactic:
simp [ENNReal.mul_le_mul_iff_right, ha.ne_zero, (isUnit_iff.1 ha).2]

Premises used: And.right, ENNReal.mul_le_mul_iff_right, Iff.mp, IsUnit.ne_zero, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : IsUnit a
⊢ ∀ {a_2 b : ℝ≥0∞},
    LE.le (α := ℝ≥0∞) ((ha.unit.mulRight : (a : ℝ≥0∞) → ℝ≥0∞) a_2 : ℝ≥0∞)
        ((ha.unit.mulRight : (a : ℝ≥0∞) → ℝ≥0∞) b : ℝ≥0∞) ↔
      a_2 ≤ b

Tactic:
simp [ENNReal.mul_le_mul_iff_left, ha.ne_zero, (isUnit_iff.1 ha).2]

Premises used: ENNReal.mul_le_mul_iff_left, And.right, Iff.mp, IsUnit.ne_zero, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
pos : ∀ (hf : ∀ (i : ι), f i = 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
neg : ∀ (hf : ¬∀ (i : ι), f i = 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
by_cases hf : ∀ i, f i = 0
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
simp [hf]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
neg : HMul.hMul (α := ℝ≥0∞) 0 (⨆ (i : ι), f i) = ⨆ (i : ι), 0 * f i
neg₁ : ∀ (ha₀ : a ≠ 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ HMul.hMul (α := ℝ≥0∞) 0 (⨆ (i : ι), f i) = ⨆ (i : ι), 0 * f i

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
neg : ∀ (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
neg₁ : ∀ (ha : a ≠ ∞), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
neg : ∀ (i : ι) (hi : ¬f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i

Tactic:
obtain ⟨i, hi⟩ := not_forall.1 hf

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : ¬f i = 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i

Tactic:
simpa [iSup_eq_zero.not.2 hf, eq_comm (a := ⊤)]
      using le_iSup_of_le (f := fun i => ⊤ * f i) i (top_mul hi).ge

Premises used: Iff.mpr, Eq.ge, Iff.not, eq_comm, ENNReal.top_mul, le_iSup_of_le, ENNReal.iSup_eq_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
(mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

Premises used: Iff.mpr, OrderIso.map_iSup, And.intro, ENNReal.mulLeftOrderIso, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

Premises used: Iff.mpr, OrderIso.map_iSup, And.intro, ENNReal.mulLeftOrderIso, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

Tactic:
simp [mul_comm, mul_iSup]

Premises used: mul_comm, ENNReal.mul_iSup
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
simp only [sSup_eq_iSup, mul_iSup]

Premises used: sSup_eq_iSup, ENNReal.mul_iSup