mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Tactic:
replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx

Goal state after:
m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
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)⁻¹

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

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

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

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

Tactic:
simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

Goal state before:
pp: ι : Sort u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : ι → ℝ≥0∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ sphere x ε ∪ ball x ε = closedBall x ε

Tactic:
union_comm,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε ∪ sphere x ε = closedBall x ε
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

Tactic:
rintro ⟨ε, ε₀, hε⟩

Goal state after:
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 (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
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

Tactic:
rintro ⟨ε, ε₀, hε⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅

pp: case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sInf s

Tactic:
· rw [smul_set_empty, Real.sInf_empty, smul_zero]

Goal state after:
case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sInf s
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: a b : ℝ≥0
⊢ a ≤ b + nndist a b

Tactic:
by
  suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
    rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
  rw [← sub_le_iff_le_add']
  exact le_of_abs_le (dist_eq a b).ge

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
⊢ sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0

Tactic:
cases x

Goal state after:
case inr.inl.mk
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
fst✝ : α
snd✝ : β
⊢ sphere (fst✝, snd✝) 0 =
    sphere (fst✝, snd✝).1 0 ×ˢ closedBall (fst✝, snd✝).2 0 ∪ closedBall (fst✝, snd✝).1 0 ×ˢ sphere (fst✝, snd✝).2 0
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
intro h

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x ↦ x ∈ s) x
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inl
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : IsEmpty γ
⊢ sSup (range fun s ↦ f ↑s) = sSup (range fun i ↦ f i)

pp: case inr
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : Nonempty γ
⊢ sSup (range fun s ↦ f ↑s) = sSup (range fun i ↦ f i)

Tactic:
· simp [Set.range_eq_empty]

Goal state after:
case inr
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : Nonempty γ
⊢ sSup (range fun s ↦ f ↑s) = sSup (range fun i ↦ f i)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case refine_3
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense (t \ ({x | IsBot x} ∪ {x | IsTop x}))

pp: case refine_4
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsBot x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

pp: case refine_5
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsTop x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

Tactic:
· exact htd.sdiff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)

Goal state after:
case refine_4
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsBot x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

case refine_5
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsTop x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ (∀ (b : β), nndist (f b) (g b) ≤ r) →
    ((∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i))

Tactic:
intro h

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
⊢ (∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by simp [hd, edist_triangle]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by simp [hd, edist_triangle]

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z < f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)

Tactic:
refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
    exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ :=
      generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h

Goal state after:
case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s → ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
intro h

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ (∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε) → UniformCauchySeqOn F atTop s

Tactic:
intro h

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ UniformCauchySeqOn F atTop s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst✝²] (s ∩ Icc a y)
⊢ y ∈ s

Tactic:
exact IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx ↦
    hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ a ∈ s

Tactic:
suffices OrderDual.toDual a ∈ ofDual ⁻¹' s by aesop
  have : IsClosed (OrderDual.ofDual ⁻¹' (s ∩ Icc a b)) := hs
  rw [preimage_inter, ← Icc_toDual] at this
  apply this.mem_of_ge_of_forall_exists_gt (by simp_all) (by simp_all) (fun x hx ↦ ?_)
  rw [Ico_toDual, ← preimage_inter, ← Equiv.image_symm_eq_preimage, mem_image] at hx
  aesop

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
⊢ dist m n = ↑|m - n|

Tactic:
dist_eq

Goal state after:
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n

Tactic:
dist_eq

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

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

Goal state before:
pp: case mp
x : EReal
⊢ ⊤ + x = ⊤ → x ≠ ⊥

Tactic:
intro h

Goal state after:
case mp
x : EReal
h : ⊤ + x = ⊤
⊢ x ≠ ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case mpr
x : EReal
⊢ x ≠ ⊥ → ⊤ + x = ⊤

Tactic:
intro h

Goal state after:
case mpr
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal

Tactic:
induction x <;> induction y

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: α : 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 v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h with (h' | h') <;>
  · rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff]

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

Goal state before:
pp: x y : EReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Tactic:
induction x <;> induction y

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)

Tactic:
intro h

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
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
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:
intro h

Goal state after:
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
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
Module: Mathlib.Data.EReal.Operations

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

Tactic:
cases x

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.Data.EReal.Operations

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

Tactic:
cases x

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: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
⊢ -(x + y) = -x - y

Tactic:
induction x <;> induction y

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 : EReal
h : x ≠ ⊥
⊢ x - ⊥ = ⊤

Tactic:
cases x

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

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

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

Goal state before:
pp: x : EReal
hx : x ≠ ⊤
⊢ ⊤ - x = ⊤

Tactic:
cases x

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

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

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

Goal state before:
pp: x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
⊢ x - x = 0

Tactic:
cases x

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: x : EReal
⊢ x - x ≤ 0

Tactic:
cases x

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

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

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

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

Tactic:
cases x

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: x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
cases x

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: x y : EReal
⊢ 0 < x - y ↔ y < x

Tactic:
cases x

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: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y

Tactic:
cases x

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