mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case h₁
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i ≤ f _k

pp: case h₂
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ g j ≤ g _k

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i ≤ f _k

case h₂
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ g j ≤ g _k
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ {⊥, ⊤}ᶜ

pp: case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ {⊥, ⊤}ᶜ

pp: case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ {⊥, ⊤}ᶜ

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ {⊥, ⊤}ᶜ

case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ {⊥, ⊤}ᶜ

case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ {⊥, ⊤}ᶜ
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ Ioo ⊥ ⊤

pp: case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ Ioo ⊥ ⊤

pp: case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ Ioo ⊥ ⊤

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ Ioo ⊥ ⊤

case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ Ioo ⊥ ⊤

case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ Ioo ⊥ ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
⊢ ⊥.toReal = 0 ↔ ⊥ = 0 ∨ ⊥ = ⊤ ∨ ⊥ = ⊥

pp: case coe
a✝ : ℝ
⊢ (↑a✝).toReal = 0 ↔ ↑a✝ = 0 ∨ ↑a✝ = ⊤ ∨ ↑a✝ = ⊥

pp: case top
⊢ ⊤.toReal = 0 ↔ ⊤ = 0 ∨ ⊤ = ⊤ ∨ ⊤ = ⊥

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥.toReal = 0 ↔ ⊥ = 0 ∨ ⊥ = ⊤ ∨ ⊥ = ⊥

case coe
a✝ : ℝ
⊢ (↑a✝).toReal = 0 ↔ ↑a✝ = 0 ∨ ↑a✝ = ⊤ ∨ ↑a✝ = ⊥

case top
⊢ ⊤.toReal = 0 ↔ ⊤ = 0 ∨ ⊤ = ⊤ ∨ ⊤ = ⊥
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
y : ℝ≥0∞
⊢ ↑(∞ + y) = ↑∞ + ↑y

pp: case coe
y : ℝ≥0∞
x✝ : ℝ≥0
⊢ ↑(↑x✝ + y) = ↑↑x✝ + ↑y

Tactic:
<;>

Goal state after:
case top
y : ℝ≥0∞
⊢ ↑(∞ + y) = ↑∞ + ↑y

case coe
y : ℝ≥0∞
x✝ : ℝ≥0
⊢ ↑(↑x✝ + y) = ↑↑x✝ + ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top.top
⊢ ↑(∞ + ∞) = ↑∞ + ↑∞

pp: case top.coe
x✝ : ℝ≥0
⊢ ↑(∞ + ↑x✝) = ↑∞ + ↑↑x✝

pp: case coe.top
x✝ : ℝ≥0
⊢ ↑(↑x✝ + ∞) = ↑↑x✝ + ↑∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ↑(↑x✝¹ + ↑x✝) = ↑↑x✝¹ + ↑↑x✝

Tactic:
<;>

Goal state after:
case top.top
⊢ ↑(∞ + ∞) = ↑∞ + ↑∞

case top.coe
x✝ : ℝ≥0
⊢ ↑(∞ + ↑x✝) = ↑∞ + ↑↑x✝

case coe.top
x✝ : ℝ≥0
⊢ ↑(↑x✝ + ∞) = ↑↑x✝ + ↑∞

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ↑(↑x✝¹ + ↑x✝) = ↑↑x✝¹ + ↑↑x✝
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
⊢ ⊥.toENNReal = 0 ↔ ⊥ ≤ 0

pp: case coe
a✝ : ℝ
⊢ (↑a✝).toENNReal = 0 ↔ ↑a✝ ≤ 0

pp: case top
⊢ ⊤.toENNReal = 0 ↔ ⊤ ≤ 0

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥.toENNReal = 0 ↔ ⊥ ≤ 0

case coe
a✝ : ℝ
⊢ (↑a✝).toENNReal = 0 ↔ ↑a✝ ≤ 0

case top
⊢ ⊤.toENNReal = 0 ↔ ⊤ ≤ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊥
⊢ ⊥.toENNReal = y.toENNReal ↔ ⊥ = y

pp: case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝).toENNReal = y.toENNReal ↔ ↑a✝ = y

pp: case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ ⊤.toENNReal = y.toENNReal ↔ ⊤ = y

Tactic:
<;>

