mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a

Tactic:
coe_ne_zero

Goal state after:
a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case neg.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ 0 * ⨆ i, f i = ⨆ i, 0 * f i

pp: case neg.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
· simp

Goal state after:
case neg.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
⊢ (↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹

pp: case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
· simp

Goal state after:
case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ (ball x ε ∪ sphere x ε) \ ball x ε = sphere x ε

Tactic:
Set.union_sdiff_cancel_left sphere_disjoint_ball.symm.le_bot

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ sphere x ε = sphere x ε
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf ∅ = a • sInf ∅

Tactic:
Real.sInf_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ 0 = a • 0
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sInf ∅ = a • sSup ∅

Tactic:
Real.sInf_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ 0 = a • sSup ∅
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ 0 = a • sInf ∅

Tactic:
Real.sInf_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ 0 = a • 0
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
t : Set β
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Bornology α
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

pp: case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable (range fun x ↦ f ↑x)

Tactic:
← image_univ

Goal state after:
β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable ((fun x ↦ f ↑x) '' univ)
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' ball a r = ball (↑a) r ∩ {a | p a}

Tactic:
← preimage_ball,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' val ⁻¹' ball (↑a) r = ball (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst✝³] (Ioi a)

Tactic:
· rw [← sdiff_subset_closure_iff, Ici_sdiff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
⊢ Ioc a a ⊆ closure[inst✝³] (interior (Ioc a a))

pp: case inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure[inst✝³] (interior (Ioc a b))

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure[inst✝³] (interior (Ioc a b))
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a b : α
s : Set α
x : α
inst✝ : Nontrivial α
⊢ (𝓝[≠] x).NeBot

Tactic:
refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a b : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
⊢ s.Nonempty
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : Nonempty γ
⊢ f '' S ⊆ range f

Tactic:
by grind

Goal state after:
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
x✝ : Icc a c ∈ f
⊢ Icc a c ⊆ Iio x

Tactic:
by grind

Goal state after:
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
⊢ a ≤ x

Tactic:
by grind

Goal state after:
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
h : b < x
⊢ Icc a b ⊆ Iio x

Tactic:
by grind

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

Goal state before:
pp: case inl
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hs : IsClosed[inst✝¹] ∅
⊢ IsClosed[inst✝¹] ↑(upperClosure ∅)

pp: case inr
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
h₁ : s.Nonempty
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
· simp

Goal state after:
case inr
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
h₁ : s.Nonempty
⊢ IsClosed[inst✝¹] ↑(upperClosure s)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
n : ℕ
⊢ d < u n

Tactic:
by grind

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

Goal state before:
pp: 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‖)

Tactic:
· rintro - ⟨x, rfl⟩
    exact norm_le_pi_norm' f x

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✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
⊢ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}.Countable

Tactic:
by
  apply (countable_image_lt_image_Ioi_within s f).mono
  rintro x ⟨xs, hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x⟩
  dsimp only [mem_ofPred_eq]
  contrapose! hx
  refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩
  · filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy
    exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))
  rcases hx xs u hu with ⟨v, vs, xv, fvu⟩
  have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]
  filter_upwards [this] with y hy
  exact (hf hy.1 vs hy.2.2.le).trans_lt fvu

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

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
x : γ
hx : x ∈ s
hbl : (N, N).1 ≤ b.1
hbr : (N, N).2 ≤ b.2
⊢ (F b.1 x, F b.2 x) ∈ u

Tactic:
exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ |sSup (S n)| < ε

Tactic:
abs_of_nonneg (S0 n)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ sSup (S n) < ε
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inl.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
calc
      edist a b ≤ ediam s := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + (edist x y + ediam t) := le_self_add
      _ = ediam s + edist x y + ediam t := (add_assoc _ _ _).symm

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

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

Tactic:
suffices Icc x y ⊆ s from
    hst ⟨y, xyab <| right_mem_Icc.2 hxy, this <| right_mem_Icc.2 hxy, hy.2⟩

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
h_surj : SurjOn f (Icc a b) (Icc a b)
x₀ : α
hx₀ : x₀ ∈ Icc a b ∧ f x₀ = a
x₁ : α
hx₁ : x₁ ∈ Icc a b ∧ f x₁ = b
⊢ f x₀ ≤ x₀

Tactic:
by grind

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
h_surj : SurjOn f (Icc a b) (Icc a b)
x₀ : α
hx₀ : x₀ ∈ Icc a b ∧ f x₀ = a
x₁ : α
hx₁ : x₁ ∈ Icc a b ∧ f x₁ = b
⊢ x₁ ≤ f x₁

Tactic:
by grind

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
← preimage_ball,

Goal state after:
x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' ball (↑x) r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
J : Ideal R
⊢ emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)

pp: case inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
· simp

Goal state after:
case inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr.inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)

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 ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
· simp

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 ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
rw [← Nat.dist_cast_real, ← Rat.dist_cast]; congr

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

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

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

Tactic:
· simp

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

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
· simp

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
by isBoundedDefault

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Tactic:
by isBoundedDefault

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ i ∈ f, sSup (u '' id i) = ⨅ s ∈ f, ⨆ a ∈ s, u a

Tactic:
simp only [sSup_image, id]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
hf : f.HasBasis p s
q : β → Prop
⊢ blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Tactic:
simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and,
    mem_ofPred_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
⊢ LipschitzWith 1 fun a ↦ (a, b)

Tactic:
simpa only [max_eq_left zero_le_one] using! LipschitzWith.id.prodMk (LipschitzWith.const b)

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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
⊢ ClusterPt f.limsSup f

Tactic:
let : OrderBot α := { bot := f.limsSup, bot_le := hbot }

Goal state after:
case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
this : OrderBot α := { bot := f.limsSup, bot_le := hbot }
⊢ ClusterPt f.limsSup f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
⊢ False

Tactic:
obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s :=
    dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo
      (Set.nonempty_Ioo.2 hlt)

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ False
Module: Mathlib.Data.EReal.Operations

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

Tactic:
by_contra ha

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

Goal state before:
pp: ι : 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)
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨n0⟩⟩

Goal state after:
case inl
ι : 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)
hι : IsEmpty ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

case inr
ι : 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 : ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
  refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa

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

Goal state before:
pp: x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : ¬x = y
⊢ x < y

Tactic:
by grind

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

Goal state before:
pp: case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ ⊤ = -⊥

Tactic:
neg_bot

Goal state after:
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ ⊤ = ⊤