α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ ((⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) =
    (⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}) ⊓ ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
simp only [nhds_eq_order, abs_lt, setOf_and, ← inf_principal, iInf_inf_eq]
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ (⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) = ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}

case refine_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ (⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) = ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ ((⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) =
    (⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}) ⊓ ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}
refine (congr_arg₂ _ ?_ ?_).trans inf_comm
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a x : α
⊢ (⨅ (_ : ↑(Equiv.subLeft a) x > 0), 𝓟 {a_1 | a - a_1 < ↑(Equiv.subLeft a) x}) = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ (⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) = ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}
refine (Equiv.subLeft a).iInf_congr fun x => ?_
no goals
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a x : α
⊢ (⨅ (_ : ↑(Equiv.subLeft a) x > 0), 𝓟 {a_1 | a - a_1 < ↑(Equiv.subLeft a) x}) = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)
simp [Ioi]
case refine_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a x : α
⊢ (⨅ (_ : ↑(Equiv.subRight a) x > 0), 𝓟 {a_1 | -↑(Equiv.subRight a) x < a - a_1}) = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)
case refine_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a : α
⊢ (⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) = ⨅ (x : α) (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}
refine (Equiv.subRight a).iInf_congr fun x => ?_
no goals
case refine_2
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
a x : α
⊢ (⨅ (_ : ↑(Equiv.subRight a) x > 0), 𝓟 {a_1 | -↑(Equiv.subRight a) x < a - a_1}) = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)
simp [Iio]