Goal state after:
case bot
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊥
⊢ ⊥.toENNReal = y.toENNReal ↔ ⊥ = y

case coe
y : EReal
hy : 0 ≤ y
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝).toENNReal = y.toENNReal ↔ ↑a✝ = y

case top
y : EReal
hy : 0 ≤ y
hx : 0 ≤ ⊤
⊢ ⊤.toENNReal = y.toENNReal ↔ ⊤ = y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot.bot
hx hy : 0 ≤ ⊥
⊢ ⊥.toENNReal = ⊥.toENNReal ↔ ⊥ = ⊥

pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊥.toENNReal = (↑a✝).toENNReal ↔ ⊥ = ↑a✝

pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ ⊥.toENNReal = ⊤.toENNReal ↔ ⊥ = ⊤

pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝).toENNReal = ⊥.toENNReal ↔ ↑a✝ = ⊥

pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹).toENNReal = (↑a✝).toENNReal ↔ ↑a✝¹ = ↑a✝

pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝).toENNReal = ⊤.toENNReal ↔ ↑a✝ = ⊤

pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ ⊤.toENNReal = ⊥.toENNReal ↔ ⊤ = ⊥

pp: case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊤.toENNReal = (↑a✝).toENNReal ↔ ⊤ = ↑a✝

pp: case top.top
hx hy : 0 ≤ ⊤
⊢ ⊤.toENNReal = ⊤.toENNReal ↔ ⊤ = ⊤

Tactic:
<;>

Goal state after:
case bot.bot
hx hy : 0 ≤ ⊥
⊢ ⊥.toENNReal = ⊥.toENNReal ↔ ⊥ = ⊥

case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊥.toENNReal = (↑a✝).toENNReal ↔ ⊥ = ↑a✝

case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ ⊥.toENNReal = ⊤.toENNReal ↔ ⊥ = ⊤

case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝).toENNReal = ⊥.toENNReal ↔ ↑a✝ = ⊥

case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹).toENNReal = (↑a✝).toENNReal ↔ ↑a✝¹ = ↑a✝

case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝).toENNReal = ⊤.toENNReal ↔ ↑a✝ = ⊤

case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ ⊤.toENNReal = ⊥.toENNReal ↔ ⊤ = ⊥

case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊤.toENNReal = (↑a✝).toENNReal ↔ ⊤ = ↑a✝

case top.top
hx hy : 0 ≤ ⊤
⊢ ⊤.toENNReal = ⊤.toENNReal ↔ ⊤ = ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : a = 0
⊢ a⁻¹⁻¹ = a

pp: case neg
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
<;>

Goal state after:
case pos
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : a = 0
⊢ a⁻¹⁻¹ = a

case neg
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : ¬a = 0
⊢ a⁻¹⁻¹ = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case pos.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

pp: case pos.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

pp: case neg.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ¬∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

pp: case neg.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ¬↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

Tactic:
<;>

Goal state after:
case pos.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case pos.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

case neg.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ¬∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case neg.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ¬↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case top.inl
c : ℝ≥0
h0 : ∞ ≠ 0 ∨ ↑c ≠ 0
ht : ∞ ≠ ∞ ∨ ↑c ≠ ∞
⊢ 0 = 0 ↔ 0 * ∞ ≤ ↑c

pp: case top.inr
a : ℝ≥0∞
c : ℝ≥0
h0 : ∞ ≠ 0 ∨ ↑c ≠ 0
ht : ∞ ≠ ∞ ∨ ↑c ≠ ∞
ha : a ≠ 0
⊢ a = 0 ↔ a * ∞ ≤ ↑c

Tactic:
<;>

Goal state after:
case top.inl
c : ℝ≥0
h0 : ∞ ≠ 0 ∨ ↑c ≠ 0
ht : ∞ ≠ ∞ ∨ ↑c ≠ ∞
⊢ 0 = 0 ↔ 0 * ∞ ≤ ↑c

case top.inr
a : ℝ≥0∞
c : ℝ≥0
h0 : ∞ ≠ 0 ∨ ↑c ≠ 0
ht : ∞ ≠ ∞ ∨ ↑c ≠ ∞
ha : a ≠ 0
⊢ a = 0 ↔ a * ∞ ≤ ↑c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_1
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0

pp: case refine_2
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ c ≠ ∞

Tactic:
<;>

Goal state after:
case refine_1
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0

case refine_2
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ c ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case h0
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ 1 ≠ 0

pp: case ht
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ 1 ≠ ∞

Tactic:
<;>

Goal state after:
case h0
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ 1 ≠ 0

case ht
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ 1 ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ℝ≥0∞ ≃o ↑(Iic 1)

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 ?_
  · simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]
  · have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
    simp only [inv_inv, tsub_add_cancel_of_le this]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ℝ≥0∞ ≃o ↑(Iic 1)

Tactic:
by
  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 ?_
  · simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]
  · have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
    simp only [inv_inv, tsub_add_cancel_of_le this]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case right
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b

Tactic:
← ENNReal.div_eq_inv_mul

Goal state after:
case right
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.zero
⊢ 0 ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞

pp: case ofNat.succ
n : ℕ
⊢ 0 ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞

pp: case negSucc
n : ℕ
⊢ 0 ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞

Tactic:
<;>

Goal state after:
case ofNat.zero
⊢ 0 ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞

case ofNat.succ
n : ℕ
⊢ 0 ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞

case negSucc
n : ℕ
⊢ 0 ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.zero
⊢ ∞ ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0

pp: case ofNat.succ
n : ℕ
⊢ ∞ ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0

pp: case negSucc
n : ℕ
⊢ ∞ ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0

Tactic:
<;>

Goal state after:
case ofNat.zero
⊢ ∞ ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0

case ofNat.succ
n : ℕ
⊢ ∞ ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0

case negSucc
n : ℕ
⊢ ∞ ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.ofNat a ≤ b
⊢ x ^ Int.ofNat a ≤ x ^ b

pp: case negSucc
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.negSucc a ≤ b
⊢ x ^ Int.negSucc a ≤ x ^ b

Tactic:
<;>

Goal state after:
case ofNat
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.ofNat a ≤ b
⊢ x ^ Int.ofNat a ≤ x ^ b

case negSucc
x : ℝ≥0∞
hx : 1 ≤ x
b : ℤ
a : ℕ
h : Int.negSucc a ≤ b
⊢ x ^ Int.negSucc a ≤ x ^ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc.ofNat.refine_1
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)

pp: case negSucc.ofNat.refine_2
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b

Tactic:
<;>

Goal state after:
case negSucc.ofNat.refine_1
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)

case negSucc.ofNat.refine_2
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
ContinuousAt,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inl.inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inl.inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
<;>

Goal state after:
case inl.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

case inl.inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

case inl.inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
ContinuousAt,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inr.inl.inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

pp: case inr.inl.inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
<;>

Goal state after:
case inr.inl.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

case inr.inl.inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

case inr.inl.inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x = ∞
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.ofNat a✝ = (x ^ Int.ofNat a✝)⁻¹

pp: case negSucc
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.negSucc a✝ = (x ^ Int.negSucc a✝)⁻¹

Tactic:
<;>

Goal state after:
case ofNat
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.ofNat a✝ = (x ^ Int.ofNat a✝)⁻¹

case negSucc
x : ℝ≥0∞
a✝ : ℕ
⊢ x⁻¹ ^ Int.negSucc a✝ = (x ^ Int.negSucc a✝)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∞ * f i < b

pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, f i < b

Tactic:
<;>

Goal state after:
case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∞ * f i < b

case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, f i < b
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ Function.swap dist = dist

Tactic:
funext x y

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s

pp: case mpr
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s

Tactic:
· rintro ⟨ε, ε₀, hε⟩
    rcases hf ε₀ with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩

Goal state after:
case mpr
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

pp: case mpr
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
<;>

Goal state after:
case mp
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

case mpr
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
ContinuousAt,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
ContinuousAt,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
by
  have : (ball x ε).Nonempty := by simp [hε]
  simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
⊢ TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩

Goal state after:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩

Goal state after:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ ↑(nndist x y) = 0 ↔ nndist x y = 0

Tactic:
ENNReal.coe_eq_zero

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ nndist x y = 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

pp: case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
<;>

Goal state after:
case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

pp: case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

pp: case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
<;>

Goal state after:
case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
simp [enorm, nnnorm_of_nonneg hr, ENNReal.ofReal, toNNReal, hr]

Goal state after: