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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ (fun j ↦ ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε}) = fun x ↦ 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
;

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ (fun j ↦ ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε}) = fun x ↦ 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓝 a ⊓ 𝓟 s).NeBot
⊢ IsLUB s a

Tactic:
inf_comm

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case grind
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this✝ : Ioo a b = Icc a b
this : b ∈ Ioo a b
⊢ False

Tactic:
;

Goal state after:
case grind
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this✝ : Ioo a b = Icc a b
this : b ∈ Ioo a b
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
⊢ False

Tactic:
set s := { x ∈ Icc a b | Icc a x ∉ f }

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
⊢ ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
⊢ ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → a_1 ∈ {x}

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → a_1 ∈ {x}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)

Tactic:
;

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist

Tactic:
;

Goal state after:
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist

Tactic:
;

Goal state after:
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist

Tactic:
;

Goal state after:
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist

Tactic:
;

Goal state after:
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|

Tactic:
;

Goal state after:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: case h
r : ℝ
⊢ r ≤ |r|

Tactic:
;

Goal state after:
case h
r : ℝ
⊢ r ≤ |r|
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
⊢ f x ≤ f b

Tactic:
· rcases hxb.eq_or_lt with rfl | hxb
    · exact le_rfl
    simp only [ContinuousWithinAt] at h'x
    apply le_of_tendsto h'x
    have : s ∩ Iio b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Iio_mem_nhds hxb)
    filter_upwards [this] with y hy
    exact hf hy.1 hb (le_of_lt hy.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
let t := {c | ∃ x, ∃ y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ (x '' t).PairwiseDisjoint fun x ↦ Ioo x (y (f x))

pp: case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ ∀ x_1 ∈ x '' t, x_1 < y (f x_1)

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ (x '' t).PairwiseDisjoint fun x ↦ Ioo x (y (f x))

case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ ∀ x_1 ∈ x '' t, x_1 < y (f x_1)
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ ⋯.choose * b = c

Tactic:
exact (IsDedekindDomain.exists_add_spanSingleton_mul_eq hac ha hb).choose_spec

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

Goal state before:
pp: case inl
α : 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 = ∅
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

pp: case inr
α : 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
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
;

Goal state after:
case inl
α : 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 = ∅
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

case inr
α : 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
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
x' : β
hx' : x' ∈ K
⊢ f x' ≤ f x

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
x' : β
hx' : x' ∈ K
⊢ f x' ≤ f x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I)

Tactic:
inf_comm,

Goal state after:
case neg
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I)
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α✝
α : Type u_3
β : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : ProperSpace α
inst✝ : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall (x, y) r)

Tactic:
rw [← closedBall_prod_same x y]

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α✝
α : Type u_3
β : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : ProperSpace α
inst✝ : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝³ : FunLike 𝓕 E F
inst✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = dist (f x) (f y)

Tactic:
;

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝³ : FunLike 𝓕 E F
inst✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = dist (f x) (f y)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : 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]]
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
cases le_total (f a) (f b)

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.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ∩ ball x 1 ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ ball x 1)

Tactic:
aesop (add safe apply IsOpen.inter)

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ ∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s

Tactic:
intro r

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n

Tactic:
;

Goal state after:
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k) (𝓟 s ⊓ comap f (cobounded α))

Tactic:
inf_comm,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k) (comap f (cobounded α) ⊓ 𝓟 s)
Module: Mathlib.Topology.Instances.Int

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

Tactic:
;

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

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|

Tactic:
;

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|
Module: Mathlib.Topology.Instances.Int

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

Tactic:
;

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
⊢ cobounded α = cocompact α

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
⊢ cobounded α = cocompact α