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

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

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

pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal

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

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

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

pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

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

pp: case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
<;>

Goal state after:
case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal

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

case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal

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

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

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

case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

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

case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ b ≤ c

Tactic:
apply hb c

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ b ≤ c

Tactic:
apply hb c

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ (⊥ + y).toENNReal ≤ ⊥.toENNReal + y.toENNReal

pp: case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).toENNReal ≤ (↑a✝).toENNReal + y.toENNReal

pp: case top
y : EReal
⊢ (⊤ + y).toENNReal ≤ ⊤.toENNReal + y.toENNReal

Tactic:
<;>

Goal state after:
case bot
y : EReal
⊢ (⊥ + y).toENNReal ≤ ⊥.toENNReal + y.toENNReal

case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).toENNReal ≤ (↑a✝).toENNReal + y.toENNReal

case top
y : EReal
⊢ (⊤ + y).toENNReal ≤ ⊤.toENNReal + y.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

pp: case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

pp: case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

pp: case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
<;>

Goal state after:
case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)

pp: case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)

Tactic:
<;>

Goal state after:
case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)

case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hy : y ≠ ⊥
hx : ⊥ ≠ ⊥
⊢ ⊥ + y ≠ ⊤ → ⊥ ≠ ⊤ ∧ y ≠ ⊤

pp: case coe
y : EReal
hy : y ≠ ⊥
a✝ : ℝ
hx : ↑a✝ ≠ ⊥
⊢ ↑a✝ + y ≠ ⊤ → ↑a✝ ≠ ⊤ ∧ y ≠ ⊤

pp: case top
y : EReal
hy : y ≠ ⊥
hx : ⊤ ≠ ⊥
⊢ ⊤ + y ≠ ⊤ → ⊤ ≠ ⊤ ∧ y ≠ ⊤

Tactic:
<;>

Goal state after:
case bot
y : EReal
hy : y ≠ ⊥
hx : ⊥ ≠ ⊥
⊢ ⊥ + y ≠ ⊤ → ⊥ ≠ ⊤ ∧ y ≠ ⊤

case coe
y : EReal
hy : y ≠ ⊥
a✝ : ℝ
hx : ↑a✝ ≠ ⊥
⊢ ↑a✝ + y ≠ ⊤ → ↑a✝ ≠ ⊤ ∧ y ≠ ⊤

case top
y : EReal
hy : y ≠ ⊥
hx : ⊤ ≠ ⊥
⊢ ⊤ + y ≠ ⊤ → ⊤ ≠ ⊤ ∧ y ≠ ⊤
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊥ = ⊥
⊢ ¬↑a✝ + ⊥ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊥ = ⊤

pp: case coe.coe
a✝¹ : ℝ
hx : ¬↑a✝¹ = ⊥
a✝ : ℝ
hy : ¬↑a✝ = ⊥
⊢ ¬↑a✝¹ + ↑a✝ = ⊤ → ¬↑a✝¹ = ⊤ ∧ ¬↑a✝ = ⊤

pp: case coe.top
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊤ = ⊥
⊢ ¬↑a✝ + ⊤ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊤ = ⊤

Tactic:
<;>

Goal state after:
case coe.bot
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊥ = ⊥
⊢ ¬↑a✝ + ⊥ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊥ = ⊤

case coe.coe
a✝¹ : ℝ
hx : ¬↑a✝¹ = ⊥
a✝ : ℝ
hy : ¬↑a✝ = ⊥
⊢ ¬↑a✝¹ + ↑a✝ = ⊤ → ¬↑a✝¹ = ⊤ ∧ ¬↑a✝ = ⊤

case coe.top
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊤ = ⊥
⊢ ¬↑a✝ + ⊤ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ ⊥ ≠ ⊤

pp: case coe
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a✝ : ℝ
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤

pp: case top
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤

Tactic:
<;>

Goal state after:
case bot
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ ⊥ ≠ ⊤

case coe
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a✝ : ℝ
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤

case top
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
h1 : ⊥ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊥ + y) = -⊥ - y

pp: case coe
y : EReal
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ y ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(↑a✝ + y) = -↑a✝ - y

pp: case top
y : EReal
h1 : ⊤ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊤ + y) = -⊤ - y

Tactic:
<;>

Goal state after:
case bot
y : EReal
h1 : ⊥ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊥ + y) = -⊥ - y

case coe
y : EReal
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ y ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(↑a✝ + y) = -↑a✝ - y

