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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
constructor

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

case mpr
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | dist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
  constructor
  · rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_ofPred.2 hx.le)⟩

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

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
constructor

Goal state after:
case mp
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

case mpr
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
    ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ m.replaceUniformity H = m

Tactic:
ext

Goal state after:
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = toUniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m

Tactic:
ext

Goal state after:
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = toUniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m

Tactic:
ext

Goal state after:
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: r : ℝ
⊢ closedBall 0 r = Icc (-r) r

Tactic:
simp [Real.closedBall_eq_Icc]

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
rw [mul_comm, mul_iSup]

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a
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:
rw [iSup_mul]

Goal state after:
ι : Sort u_3
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ i, g i * h ≤ a
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
⊢ sphere x r = {x - r, x + r}

Tactic:
ext

Goal state after:
x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ {x - r, x + r}
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), closedBall x r' = closedBall x r

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), closedBall x r' ↔ x✝ ∈ closedBall x r
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), ball x r' = closedBall x r

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), ball x r' ↔ x✝ ∈ closedBall x r
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ r', ⋃ (_ : r' < r), ball x r' = ball x r

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∈ ball x r
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ r', ⋃ (_ : r' < r), closedBall x r' = ball x r

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∈ ball x r
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
by
  rw [← interior_Icc, mem_interior_iff_mem_nhds]

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

Goal state before:
pp: case inr.inr
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
ext

Goal state after:
case inr.inr
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
x✝ : (b : β) → X b
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
a : E
⊢ ‖fun _i ↦ a‖ = ‖a‖

Tactic:
by
  simpa only [← dist_one_right] using! dist_pi_const a 1

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ IsGreatest (Set.range fun x ↦ ‖f x‖) ‖f‖

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ‖f‖ ∈ Set.range fun x ↦ ‖f x‖

case right
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ‖f‖ ∈ upperBounds (Set.range fun x ↦ ‖f x‖)
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 α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
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
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this✝ : x d ≤ y c
this : d ≤ f (y c)
⊢ False

Tactic:
hfy _ hc

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}
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
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
this✝ : x d ≤ y c
this : d ≤ c
⊢ False
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
⊢ ∃ x ∈ s, IsMinOn f s x
Module: Mathlib.Topology.MetricSpace.Cauchy

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

Tactic:
constructor

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

case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ (∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε) → UniformCauchySeqOn F atTop s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • closedBall b r = closedBall (a • b) r

Tactic:
ext

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • closedBall b r = closedBall (a • b) r

Tactic:
ext
  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • ball b r = ball (a • b) r

Tactic:
ext

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case singleton
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
Hlt : ∀ i ∈ {a✝}, f i < g i
⊢ ∑ i ∈ {a✝}, f i < ∑ i ∈ {a✝}, g i

Tactic:
simp [Hlt _ (Finset.mem_singleton_self _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l v

Tactic:
apply hu.imp
  exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u → ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
Module: Mathlib.Data.EReal.Operations

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

Tactic:
constructor

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

case mpr
x : EReal
⊢ x ≠ ⊥ → ⊤ + x = ⊤
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x

Tactic:
by simp [IsCobounded]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a

Tactic:
by simp [IsCobounded]

Goal state after:
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:
refine hc.mono fun a h ↦ ?_

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 : α
h : (fun x1 x2 ↦ x1 ≤ x2) (s.sup' hs fun i ↦ F i a) c
⊢ (fun x1 x2 ↦ x1 ≤ x2) (F i a) c
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 β
⊢ SupConvergenceClass (α × β)

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ ∀ (a : α × β) (s : Set (α × β)), IsLUB s a → Tendsto Subtype.val atTop (𝓝 a)
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 : α × β) (s : Set (α × β)), IsLUB s a → Tendsto Subtype.val atTop (𝓝 a)

Tactic:
rintro ⟨a, b⟩ s h

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 s (a, b)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
constructor

Goal state after:
case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)

case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)

case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

pp: case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
· rintro ⟨t, ht, hft⟩
    exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩

Goal state after:
case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ c

Tactic:
filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr

Goal state after:
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : limsup (fun i ↦ u i r) cofinite < b
⊢ limsup (fun x ↦ u x r) cofinite ≤ c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ (⊤ * ↑x✝).toReal = ⊤.toReal * (↑x✝).toReal

Tactic:
| top_neg _ h =>

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

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
s : Finset α
⊢ Ici s.card = Finset.card '' {a' | s ⊆ a'}

Tactic:
ext

Goal state after:
α : Type u_3
inst✝ : Infinite α
s : Finset α
x✝ : ℕ
⊢ x✝ ∈ Ici s.card ↔ x✝ ∈ Finset.card '' {a' | s ⊆ a'}
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ u n v ≤ b''

Tactic:
refine hrs n v ?_

Goal state after:
case pos
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ v ≥ rs n
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)

Tactic:
| top_neg _ h =>

Goal state after: