mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
H :
  ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄,
    ∀ a ∈ s,
      [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ →
        ∀ b ∈ t, [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ → a ≤ b → x ∈ ⊥
hab : ¬a ≤ b
⊢ x ∈ ⊥

pp: α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
⊢ x ∈ ⊥

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
H :
  ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄,
    ∀ a ∈ s,
      [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ →
        ∀ b ∈ t, [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ → a ≤ b → x ∈ ⊥
hab : ¬a ≤ b
⊢ x ∈ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hxa : x ≤ a
⊢ x ∈ ⊥

pp: case inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
⊢ x ∈ ⊥

Tactic:
·

Goal state after:
case inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hxa : x ≤ a
⊢ x ∈ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥

pp: case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥

Tactic:
·

Goal state after:
case inr.inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case pos
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mp
a b : ℝ≥0∞
⊢ a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

pp: case mpr
a b : ℝ≥0∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞

Tactic:
·

Goal state after:
case mp
a b : ℝ≥0∞
⊢ a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mpr
a b : ℝ≥0∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞

Tactic:
·

Goal state after:
case mpr
a b : ℝ≥0∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ⊢ 0 < ∞

Tactic:
exact zero_lt_top

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

Goal state before:
pp: case pos
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : c = ∞
⊢ a - b + c = a + c - b

pp: case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + c = a + c - b

Tactic:
·

Goal state after:
case pos
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : c = ∞
⊢ a - b + c = a + c - b
Module: Mathlib.Data.ENNReal.Operations

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

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

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

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

Tactic:
·

Goal state after:
case top.top
c : ℝ≥0
⊢ ∞ + ↑c - (∞ + ↑c) = ∞ - ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top.coe
c x✝ : ℝ≥0
⊢ ∞ + ↑c - (↑x✝ + ↑c) = ∞ - ↑x✝

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

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

Tactic:
·

Goal state after:
case top.coe
c x✝ : ℝ≥0
⊢ ∞ + ↑c - (↑x✝ + ↑c) = ∞ - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

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

Tactic:
·

Goal state after:
case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝

Tactic:
·

Goal state after:
case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a < ∞ + c

pp: case inr
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
·

Goal state after:
case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a < ∞ + c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
·

Goal state after:
case inr
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

pp: case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c

Tactic:
·

Goal state after:
case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ∞
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

pp: case inr.inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Tactic:
·

Goal state after:
case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ∞
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top
b : ℝ≥0
⊢ ∞.toReal - (↑b).toReal ≤ (∞ - ↑b).toReal

pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
·

Goal state after:
case top
b : ℝ≥0
⊢ ∞.toReal - (↑b).toReal ≤ (∞ - ↑b).toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
·

Goal state after:
case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

pp: case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
·

Goal state after:
case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a

pp: case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top
a b : ℝ≥0
h : ↑b ≤ ↑a
⊢ ↑a - ∞ - (↑a - ↑b) = ↑b - ∞

pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ ↑a - ↑x✝ - (↑a - ↑b) = ↑b - ↑x✝

Tactic:
·

Goal state after:
case top
a b : ℝ≥0
h : ↑b ≤ ↑a
⊢ ↑a - ∞ - (↑a - ↑b) = ↑b - ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ ↑a - ↑x✝ - (↑a - ↑b) = ↑b - ↑x✝

Tactic:
·

Goal state after:
case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ ↑a - ↑x✝ - (↑a - ↑b) = ↑b - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩

Goal state after:
case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

pp: case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ¬∃ i, f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ∞ ≤ ENNReal.ofReal (⨅ i, f i) ↔ ∞ ≤ ⨅ i, ENNReal.ofReal (f i)

pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
·

Goal state after:
case inr.inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ∞ ≤ ENNReal.ofReal (⨅ i, f i) ↔ ∞ ≤ ⨅ i, ENNReal.ofReal (f i)
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure[instTopologicalSpace] (⇑ofDual ⁻¹' t))
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i

Tactic:
·

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i

Tactic:
·

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {choose ⋯}) ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (choose ⋯) ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {choose ⋯}) ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (choose ⋯) ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (choose ⋯) ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {a}) ≠ 0