mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: ⊢ (Iio ∞).OrdConnected

Tactic:
]

Goal state after:
⊢ (Iio ∞).OrdConnected
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: ⊢ IsOpen (Iio ∞)

Tactic:
]

Goal state after:
⊢ IsOpen (Iio ∞)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝³] (⇑e ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝³] (⇑e ⁻¹' s)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Ioi (e.symm a))

Tactic:
]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Ioi (e.symm a))
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Iio (e.symm a))

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Iio (e.symm a))
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r

Tactic:
]

Goal state after:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ∅ = ∅

pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊

Tactic:
]

Goal state after:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r

Tactic:
]

Goal state after:
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊)

Tactic:
]

Goal state after:
x : ℕ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊)
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: r₁ r₂ : ℚ
⊢ |↑r₂ - ↑r₁| = |-↑r₁ + ↑r₂|

Tactic:
]

Goal state after:
r₁ r₂ : ℚ
⊢ |↑r₂ - ↑r₁| = |-↑r₁ + ↑r₂|
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
]

Goal state after:
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖

Tactic:
]

Goal state after:
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
]

Goal state after:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
]

Goal state after:
case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ s.sum ?m.36 = ∑ i ∈ s, ↑(f i).toNNReal

pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ?m.36 x

pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ α → ℝ≥0∞

pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ a ∈ s, f a ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ a ∈ s, f a ≠ ∞
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).toNNReal = ∑ a ∈ s, (f a).toReal

Tactic:
toNNReal_sum hf,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ↑(∑ a ∈ s, (f a).toNNReal) = ∑ a ∈ s, (f a).toReal
Module: Mathlib.Data.ENNReal.BigOperators

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

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ i ∈ s, ↑(f i).toNNReal = ∑ a ∈ s, (f a).toReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
]

Goal state after:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case mp
h : ⊥ = ⊤
⊢ False

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : EReal
⊢ x ≠ ⊥ ↔ x ≠ ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0

Tactic:
]

Goal state after:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ ↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) =
    min ↑(multiplicity p.asIdeal I) ↑(multiplicity p.asIdeal J)

Tactic:
]

Goal state after:
case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ ↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) =
    min ↑(multiplicity p.asIdeal I) ↑(multiplicity p.asIdeal J)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a) c

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a) c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (v a) c

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (v a) c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i ↦ F i a) ≤ s.sup' hs m

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i ↦ F i a) ≤ s.sup' hs m
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (F i a) c

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (F i a) c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i ↦ F i a) ≤ s.sup m

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i ↦ F i a) ≤ s.sup m
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mpr.inr
ι₁ : 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)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l')

Tactic:
]

Goal state after:
case mpr.inr
ι₁ : 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)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l')
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h_empty
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⊤

Tactic:
]

Goal state after:
case h_empty
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
]

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
]

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ -b ≤ a ↔ -b ≤ a

Tactic:
]

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

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
]

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ b ≤ -a ↔ b ≤ -a

Tactic:
]

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

Goal state before:
pp: a b : EReal
⊢ -b < a ↔ -b < a

Tactic:
]

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

Goal state before:
pp: a b : EReal
⊢ b < -a ↔ b < -a

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ (map u (f ⊓ 𝓟 {x | p x})).limsSup = (map u (f ⊓ 𝓟 {x | p x})).limsSup

Tactic:
]

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

Goal state before:
pp: a : EReal
⊢ 0 < a ↔ 0 < a

Tactic:
]

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

Goal state before:
pp: a : EReal
⊢ -a < 0 ↔ 0 < a

Tactic:
by rw [neg_lt_comm, neg_zero]

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

Goal state before:
pp: a : EReal
⊢ 0 ≤ a ↔ 0 ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup u (map v f) ≤ limsup u g

Tactic:
]

Goal state after:
ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup u (map v f) ≤ limsup u g
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
⊢ a < 0 ↔ a < 0

Tactic:
]

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

Goal state before:
pp: a : EReal
⊢ a ≤ 0 ↔ a ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ iSup u = ⨆ i, u i

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ iInf u = ⨅ i, u i

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f

Tactic:
]

Goal state after:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ (map f atTop).limsInf = (map f atTop).limsInf

Tactic:
]

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-a✝¹ - a✝) = ↑(-a✝¹ - a✝)

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -x + y = -x + y

pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥

Tactic:
]

Goal state after:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ iSup u = ⨆ i, u i

Tactic:
]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ iInf u = ⨅ i, u i

Tactic:
]

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

Goal state before:
pp: case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ min (emultiplicity p.asIdeal (I none)) (⨅ i, emultiplicity p.asIdeal (I (some i))) =
    min (emultiplicity p.asIdeal (I none)) (⨅ b, emultiplicity p.asIdeal (I (some b)))

Tactic:
]

Goal state after: