mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
y : δ
⊢ y ∈ Ioi (f a) → y ∈ f '' Iio a

Tactic:
hy

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
y : δ
hy : y ∈ Ioi (f a)
⊢ y ∈ f '' Iio a
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty
  · exact ⟨fun i ↦ ∅, monotone_const, by simp_all⟩
  refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
  · exact inter_subset_inter_right _ (ball_subset_ball (Nat.cast_le.2 hij))
  · simp [← inter_iUnion]
  · exact isBounded_ball.subset inter_subset_right

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

Goal state before:
pp: case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
⊢ False

Tactic:
by_cases! hb : f ⊥ < f b

Goal state after:
case pos
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
⊢ False

case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ False
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 f l atTop

Tactic:
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]

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.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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
cases subsingleton_or_nontrivial α with
  | inl h => exact Or.inl <| Subsingleton.strictMono f
  | inr h =>
    obtain ⟨a, b, hab⟩ := exists_pair_lt α
    exact H hab

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

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddBelow (closedBall 0 r)

Tactic:
by simp [closedBall_eq_Icc]

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

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddAbove (closedBall 0 r)

Tactic:
by simp [closedBall_eq_Icc]

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

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

Tactic:
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]

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

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

Tactic:
constructor <;> intro h

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

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y

Tactic:
simpa [add_comm] using add_lt_add_right_coe h z

Goal state after:
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 <;> intro h

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
h : 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
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

pp: case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z

Tactic:
· obtain rfl := htop rfl rfl
      simpa

Goal state after:
case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
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 : ℝ≥0∞
y : EReal
⊢ ↑x = y → recENNReal coe neg_coe y ≍ coe x

Tactic:
hy

Goal state after:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
y : EReal
hy : ↑x = y
⊢ recENNReal coe neg_coe y ≍ coe x
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ edist (f x) (f y) < ↑K * r

Tactic:
grw [h x y]; gcongr; simp

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
x✝ : α
hx : x✝ ∈ s
y✝ : α
⊢ y✝ ∈ s → edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y✝) ≤ ↑(max Kf Kg) * edist x✝ y✝

Tactic:
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 bot
a b : EReal
h : a ≤ b + ⊥
⊢ a - ⊥ ≤ b

Tactic:
add_bot,

Goal state after:
case bot
a b : EReal
h : a ≤ ⊥
⊢ a - ⊥ ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥

Tactic:
exact mul_bot_of_pos h

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

Goal state before:
pp: case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Goal state after:
case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Goal state after:
case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

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

Goal state before:
pp: case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Goal state after:
case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

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

Goal state before:
pp: case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Goal state after:
case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

Tactic:
· apply le_limsup_of_frequently_le _ h₂
    push +distrib Not at h'
    rcases h' with ⟨z, z_x, hz⟩
    exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
⊢ Pairwise (Disjoint on fun i ↦ ⋃ b ∈ decode₂ β i, f b)

Tactic:
by
  rintro i j ij
  refine disjoint_left.mpr fun x => ?_
  suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
  rintro a rfl ha b rfl hb
  exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩

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

Goal state before:
pp: a b : EReal
⊢ 0 < a * b ∨ 0 = a * b ↔ (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
mul_pos_iff,

Goal state after:
a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ 0 = a * b ↔ (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
mul_pos_iff,

Goal state after:
a b : EReal
⊢ 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this : x < F.limsSup
⊢ False

Tactic:
have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this✝ : x < F.limsSup
this : (Set.Ioo c F.limsSup).Nonempty
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : ¬L.NeBot
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
simpa [tprod_bot hL] using
      (MonoidHomClass.toMonoidHom g).map_finprod_of_injective hge.injective _

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
· exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
obtain ⟨s, hs⟩ := vanish e he

Goal state after:
case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val

Tactic:
exact ⟨⟨n, h⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
  norm_cast

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
α : Fin 2 → Type u_3
inst✝ : (i : Fin 2) → PseudoEMetricSpace (α i)
x hx : (i : Fin 2) → α i
⊢ edist ((piFinTwoEquiv α).toFun x) ((piFinTwoEquiv α).toFun hx) = edist x hx

Tactic:
simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
by
  refine
    ⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
  rintro s ⟨hbs, hsc⟩
  refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
  rw [← seqClosure_eq_closure]
  rintro ⟨u, hus, hu⟩
  exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Tactic:
rcases hx with ⟨u, hus, hu⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
⊢ x ∈ seqClosure s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Set E
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Tactic:
by
  simp [Metric.mem_closure_iff, dist_eq_norm_div]

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

Goal state before:
pp: case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
· intro l hl
    obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := Nat.exists_eq_succ_of_ne_zero hl.ne'
    rw [← norm_inv']
    simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right,
      mul_inv_rev, inv_inv, v]
    apply hφ

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
⊢ y ∈ closedEBall x ↑δ → f y ∈ Icc (f x - ε) (f x + ε)

Tactic:
hy

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y ∈ Icc (f x - ε) (f x + ε)
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

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

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K ↔ IsComplete (closedBall 0 1)

Tactic:
constructor <;> intro h

Goal state after:
case mp
K : Type u_4
inst✝ : NormedField K
h : CompleteSpace K
⊢ IsComplete (closedBall 0 1)

case mpr
K : Type u_4
inst✝ : NormedField K
h : IsComplete (closedBall 0 1)
⊢ CompleteSpace K
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) ↔ MeasurableSet s

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ MeasurableSet s

case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x ↦ b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
⊢ MeasurableSet (measurableAtom x)

Tactic:
have : ∀ (y : β), y ∉ measurableAtom x → ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s :=
    fun y hy ↦ by simpa [measurableAtom] using hy

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
this : ∀ y ∉ measurableAtom x, ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s
⊢ MeasurableSet (measurableAtom x)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
z : β
hz : z ∈ measurableAtom x
⊢ z ∈ measurableAtom y

Tactic:
simp only [measurableAtom, mem_iInter] at hz hx ⊢

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y z : β
hz : ∀ (i : Set β), x ∈ i → MeasurableSet i → z ∈ i
hx : ∀ (i : Set β), y ∈ i → MeasurableSet i → x ∈ i
⊢ ∀ (i : Set β), y ∈ i → MeasurableSet i → z ∈ i
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ((restrict s) m) u ≤ ((restrict t) m') u

Tactic:
simp only [restrict_apply]
  exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

Goal state after: