mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ↑y) = Ioi x ∩ Iio y

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x

Tactic:
simp

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y

Tactic:
simp

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y

Tactic:
simp

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ

Tactic:
simp

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

Goal state before:
pp: ⊢ sInf {b | 1 ≤ 0 * b} = ∞

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ ↑(∞ * ↑0) = ⊤ * ↑↑0

Tactic:
simp

Goal state after:
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
v : HeightOneSpectrum R
n : ℕ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ n) = ↑n * count K v I

Tactic:
by
  induction n with
  | zero => rw [pow_zero, ofNat_zero, zero_mul, count_one]
  | succ n h =>
    classical rw [pow_succ, count_mul']
    by_cases hI : I = 0
    · have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
      rw [if_neg h_neg, hI, count_zero, mul_zero]
    · rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]
      ring

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

Goal state before:
pp: case bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ ↑x ∈ {⊥, ⊤}ᶜ

Tactic:
simp

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

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ (fun x ↦ (↑x).toReal) ((fun x ↦ ⟨↑x, ⋯⟩) x) = x

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ ∞ ↔ a ≠ 0

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ 0 ↔ a ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

Tactic:
simp

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

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b / c
⊢ a * c < b

Tactic:
by
  contrapose! h
  exact ENNReal.div_le_of_le_mul h

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

Goal state before:
pp: a b c : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ b⁻¹ < c⁻¹ ↔ c < b

Tactic:
simp

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

Goal state before:
pp: case h0
a b : ℝ≥0∞
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case ht
a b : ℝ≥0∞
⊢ 1 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case hp₂
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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
⊢ (w ∈ fun i ↦ i = v → False) → count K v (↑w.asIdeal ^ exps w) = 0

Tactic:
hw

Goal state after:
case hp₂
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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ count K v (↑w.asIdeal ^ exps w) = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
⊢ max (edist x.1 x.1) (edist x.2 x.2) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε

Tactic:
rw [edist_comm, mem_closedEBall]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
simp

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
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

Tactic:
simp

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

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
x x✝ : γ
⊢ x✝ ∈ closedEBall x 0 ↔ x✝ ∈ {x}

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ∞⁻¹.toNNReal = ∞.toNNReal⁻¹

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ univ → ∀ ⦃y : α⦄, y ∈ univ → dist x y ≤ C) ↔ ∃ C, ∀ (a b : α), dist a b ≤ C

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ univ → ∀ ⦃y : α⦄, y ∈ univ → nndist x y ≤ C) ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal

Tactic:
conv_rhs => rw [← mul_one (J * _)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ q ∈ s, q.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x ↑ε = ball x ↑ε

Tactic:
← eball_ofReal

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x ↑ε = eball x (ENNReal.ofReal ↑ε)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x ↑ε = eball x (ENNReal.ofReal ↑ε)

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α✝
α : Type u
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y ≠ ∞
⊢ ∀ (x y : α), 0 ≤ (edist x y).toReal

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0
⊢ a = b ↔ ↑a = ↑b

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0
⊢ a ≤ b ↔ ↑a ≤ ↑b

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0
⊢ a < b ↔ ↑a < ↑b

Tactic:
simp

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

Goal state before:
pp: a b : ℝ≥0
⊢ a ≠ b ↔ ↑a ≠ ↑b

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : Tendsto f l (𝓝 0)
⊢ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε

Tactic:
rw [nhds_basis_closedBall.tendsto_right_iff] at hf

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
⊢ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ

Tactic:
eq_univ_iff_forall,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ∀ (x : α), x ∈ ⋃ c ∈ s, ball c r
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
simp

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

Tactic:
simp

Goal state after:
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 ∅

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
⊢ False

Tactic:
have H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p := by
    refine sum_mem fun q hq ↦ ?_
    rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
    refine Ideal.mul_mono_right ?_ (ha q hq.1)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
simp

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

Goal state before:
pp: X : Type u_2
inst✝ : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset ↑s
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i) ε
⊢ ↑(Finset.map { toFun := Subtype.val, inj' := ⋯ } t) ⊆ s

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
simp

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

Goal state before:
pp: c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c

Tactic:
simp

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

Goal state before:
pp: c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c

Tactic:
simp

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

Goal state before:
pp: case inr.inl.mk
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
fst✝ : α
snd✝ : β
⊢ sphere (fst✝, snd✝) 0 =
    sphere (fst✝, snd✝).1 0 ×ˢ closedBall (fst✝, snd✝).2 0 ∪ closedBall (fst✝, snd✝).1 0 ×ˢ sphere (fst✝, snd✝).2 0

Tactic:
simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]

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

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

Tactic:
apply Subset.antisymm
  · exact closure_minimal Ico_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
    rw [closure_Ioo hab]

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))

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
f : (b : β) → X b
⊢ ∀ b ∈ Finset.univ, edist (f b) (f b) ≤ ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s t : Set α
hs : Dense s
ht : IsOpen[inst✝²] t
x : α
⊢ t ∩ s ⊆ t

Tactic:
simp

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Tactic:
← coe_nndist,

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ ↑(nndist f g) = ↑r ↔ (∃ i, ↑(nndist (f i) (g i)) = ↑r) ∧ ∀ (b : β), ↑(nndist (f b) (g b)) ≤ ↑r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
inhabit β

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0
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 ∅)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvx : Tendsto v atTop (𝓝[≤] x)
hvt : ∀ (n : ℕ), v n ∈ t
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
replace hvx := hvx.mono_right nhdsWithin_le_nhds

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : EMetricSpace α
h : ∀ (x y : α), edist x y ≠ ⊤
⊢ ∀ (x y : α), 0 ≤ (edist x y).toReal

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
⊢ x ∉ Ioo y x ∩ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by
  simpa using! exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
⊢ ‖0‖ₑ = 0

Tactic:
simp

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
⊢ ∀ (x y : ℝ≥0∞), ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Tactic:
simp

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
⊢ ∀ (x : ℝ≥0∞), ‖x‖ₑ = 0 ↔ x = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ ↑‖2‖₊ = ↑2

Tactic:
simp

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
⊢ Finset.univ.Nonempty

Tactic:
simp

Goal state after:
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
b : ι
⊢ ∀ (i : ι), ‖0‖₊ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ ∅ ∈ {s | BddBelow s ∧ BddAbove s}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ ∀ (x : α), {x} ∈ {s | BddBelow s ∧ BddAbove s}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
x✝ : ∃ i, True ∧ Ici i ⊆ s
b : α
left✝ : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
⊢ ⊥ ≤ x

Tactic:
simp

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 : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
⊢ s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x

Tactic:
simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
w : α
⊢ w ∈ Ioo z x → l < f w

Tactic:
hw

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
w : α
hw : w ∈ Ioo z x
⊢ l < f w
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w✝ : α
hy : y < w✝
hx : w✝ < x
w : α
⊢ w ∈ Ioo y x → f w < m

Tactic:
hw

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w✝ : α
hy : y < w✝
hx : w✝ < x
w : α
hw : w ∈ Ioo y x
⊢ f w < m
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
w : α
⊢ w ∈ Ioo x y → l < f w

Tactic:
hw

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
w : α
hw : w ∈ Ioo x y
⊢ l < f w
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
w : α
⊢ w ∈ Ioo x z → f w < m

Tactic:
hw

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
w : α
hw : w ∈ Ioo x z
⊢ f w < m