mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ b ≤ x

pp: case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ a

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ b ≤ x

case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ a
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
⊢ ∃ a < x, l < f a

Tactic:
simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using!
        exists_lt_of_lt_csSup (h.image _) hl

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
⊢ IsEmpty α → ∃ t, IsCompact t ∧ tᶜ ⊆ s

pp: case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
⊢ Nonempty α → ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
⊢ IsEmpty α → ∃ t, IsCompact t ∧ tᶜ ⊆ s

case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
⊢ Nonempty α → ∃ t, IsCompact t ∧ tᶜ ⊆ s
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
⊢ IsEmpty α → ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
⊢ Nonempty α → ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
⊢ IsEmpty α → ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
⊢ Nonempty α → ∃ t, IsCompact t ∧ tᶜ ⊆ x✝
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
<;>

Goal state after:
case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Tactic:
· obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
    exact ⟨a, has⟩

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

Goal state before:
pp: case inr
α : 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
⊢ ContinuousAt (fun x ↦ sSup (f x '' K)) x

Tactic:
ContinuousAt,

Goal state after:
case inr
α : 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
⊢ Tendsto (fun x ↦ sSup (f x '' K)) (𝓝 x) (𝓝 (sSup (f x '' K)))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])

case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: case inl
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : 0 ≤ n
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

pp: case inr
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : n ≤ 0
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
<;>

Goal state after:
case inl
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : 0 ≤ n
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

case inr
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
hn : n ≤ 0
⊢ ‖a ^ |n|‖ = ‖a ^ n‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖

pp: case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∉ s
⊢ ‖1⁻¹ * f x‖ = ‖1 / f x‖

pp: case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹‖ = ‖f x / 1‖

pp: case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∉ s
⊢ ‖1⁻¹‖ = ‖1 / 1‖

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖

case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∉ s
⊢ ‖1⁻¹ * f x‖ = ‖1 / f x‖

case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹‖ = ‖f x / 1‖

case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∉ s
⊢ ‖1⁻¹‖ = ‖1 / 1‖
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Injective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)

pp: case refine_4
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Surjective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)

Tactic:
· rw [← LinearMap.ker_eq_bot, Submodule.mapQ, Submodule.ker_liftQ,
      LinearMap.ker_comp, Submodule.ker_mkQ, ← Submodule.comap_comp,
      LinearMap.subtype_comp_restrict, ← le_bot_iff, Submodule.map_le_iff_le_comap,
      Submodule.comap_bot, Submodule.ker_mkQ, LinearMap.domRestrict,
      Submodule.comap_comp, ← Submodule.map_le_iff_le_comap,
      Submodule.map_comap_eq, Submodule.range_subtype]
    by_cases H' : I'.divMod I J' = 0
    · obtain rfl : J' = I' := by simpa [H'] using divMod_spec h' hJ' hI
      obtain rfl : I = J := mul_left_injective₀ hJ' (H.trans (mul_comm _ _))
      exact inf_le_left
    rw [← inv_mul_eq_iff_eq_mul₀ (by simpa [spanSingleton_eq_zero_iff] using H'), mul_inf₀
      (zero_le _), inv_mul_cancel_left₀ (by simpa [spanSingleton_eq_zero_iff] using H')] at this
    rw [← this, inf_comm, coe_inf]
    refine inf_le_inf ?_ le_rfl
    intro x hx
    rw [spanSingleton_inv]
    convert! mul_mem_mul (mem_spanSingleton_self _ _) hx
    simp [H']

Goal state after:
case refine_4
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Surjective
    ⇑((Submodule.comap (↑I).subtype ↑J).mapQ (Submodule.comap (↑I').subtype ↑J')
        (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ⋯)
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case none
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
⊢ ediam (⋃ i ∈ none, s i) = ⨆ i ∈ none, ediam (s i)

pp: case some
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
val✝ : ι
⊢ ediam (⋃ i ∈ some val✝, s i) = ⨆ i ∈ some val✝, ediam (s i)

Tactic:
<;>

Goal state after:
case none
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
⊢ ediam (⋃ i ∈ none, s i) = ⨆ i ∈ none, ediam (s i)

case some
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
val✝ : ι
⊢ ediam (⋃ i ∈ some val✝, s i) = ⨆ i ∈ some val✝, ediam (s i)
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

pp: case inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
<;>

Goal state after:
case inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

case inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
by
  have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t := fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
      _ ≤ ediam s + edist x y + ediam t := by
        gcongr
        exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]
  refine ediam_le fun a ha b hb => ?_
  rw [mem_union] at ha hb
  rcases ha with h'a | h'a <;> rcases hb with h'b | h'b
  · calc
      edist a b ≤ ediam s := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + (edist x y + ediam t) := le_self_add
      _ = ediam s + edist x y + ediam t := (add_assoc _ _ _).symm
  · exact A a h'a b h'b
  · have Z := A b h'b a h'a
    rwa [edist_comm] at Z
  · calc
      edist a b ≤ ediam t := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + edist x y + ediam t := le_add_self

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : EMetricSpace X
⊢ 0 < ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Tactic:
simp only [ediam_pos_iff, Set.Nontrivial]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
have xyab : Icc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2
  by_contra hst
  suffices Icc x y ⊆ s from
    hst ⟨y, xyab <| right_mem_Icc.2 hxy, this <| right_mem_Icc.2 hxy, hy.2⟩
  apply (IsClosed.inter hs isClosed_Icc).Icc_subset_of_forall_mem_nhdsWithin hx.2
  rintro z ⟨zs, hz⟩
  have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩
  have : tᶜ ∩ Ioc z y ∈ 𝓝[>] z := by
    rw [← nhdsWithin_Ioc_eq_nhdsGT hz.2]
    exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
  apply mem_of_superset this
  have : Ioc z y ⊆ s ∪ t := fun w hw => hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩)
  exact fun w ⟨wt, wzy⟩ => (this wzy).elim id fun h => (wt h).elim

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

Goal state before:
pp: case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h✝ : f a ≤ f b
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

pp: case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h✝ : f b ≤ f a
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h✝ : f a ≤ f b
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h✝ : f b ≤ f a
⊢ [[f a, f b]] ⊆ f '' [[a, b]]
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f a ≤ f b
⊢ SurjOn f s [[f a, f b]]

pp: case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f b ≤ f a
⊢ SurjOn f s [[f a, f b]]

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f a ≤ f b
⊢ SurjOn f s [[f a, f b]]

case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
hab : f b ≤ f a
⊢ SurjOn f s [[f a, f b]]
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∃ j, (x ∈ j ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] j) ∧ Bornology.IsBounded j ∧ j ⊆ s

Tactic:
exact ⟨s ∩ Metric.ball x 1,
    by aesop (add safe apply IsOpen.inter),
    by simpa using Metric.isBounded_ball.subset Set.inter_subset_right⟩

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]

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

Goal state before:
pp: case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x y ≠ ∞

pp: case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x z ≠ ∞

pp: case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

pp: case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞

Tactic:
<;>

Goal state after:
case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x y ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x z ≠ ∞

case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: case inl
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ ↑n‖ ≤ ‖↑n‖ * ‖a‖

pp: case inr
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ (-↑n)‖ ≤ ‖-↑n‖ * ‖a‖

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ ↑n‖ ≤ ‖↑n‖ * ‖a‖

case inr
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ (-↑n)‖ ≤ ‖-↑n‖ * ‖a‖
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ ¬ediam univ ≠ ∞

Tactic:
Classical.not_not

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ ediam univ = ∞
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: case inl
r : ℝ
hr : 0 ≤ r
⊢ BddAbove (closedBall 0 r)

pp: case inr
r : ℝ
hr : r < 0
⊢ BddAbove (closedBall 0 r)

Tactic:
<;>

Goal state after:
case inl
r : ℝ
hr : 0 ≤ r
⊢ BddAbove (closedBall 0 r)

case inr
r : ℝ
hr : r < 0
⊢ BddAbove (closedBall 0 r)
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

Tactic:
by
  rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
  rfl

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

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

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

Tactic:
<;>

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

case mpr
x : EReal
⊢ x ≠ ⊥ → ⊤ + x = ⊤
Module: Mathlib.Data.EReal.Operations

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

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

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

Tactic:
<;>

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

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

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