case top
y : EReal
h1 : ⊤ ≠ ⊥ ∨ y ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ y ≠ ⊥
⊢ -(⊤ + y) = -⊤ - y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h1 : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊥ + ⊥) = -⊥ - ⊥

pp: case bot.coe
a✝ : ℝ
h1 : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊥ + ↑a✝) = -⊥ - ↑a✝

pp: case bot.top
h1 : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊥ + ⊤) = -⊥ - ⊤

pp: case coe.bot
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(↑a✝ + ⊥) = -↑a✝ - ⊥

pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

pp: case coe.top
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(↑a✝ + ⊤) = -↑a✝ - ⊤

pp: case top.bot
h1 : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊤ + ⊥) = -⊤ - ⊥

pp: case top.coe
a✝ : ℝ
h1 : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊤ + ↑a✝) = -⊤ - ↑a✝

pp: case top.top
h1 : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊤ + ⊤) = -⊤ - ⊤

Tactic:
<;>

Goal state after:
case bot.bot
h1 : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊥ + ⊥) = -⊥ - ⊥

case bot.coe
a✝ : ℝ
h1 : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊥ + ↑a✝) = -⊥ - ↑a✝

case bot.top
h1 : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊥ + ⊤) = -⊥ - ⊤

case coe.bot
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(↑a✝ + ⊥) = -↑a✝ - ⊥

case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

case coe.top
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(↑a✝ + ⊤) = -↑a✝ - ⊤

case top.bot
h1 : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊤ + ⊥) = -⊤ - ⊥

case top.coe
a✝ : ℝ
h1 : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊤ + ↑a✝) = -⊤ - ↑a✝

case top.top
h1 : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊤ + ⊤) = -⊤ - ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥

Tactic:
<;>

Goal state after:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨅ (_ : True), sSup (u '' Ici i) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
by simp only [sSup_image, iInf_const]; rfl

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ (𝓟 (range u)).limsInf = ⨅ i, u i

Tactic:
limsInf_principal_eq_sInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ sInf (range u) = ⨅ i, u i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
h : ⊥ ≠ ⊥
⊢ ⊥ - ⊥ = ⊤

pp: case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ↑a✝ - ⊥ = ⊤

pp: case top
h : ⊤ ≠ ⊥
⊢ ⊤ - ⊥ = ⊤

Tactic:
<;>

Goal state after:
case bot
h : ⊥ ≠ ⊥
⊢ ⊥ - ⊥ = ⊤

case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ↑a✝ - ⊥ = ⊤

case top
h : ⊤ ≠ ⊥
⊢ ⊤ - ⊥ = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : ι → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
by
  induction ι using Finite.induction_empty_option with
  | h_empty =>
    rw [iSup_of_empty, iInf_of_empty]
    exact emultiplicity_zero _
  | of_equiv e ih =>
    specialize ih (I ∘ e)
    rw [← sSup_range, ← sInf_range] at ih ⊢
    rw [EquivLike.range_comp I e] at ih
    rw [ih]
    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
  | h_option ih =>
    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
hx : ⊥ ≠ ⊤
⊢ ⊤ - ⊥ = ⊤

pp: case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤
⊢ ⊤ - ↑a✝ = ⊤

pp: case top
hx : ⊤ ≠ ⊤
⊢ ⊤ - ⊤ = ⊤

Tactic:
<;>

Goal state after:
case bot
hx : ⊥ ≠ ⊤
⊢ ⊤ - ⊥ = ⊤

case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤
⊢ ⊤ - ↑a✝ = ⊤

case top
hx : ⊤ ≠ ⊤
⊢ ⊤ - ⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
h_top : ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥
⊢ ⊥ - ⊥ = 0

pp: case coe
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥
⊢ ↑a✝ - ↑a✝ = 0

pp: case top
h_top : ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥
⊢ ⊤ - ⊤ = 0

Tactic:
<;>

Goal state after:
case bot
h_top : ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥
⊢ ⊥ - ⊥ = 0

case coe
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥
⊢ ↑a✝ - ↑a✝ = 0

case top
h_top : ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥
⊢ ⊤ - ⊤ = 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
⊢ ⊥ - ⊥ ≤ 0

pp: case coe
a✝ : ℝ
⊢ ↑a✝ - ↑a✝ ≤ 0

pp: case top
⊢ ⊤ - ⊤ ≤ 0

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥ - ⊥ ≤ 0

case coe
a✝ : ℝ
⊢ ↑a✝ - ↑a✝ ≤ 0

case top
⊢ ⊤ - ⊤ ≤ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥

pp: case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ↑a✝ - y ↔ y ≤ ↑a✝

pp: case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤

Tactic:
<;>

Goal state after:
case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥

case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ↑a✝ - y ↔ y ≤ ↑a✝

case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊥ ↔ ⊥ ≤ ⊥

pp: case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊥ - ↑a✝ ↔ ↑a✝ ≤ ⊥

pp: case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊤ ↔ ⊤ ≤ ⊥

pp: case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊥ ↔ ⊥ ≤ ↑a✝

pp: case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ↑a✝¹ - ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

pp: case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊤ ↔ ⊤ ≤ ↑a✝

pp: case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊥ ↔ ⊥ ≤ ⊤

pp: case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊤ - ↑a✝ ↔ ↑a✝ ≤ ⊤

pp: case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊤ ↔ ⊤ ≤ ⊤

Tactic:
<;>

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊥ - ↑a✝ ↔ ↑a✝ ≤ ⊥

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊤ ↔ ⊤ ≤ ⊥

case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ↑a✝¹ - ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊤ ↔ ⊤ ≤ ↑a✝

case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊥ ↔ ⊥ ≤ ⊤

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊤ - ↑a✝ ↔ ↑a✝ ≤ ⊤

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊤ ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y

pp: case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ - y ≤ 0 ↔ ↑a✝ ≤ y

pp: case top
y : EReal
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y

Tactic:
<;>

Goal state after:
case bot
y : EReal
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y

case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ - y ≤ 0 ↔ ↑a✝ ≤ y

case top
y : EReal
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y
Module: Mathlib.Data.EReal.Operations

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

pp: case bot.coe
a✝ : ℝ
⊢ ⊥ - ↑a✝ ≤ 0 ↔ ⊥ ≤ ↑a✝

pp: case bot.top
⊢ ⊥ - ⊤ ≤ 0 ↔ ⊥ ≤ ⊤

pp: case coe.bot
a✝ : ℝ
⊢ ↑a✝ - ⊥ ≤ 0 ↔ ↑a✝ ≤ ⊥

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ - ↑a✝ ≤ 0 ↔ ↑a✝¹ ≤ ↑a✝

pp: case coe.top
a✝ : ℝ
⊢ ↑a✝ - ⊤ ≤ 0 ↔ ↑a✝ ≤ ⊤

pp: case top.bot
⊢ ⊤ - ⊥ ≤ 0 ↔ ⊤ ≤ ⊥

pp: case top.coe
a✝ : ℝ
⊢ ⊤ - ↑a✝ ≤ 0 ↔ ⊤ ≤ ↑a✝

pp: case top.top
⊢ ⊤ - ⊤ ≤ 0 ↔ ⊤ ≤ ⊤

Tactic:
<;>

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

case bot.coe
a✝ : ℝ
⊢ ⊥ - ↑a✝ ≤ 0 ↔ ⊥ ≤ ↑a✝

case bot.top
⊢ ⊥ - ⊤ ≤ 0 ↔ ⊥ ≤ ⊤

case coe.bot
a✝ : ℝ
⊢ ↑a✝ - ⊥ ≤ 0 ↔ ↑a✝ ≤ ⊥

case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ - ↑a✝ ≤ 0 ↔ ↑a✝¹ ≤ ↑a✝

case coe.top
a✝ : ℝ
⊢ ↑a✝ - ⊤ ≤ 0 ↔ ↑a✝ ≤ ⊤

case top.bot
⊢ ⊤ - ⊥ ≤ 0 ↔ ⊤ ≤ ⊥

case top.coe
a✝ : ℝ
⊢ ⊤ - ↑a✝ ≤ 0 ↔ ⊤ ≤ ↑a✝

case top.top
⊢ ⊤ - ⊤ ≤ 0 ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ 0 < ⊥ - y ↔ y < ⊥

pp: case coe
y : EReal
a✝ : ℝ
⊢ 0 < ↑a✝ - y ↔ y < ↑a✝

pp: case top
y : EReal
⊢ 0 < ⊤ - y ↔ y < ⊤

Tactic:
<;>

Goal state after:
case bot
y : EReal
⊢ 0 < ⊥ - y ↔ y < ⊥

case coe
y : EReal
a✝ : ℝ
⊢ 0 < ↑a✝ - y ↔ y < ↑a✝

case top
y : EReal
⊢ 0 < ⊤ - y ↔ y < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
⊢ 0 < ⊥ - ⊥ ↔ ⊥ < ⊥

pp: case bot.coe
a✝ : ℝ
⊢ 0 < ⊥ - ↑a✝ ↔ ↑a✝ < ⊥

pp: case bot.top
⊢ 0 < ⊥ - ⊤ ↔ ⊤ < ⊥

pp: case coe.bot
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊥ ↔ ⊥ < ↑a✝

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ 0 < ↑a✝¹ - ↑a✝ ↔ ↑a✝ < ↑a✝¹

pp: case coe.top
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊤ ↔ ⊤ < ↑a✝

pp: case top.bot
⊢ 0 < ⊤ - ⊥ ↔ ⊥ < ⊤

pp: case top.coe
a✝ : ℝ
⊢ 0 < ⊤ - ↑a✝ ↔ ↑a✝ < ⊤

pp: case top.top
⊢ 0 < ⊤ - ⊤ ↔ ⊤ < ⊤

Tactic:
<;>

Goal state after:
case bot.bot
⊢ 0 < ⊥ - ⊥ ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
⊢ 0 < ⊥ - ↑a✝ ↔ ↑a✝ < ⊥

case bot.top
⊢ 0 < ⊥ - ⊤ ↔ ⊤ < ⊥

case coe.bot
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊥ ↔ ⊥ < ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
⊢ 0 < ↑a✝¹ - ↑a✝ ↔ ↑a✝ < ↑a✝¹

case coe.top
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊤ ↔ ⊤ < ↑a✝

case top.bot
⊢ 0 < ⊤ - ⊥ ↔ ⊥ < ⊤

case top.coe
a✝ : ℝ
⊢ 0 < ⊤ - ↑a✝ ↔ ↑a✝ < ⊤

case top.top
⊢ 0 < ⊤ - ⊤ ↔ ⊤ < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊥ - y < 0 ↔ ⊥ < y

pp: case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ ↑a✝ - y < 0 ↔ ↑a✝ < y

pp: case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊤ - y < 0 ↔ ⊤ < y

Tactic:
<;>

Goal state after:
case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊥ - y < 0 ↔ ⊥ < y

case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ ↑a✝ - y < 0 ↔ ↑a✝ < y

case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ ⊤ - y < 0 ↔ ⊤ < y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊥ - ⊥ < 0 ↔ ⊥ < ⊥

pp: case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊥ - ↑a✝ < 0 ↔ ⊥ < ↑a✝

pp: case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊥ - ⊤ < 0 ↔ ⊥ < ⊤

pp: case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ↑a✝ - ⊥ < 0 ↔ ↑a✝ < ⊥

pp: case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ↑a✝¹ - ↑a✝ < 0 ↔ ↑a✝¹ < ↑a✝

pp: case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ↑a✝ - ⊤ < 0 ↔ ↑a✝ < ⊤

pp: case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊤ - ⊥ < 0 ↔ ⊤ < ⊥

pp: case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊤ - ↑a✝ < 0 ↔ ⊤ < ↑a✝

pp: case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊤ - ⊤ < 0 ↔ ⊤ < ⊤

Tactic:
<;>

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊥ - ⊥ < 0 ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊥ - ↑a✝ < 0 ↔ ⊥ < ↑a✝

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊥ - ⊤ < 0 ↔ ⊥ < ⊤

case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ↑a✝ - ⊥ < 0 ↔ ↑a✝ < ⊥

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ↑a✝¹ - ↑a✝ < 0 ↔ ↑a✝¹ < ↑a✝

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ↑a✝ - ⊤ < 0 ↔ ↑a✝ < ⊤

case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊤ - ⊥ < 0 ↔ ⊤ < ⊥

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊤ - ↑a✝ < 0 ↔ ⊤ < ↑a✝

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊤ - ⊤ < 0 ↔ ⊤ < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hy : 0 ≤ y
⊢ (⊥ - y).toENNReal = ⊥.toENNReal - y.toENNReal

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

pp: case top
y : EReal
hy : 0 ≤ y
⊢ (⊤ - y).toENNReal = ⊤.toENNReal - y.toENNReal

Tactic:
<;>

Goal state after:
case bot
y : EReal
hy : 0 ≤ y
⊢ (⊥ - y).toENNReal = ⊥.toENNReal - y.toENNReal

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

case top
y : EReal
hy : 0 ≤ y
⊢ (⊤ - y).toENNReal = ⊤.toENNReal - y.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal

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

pp: case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal

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

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

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

pp: case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

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

pp: case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal

Tactic:
<;>

Goal state after:
case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal

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

case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal

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

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

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

case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

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

case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal