awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n : ℝ≥0∞)⁻¹ * a < b
⊢ ∃ n > 0, (↑n : ℝ≥0∞) * a < b
have h : GT.gt (α := ℝ≥0) (↑n : ℝ≥0)⁻¹ 0 ∧ (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) * a < b
Tactic: use (n : ℝ≥0)⁻¹
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
⊢ ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a
have rcases : ∀ (n : ℕ) (hn : (↑n : ℝ≥0∞)⁻¹ < a), ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a
Tactic: rcases exists_inv_nat_lt ha with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ ∃ (n : ℕ), HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < a
have refine : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < (↑n : ℝ≥0∞)⁻¹
Tactic: refine ⟨n, lt_trans ?_ hn⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < (↑n : ℝ≥0∞)⁻¹
have rw : (↑n : ℝ≥0∞) < HPow.hPow (α := ℝ≥0∞) 2 n
Tactic: rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n : ℝ≥0∞)⁻¹ < a
⊢ (↑n : ℝ≥0∞) < HPow.hPow (α := ℝ≥0∞) 2 n
have norm_cast : n < HPow.hPow (α := ℕ) 2 n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ (↑(r ^ n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ n
have ofNat : ∀ (n : ℕ), (↑(r ^ Int.ofNat n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.ofNat n
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℤ
ofNat : ∀ (n : ℕ), (↑(r ^ Int.ofNat n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.ofNat n
⊢ (↑(r ^ n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ n
have negSucc : ∀ (n : ℕ), (↑(r ^ Int.negSucc n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.negSucc n
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ (↑(r ^ Int.negSucc n) : ℝ≥0∞) = (↑r : ℝ≥0∞) ^ Int.negSucc n
have this : r ^ n.succ ≠ 0
Tactic: have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
n : ℤ
⊢ HPow.hPow (α := ℝ≥0∞) 0 n = if n = 0 then 1 else if 0 < n then 0 else ∞
have ofNat : HPow.hPow (α := ℝ≥0∞) 0 (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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 ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 n = if n = 0 then 1 else if 0 < n then 0 else ∞
have 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 ∞
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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 ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 n = if n = 0 then 1 else if 0 < n then 0 else ∞
have 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 ∞
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
n : ℤ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ n = if n = 0 then 1 else if 0 < n then ∞ else 0
have ofNat : HPow.hPow (α := ℝ≥0∞) ∞ (Int.ofNat 0) = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ n = if n = 0 then 1 else if 0 < n then ∞ else 0
have 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
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) ∞ n = if n = 0 then 1 else if 0 < n then ∞ else 0
have negSucc : ∀ (n : ℕ), HPow.hPow (α := ℝ≥0∞) ∞ (Int.negSucc n) = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0
Tactic: obtain ((_ | n) | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ 0 < a ^ n
have ofNat : ∀ (a_1 : ℕ), 0 < a ^ Int.ofNat a_1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
ofNat : ∀ (a_1 : ℕ), 0 < a ^ Int.ofNat a_1
⊢ 0 < a ^ n
have negSucc : ∀ (a_1 : ℕ), 0 < a ^ Int.negSucc a_1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ a ^ n < ∞
have ofNat : ∀ (a_1 : ℕ), a ^ Int.ofNat a_1 < ∞
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
ofNat : ∀ (a_1 : ℕ), a ^ Int.ofNat a_1 < ∞
⊢ a ^ n < ∞
have negSucc : ∀ (a_1 : ℕ), a ^ Int.negSucc a_1 < ∞
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico (y ^ n) (y ^ (n + 1))
Tactic: lift x to ℝ≥0 using h'x
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico (y ^ n) (y ^ (n + 1))
have lift : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
Tactic: lift y to ℝ≥0 using h'y
Cleared hypotheses: y, hy, h'y
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have A : y ≠ 0
Tactic: have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), y ^ n ≤ x ∧ x < y ^ (n + 1)
have refine : x ≠ 0
Tactic: refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have obtain : ∀ (n : ℤ) (hn : y ^ n ≤ x) (h'n : x < y ^ (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
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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))
have refine_1 : (↑y : ℝ≥0∞) ^ n ≤ (↑x : ℝ≥0∞)
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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∞)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ico ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have refine_2 : (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞) ^ (n + 1)
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)
⊢ (↑y : ℝ≥0∞) ^ n ≤ (↑x : ℝ≥0∞)
have refine_1 : (↑(y ^ n) : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)
⊢ (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞) ^ (n + 1)
have refine_2 : (↑x : ℝ≥0∞) < (↑(y ^ (n + 1)) : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ (n : ℤ), x ∈ Ioc (y ^ n) (y ^ (n + 1))
have lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc (y ^ n) (y ^ (n + 1))
Tactic: lift x to ℝ≥0 using h'x
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc (y ^ n) (y ^ (n + 1))
have lift : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
Tactic: lift y to ℝ≥0 using h'y
Cleared hypotheses: y, hy, h'y
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have A : y ≠ 0
Tactic: have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), y ^ n < x ∧ x ≤ y ^ (n + 1)
have refine : x ≠ 0
Tactic: refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
A : y ≠ 0
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have obtain : ∀ (n : ℤ) (hn : y ^ n < x) (h'n : x ≤ y ^ (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
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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))
have refine_1 : (↑y : ℝ≥0∞) ^ n < (↑x : ℝ≥0∞)
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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∞)
⊢ ∃ (n : ℤ), (↑x : ℝ≥0∞) ∈ Ioc ((↑y : ℝ≥0∞) ^ n) ((↑y : ℝ≥0∞) ^ (n + 1))
have refine_2 : (↑x : ℝ≥0∞) ≤ (↑y : ℝ≥0∞) ^ (n + 1)
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)
⊢ (↑y : ℝ≥0∞) ^ n < (↑x : ℝ≥0∞)
have refine_1 : (↑(y ^ n) : ℝ≥0∞) < (↑x : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)
⊢ (↑x : ℝ≥0∞) ≤ (↑y : ℝ≥0∞) ^ (n + 1)
have refine_2 : (↑x : ℝ≥0∞) ≤ (↑(y ^ (n + 1)) : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
⊢ Eq (α := Set ℝ≥0∞) (Ioo 0 ∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1)))
have h : ∀ (x : ℝ≥0∞),
  Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) x ↔ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) x ↔ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))) x
have h : 0 < x ∧ x < ∞ ↔ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
Tactic: simp only [mem_iUnion, mem_Ioo, mem_Ico]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ 0 < x ∧ x < ∞ ↔ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
have h : 0 < x ∧ x < ∞ → ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
h : 0 < x ∧ x < ∞ → ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
⊢ 0 < x ∧ x < ∞ ↔ ∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)
have h₁ : (∃ (i : ℤ), y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ∞
have h : 0 < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ 0 < x ∧ x < ∞
have h₁ : x < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x
have apply : 0 < y ^ n
Tactic: apply lt_of_lt_of_le _ hn
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞
have apply : y ^ (n + 1) < ∞
Tactic: apply lt_trans h'n _
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b
have ofNat : ∀ (a : ℕ) (h : Int.ofNat a ≤ b), x ^ Int.ofNat a ≤ x ^ b
Tactic: obtain a | a := a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
ofNat : ∀ (a : ℕ) (h : Int.ofNat a ≤ b), x ^ Int.ofNat a ≤ x ^ b
⊢ x ^ a ≤ x ^ b
have negSucc : ∀ (a : ℕ) (h : Int.negSucc a ≤ b), x ^ Int.negSucc a ≤ x ^ b
Tactic: obtain a | a := a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.ofNat a ≤ b
⊢ x ^ Int.ofNat a ≤ x ^ b
have ofNat : ∀ (b : ℕ) (h : Int.ofNat a ≤ Int.ofNat b), x ^ Int.ofNat a ≤ x ^ Int.ofNat b
Tactic: obtain b | b := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ x ^ Int.ofNat a ≤ x ^ b
have ofNat₁ : ∀ (b : ℕ) (h : Int.ofNat a ≤ Int.negSucc b), x ^ Int.ofNat a ≤ x ^ Int.negSucc b
Tactic: obtain b | b := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.negSucc a ≤ b
⊢ x ^ Int.negSucc a ≤ x ^ b
have negSucc : ∀ (b : ℕ) (h : Int.negSucc a ≤ Int.ofNat b), x ^ Int.negSucc a ≤ x ^ Int.ofNat b
Tactic: obtain b | b := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ x ^ Int.negSucc a ≤ x ^ b
have negSucc₁ : ∀ (b : ℕ) (h : Int.negSucc a ≤ Int.negSucc b), x ^ Int.negSucc a ≤ x ^ Int.negSucc b
Tactic: obtain b | b := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b
have ofNat : x ^ a ≤ x ^ b
Tactic: simp only [Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b
have apply : Int.negSucc b < Int.ofNat a
Tactic: apply absurd h (not_le_of_gt _)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b
have negSucc : (x ^ (a + 1))⁻¹ ≤ x ^ b
Tactic: simp only [zpow_negSucc, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b
have negSucc : 1 ≤ x ^ (a + 1)
Tactic: refine (ENNReal.inv_le_one.2 ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
negSucc : 1 ≤ x ^ (a + 1)
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b
have negSucc₁ : 1 ≤ x ^ b
Tactic: refine (ENNReal.inv_le_one.2 ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
have negSucc : x ^ (b + 1) ≤ x ^ (a + 1)
Tactic: simp only [zpow_negSucc, ENNReal.inv_le_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)
have negSucc : b + 1 ≤ a + 1
Tactic: apply pow_right_mono₀ hx
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n
have lift : ∀ (x : ℝ≥0) (hx : (↑x : ℝ≥0∞) ≠ 0), (↑x : ℝ≥0∞) ^ (m + n) = (↑x : ℝ≥0∞) ^ m * (↑x : ℝ≥0∞) ^ n
Tactic: lift x to ℝ≥0 using h'x
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
m n : ℤ
x : ℝ≥0
hx : (↑x : ℝ≥0∞) ≠ 0
⊢ (↑x : ℝ≥0∞) ^ (m + n) = (↑x : ℝ≥0∞) ^ m * (↑x : ℝ≥0∞) ^ n
have hx₁ : x ≠ 0
Tactic: replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
⊢ x ^ (-m) = (x ^ m)⁻¹
have inl : ∀ (hx₀ : x = 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hx₀ | hx₀ := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
inl : ∀ (hx₀ : x = 0), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr : ∀ (hx₀ : x ≠ 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hx₀ | hx₀ := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
⊢ x ^ (-m) = (x ^ m)⁻¹
have inl : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
inl : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inl₁ : ∀ (hm : m = 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
inl : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
inl₁ : ∀ (hm : m = 0), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inl₂ : ∀ (hm : 0 < m), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr : ∀ (hx : x = ∞), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hx | hx := eq_or_ne x ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
inr : ∀ (hx : x = ∞), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr₁ : ∀ (hx : x ≠ ∞), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hx | hx := eq_or_ne x ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
inr : ∀ (hm : m < 0), x ^ (-m) = (x ^ m)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr₁ : ∀ (hm : m = 0), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)⁻¹
⊢ x ^ (-m) = (x ^ m)⁻¹
have inr₂ : ∀ (hm : 0 < m), x ^ (-m) = (x ^ m)⁻¹
Tactic: obtain hm | hm | hm := lt_trichotomy m 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹
have rw : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
rw : x ^ (m + -n) = x ^ m * (x ^ n)⁻¹
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹
have rw₁ : x ^ m * x ^ (-n) = x ^ m * (x ^ n)⁻¹
Tactic: rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)⁻¹
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹
have rw₂ : x ^ m * (x ^ n)⁻¹ = x ^ m * (x ^ n)⁻¹
Tactic: rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
have ofNat : ∀ (a : ℕ), x⁻¹ ^ Int.ofNat a = (x ^ Int.ofNat a)⁻¹
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
n : ℤ
ofNat : ∀ (a : ℕ), x⁻¹ ^ Int.ofNat a = (x ^ Int.ofNat a)⁻¹
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
have negSucc : ∀ (a : ℕ), x⁻¹ ^ Int.negSucc a = (x ^ Int.negSucc a)⁻¹
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = x ^ (-n)
have rw : x⁻¹ ^ n = (x ^ n)⁻¹
Tactic: rw [ENNReal.zpow_neg, ENNReal.inv_zpow]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
n : ℤ
rw : x⁻¹ ^ n = (x ^ n)⁻¹
⊢ x⁻¹ ^ n = x ^ (-n)
have rw₁ : (x ^ n)⁻¹ = (x ^ n)⁻¹
Tactic: rw [ENNReal.zpow_neg, ENNReal.inv_zpow]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
n : ℤ
hn : n ≤ 0
x : ℝ≥0∞
hx : 1 ≤ x
⊢ x ^ n ≤ 1
have obtain : ∀ (m : ℤ) (hn : -m ≤ 0), x ^ (-m) ≤ 1
Tactic: obtain ⟨m, rfl⟩ := neg_surjective n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ x ^ (-m) ≤ 1
have lift : ∀ (m : ℕ) (hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0), HPow.hPow (β := ℤ) x (-(↑m : ℤ)) ≤ 1
Tactic: lift m to ℕ using by simpa using hn
Cleared hypotheses: m, hn
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℕ
hn : LE.le (α := ℤ) (-(↑m : ℤ)) 0
⊢ HPow.hPow (β := ℤ) x (-(↑m : ℤ)) ≤ 1
have rw : 1 ≤ HPow.hPow (β := ℤ) x (↑m : ℤ)
Tactic: rw [← ENNReal.inv_zpow', ENNReal.inv_zpow, ENNReal.inv_le_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞
have refine : ∀ (ha : IsUnit a), 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⟩⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
ha : IsUnit a
⊢ a ≠ ∞
have obtain : ∀ (u : ℝ≥0∞ˣ), (↑u : ℝ≥0∞) ≠ ∞
Tactic: obtain ⟨u, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
u : ℝ≥0∞ˣ
hu : (↑u : ℝ≥0∞) = ∞
⊢ False
have this : (↑u : ℝ≥0∞) * (↑u⁻¹ : ℝ≥0∞) = ∞ * (↑u⁻¹ : ℝ≥0∞)
Tactic: have := congr($hu * u⁻¹)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have pos : ∀ (hf : ∀ (i : ι), f i = 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
Tactic: by_cases hf : ∀ i, f i = 0