mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 1 = spanSingleton R⁰ 1⁻¹ * ↑⊤

Tactic:
coeIdeal_top,

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
⊢ 1 = spanSingleton R⁰ 1⁻¹ * 1
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Icc x y = Icc ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ico x y = Ico ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ici x = Ico ↑x ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Ici x = Ico ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ioc x y = Ioc ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ioc x y = Ioc ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ioo x y = Ioo ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ioo x y = Ioo ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo ↑x ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Ioi x = Ioo ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iic x = Ioc ⊥ ↑x

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ ↑x

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Goal state after:
x : ℝ
⊢ WithBot.some '' WithTop.some '' Iio x = Ioo ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
simp_rw [← Ioi_inter_Iio]
  simp

Goal state after:
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 (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s

Tactic:
rcases hf ε ε₀ with ⟨i, hi, 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 : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
by
  apply le_trans (dist_triangle4 a f g h)
  gcongr
  apply le_trans (dist_triangle4 a d e f)
  gcongr
  exact dist_triangle4 a b c d

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ 0 ≤ dist x y + dist y z

Tactic:
· simpa using add_le_add (dist_nonneg : 0 ≤ dist x y) dist_nonneg

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

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo ((x + y) / 2 - (y - x) / 2) ((x + y) / 2 + (y - x) / 2)

Tactic:
← sub_div,

Goal state after:
x y : ℝ
⊢ Ioo x y = Ioo ((x + y - (y - x)) / 2) ((x + y) / 2 + (y - x) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = ball ((x + y) / 2) ((y - x) / 2)

Tactic:
rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

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

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc ((x + y) / 2 - (y - x) / 2) ((x + y) / 2 + (y - x) / 2)

Tactic:
← sub_div,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc ((x + y - (y - x)) / 2) ((x + y) / 2 + (y - x) / 2)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a

Tactic:
by
  rw [iSup_mul]
  exact ciSup_le' H

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: case pos
ι : Sort u_4
f : ι → ℕ
h : BddAbove (range f)
⊢ ∀ (c : ℝ≥0), ↑(⨆ i, f i) ≤ c ↔ ⨆ i, ↑(f i) ≤ c

Tactic:
simp [ciSup_le_iff', ← Nat.le_floor_iff, *]

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

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∃ᶠ (b : X × X) in 𝓤 X, ∃ a, (x, a) = b ∧ a ∈ iUnion U

Tactic:
hVb.frequently_iff

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∀ (i : ℕ), True → ∃ x_1 ∈ V i, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
by_cases hne : ∃ i, S i = ∅

Goal state after:
case pos
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

case neg
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by
  obtain ⟨y, hy⟩ := exists_lt x
  apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp
  simp_all

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩
  have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
  have huf (n : ℕ) : u n ∈ range f := (huxf n).2
  choose v hv using huf
  obtain rfl : f ∘ v = u := funext hv
  exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩

Goal state after:
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ᶜ
hx' : x < b
⊢ False

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ᶜ
hx' : a < x
⊢ False

Tactic:
· exact hx (hb hx'.le)

Goal state after:
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ᶜ
hx' : a < x
⊢ False
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
rsuffices ⟨R, R0, H⟩ : ∃ R > 0, ∀ n, dist (u n) (u N) < R

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ ball x ε

Tactic:
exact Metric.nhds_basis_ball

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ Submodule.map (↑I').subtype ⊤ ≤
    Submodule.map (↑I').subtype
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J')

Tactic:
Submodule.map_top,

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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ (↑I').subtype.range ≤
    Submodule.map (↑I').subtype
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J')
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑I' ≤ ↑J' ⊔ ↑I' ⊓ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑J' ≤ ↑I'

Tactic:
inf_eq_right.mpr

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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑I' ≤ ↑J' ⊔ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ≤ ↑I'

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
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑J' ≤ ↑I'
Module: Mathlib.Topology.Order.IntermediateValue

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

Tactic:
rw [inter_comm s t]

Goal state after:
case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp_rw [← not_ordConnected_inter_Icc_iff hx hy]
    exact fun hs ↦ h _ inter_subset_left hs _ ⟨hx, le_rfl, hxy.le⟩ _ ⟨hy, hxy.le, le_rfl⟩ hxy

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a - k) atTop = atTop

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a + -k) atTop = atTop
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
h : Nontrivial α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
obtain ⟨a, b, hab⟩ := exists_pair_lt α

Goal state after:
case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
h : Nontrivial α
a b : α
hab : a < b
⊢ StrictMono f ∨ StrictAnti f
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
by simp [Int.norm_eq_abs]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h✝ : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
⊢ g / a ^ k < a

Tactic:
simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt

Goal state after:
Module: Mathlib.Topology.UniformSpace.Real

Goal state before:
pp: ⊢ CompleteSpace ℝ

Tactic:
apply complete_of_cauchySeq_tendsto

Goal state after:
⊢ ∀ (u : ℕ → ℝ), CauchySeq u → ∃ a, Tendsto u atTop (nhds a)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_
  rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
  rcases exists_between hab' with ⟨c', hc'⟩
  rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩
  exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩

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

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

Tactic:
cases x with

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

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

Tactic:
{· simp_all}

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

Goal state before:
pp: case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t

Tactic:
lift x to ℝ using ⟨h1.ne_top, hx⟩

Goal state after:
case inr
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i ↦ f (i + k)) atTop = liminf f atTop

Tactic:
rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (max Kf Kg) (fun x ↦ (f x, g x)) s

Tactic:
intro _ hx _ hy

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y✝) ≤ ↑(max Kf Kg) * edist x✝ y✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
⊢ a = ⊥ ↔ a + ⊤ ≤ c

Tactic:
refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩

Goal state after:
case top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
⊢ a = ⊥
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b ↦ u b \ a) f

Tactic:
by
  simp only [limsup_eq_iInf_iSup, _root_.sdiff_eq]
  rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
by
  have h : ∀ᶠ n : ℕ in atTop, u n < x + ε := eventually_lt_add_pos_of_limsup_le hu_bdd hu hε
  simp only [eventually_atTop] at h
  obtain ⟨n, hn⟩ := h
  exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ≥0
h_le : ↑y ≤ x
⊢ ↑(x - ↑y) = ↑x - ↑↑y

Tactic:
cases x with

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (conditional β).filter.NeBot

Tactic:
conditional_filter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (Filter.map (fun p ↦ Finset.Icc p.1 p.2) (atBot ×ˢ atTop)).NeBot