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

Goal state before:
pp: b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a * b⁻¹ * c = a * (b⁻¹ * c⁻¹⁻¹)

pp: case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
inv_inv

Goal state after:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a * b⁻¹ * c = a * (b⁻¹ * c)

case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y

Tactic:
rw [edist_comm z]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ n.succ ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
simp only [zpow_negSucc, coe_inv this, coe_pow]

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

Goal state before:
pp: α : Type u_3
m m' : PseudoMetricSpace α
h : m.toDist = m'.toDist
⊢ m = m'

Tactic:
let d := m.toDist

Goal state after:
α : Type u_3
m m' : PseudoMetricSpace α
h : m.toDist = m'.toDist
d : Dist α := m.toDist
⊢ m = m'
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ count K w I =
    ↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
      ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors)

Tactic:
rw [count_ne_zero K w hI]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j : ι
⊢ ⨅ i, f i * g i ≤ f i * g j

Tactic:
obtain ⟨k, hk⟩ := h i j

Goal state after:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ i, f i * g i ≤ f i * g j
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ sphere x ε ↔ dist y x = ε

Tactic:
mem_sphere

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x = ε ↔ dist y x = ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑(sphere x ε)

Tactic:
sphere_eq_empty_of_subsingleton (NeZero.ne ε)

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑∅
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x = ε ↔ y ∈ sphere x ε

Tactic:
mem_sphere

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x = ε ↔ dist y x = ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
eventually_swap_iff,

Goal state after:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (y : α × ι) in 𝓝 x₀ ×ˢ f, p y.swap) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
Module: Mathlib.Data.Real.Pointwise

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sInf s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sSup (a • s) = a • sSup s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sSup (a • s) = a • sSup s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x✝¹ x✝ : α
⊢ edist x✝¹ x✝ = edist x✝ x✝¹

Tactic:
by simp only [edist_dist, dist_comm]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sSup s
Module: Mathlib.Data.Real.Pointwise

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

case inr
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
⊢ sSup (a • s) = a • sInf s
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)

Tactic:
rw [← @isBounded_univ, isBounded_induced, image_univ]

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

Goal state before:
pp: case e'_3
c : ℝ
c_nn : 0 ≤ c
⊢ c.toNNReal = NNReal.mk c c_nn

Tactic:
simp [Real.toNNReal, c_nn]

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

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ioo a b) ⊆ Icc a b

Tactic:
exact closure_minimal Ioo_subset_Icc_self isClosed_Icc

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ False

Tactic:
have : Ioo a b = Icc a b := by rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this : Ioo a b = Icc a b
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c

Tactic:
obtain ⟨x, hx⟩ := exists_sup_span_eq H
    (by simpa using FractionalIdeal.num_eq_zero_iff.not.mpr ha)

Goal state after:
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
H : ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b
⊢ ‖single i y‖₊ = ‖y‖₊

Tactic:
simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous[inst✝³, inst✝⁴] f
h : HasCompactMulSupport f
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)
  rw [mem_lowerBounds, forall_mem_range] at hx
  exact ⟨x, hx⟩

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

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun n ↦ nndist (u n) (u N)
n : ℕ
h : N ≤ n
⊢ dist (u n) (u N) < ↑R + 1

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun n ↦ nndist (u n) (u N)
n : ℕ
h : n < N
⊢ dist (u n) (u N) < ↑R + 1

Tactic:
· exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : NNReal := (Finset.range N).sup fun n ↦ nndist (u n) (u N)
n : ℕ
h : n < N
⊢ dist (u n) (u N) < ↑R + 1
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ a ∈ eball 1 r ↔ ‖a‖ₑ < r

Tactic:
Metric.mem_eball,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ edist a 1 < r ↔ ‖a‖ₑ < r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹⁻¹ * y⁻¹⁻¹‖

Tactic:
inv_inv

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

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

Tactic:
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.Topology.Order.IntermediateValue

Goal state before:
pp: case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
z : α
h1z : z ∉ s
h2z : z ∈ Ioo x y
⊢ False

Tactic:
exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩

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

Goal state before:
pp: case refine_2
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
⊢ False

Tactic:
· obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
    exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r

Tactic:
simpa [neg_le]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ max b 0

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := ⟨u, ⋯⟩
⊢ ∃ a, Tendsto u atTop (nhds a)

Tactic:
refine ⟨c.lim, fun s h => ?_⟩

Goal state after:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := ⟨u, ⋯⟩
s : Set ℝ
h : s ∈ nhds c.lim
⊢ s ∈ map u atTop
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✝³] (⇑e ⁻¹' Ioi a)

Tactic:
e.preimage_Ioi

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.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)
⊢ ∀ᶠ (x : R) in map 0 f, r x 0

Tactic:
simp_all only [eventually_map, Pi.zero_apply, eventually_true]

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 β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ (s.sup' hs fun i ↦ F i a) ≤ s.sup' hs m

Tactic:
simp only [sup'_le_iff]

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 : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
hI : ⨆ i, I i = 0
⊢ ∃ i, I i = ⊥

Tactic:
rw [← bot_eq_zero, iSup_eq_bot] at hI

Goal state after:
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
hI : ∀ (i : ι), I i = ⊥
⊢ ∃ i, I i = ⊥
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
· rw [limsup_eq]
    refine sInf_le_sInf fun x hx => ?_
    rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
    filter_upwards [I_mem_F] with i hi
    exact hI ▸ le_sSup (mem_image_of_mem _ hi)

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
Module: Mathlib.Topology.EMetricSpace.Lipschitz

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

Tactic:
exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
      hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

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

Goal state before:
pp: case neg
α : 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
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! hbot : ∀ x, f.limsSup ≤ x
      · let : OrderBot α := { bot := f.limsSup, bot_le := hbot }
        refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_
        exact lt_mem_sets_of_limsSup_lt hb h |>.frequently
      · refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_
        exact frequently_lt_of_lt_limsSup hc hl |>.and_eventually <| lt_mem_sets_of_limsSup_lt hb hg

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x ↦ a ⊔ u x) f

Tactic:
by
  simp only [liminf_eq_iSup_iInf]
  rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)

Tactic:
exact hfL.comp (hgL.mono inter_subset_left)
    ((mapsTo_preimage g u).mono_left inter_subset_right)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ x < y + (t - z)

Tactic:
rw [hy_top, top_add_of_ne_bot]

Goal state after:
case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ x < ⊤

case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ t - z ≠ ⊥
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ i, ⨆ b ∈ decode₂ β i, f b = ⨆ b, f b

Tactic:
rw [iSup_comm]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ j, ⨆ i, ⨆ (_ : j ∈ decode₂ β i), f j = ⨆ b, f b
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)
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
⊢ rs ↑⟨n, hn⟩ ≤ ⨆ n, rs ↑n

Tactic:
refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using! hb''
      exact Finite.bddAbove_range _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ HasProd f a L

Tactic:
HasProd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)