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

Goal state before:
pp: ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
iInf_add,

Goal state after:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = ⨅ i, f i + iInf g
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
iInf_add,

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ i, f i + iInf g
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : ¬I * I' ≠ 0
⊢ count K v (I * I') = 0

Tactic:
not_ne_iff

Goal state after:
case neg
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
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ count K v (I * I') = 0
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
hv : ↑v.asIdeal ≠ 0
⊢ ↑v.asIdeal = 1 * ↑v.asIdeal

Tactic:
one_mul

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
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : ↑v.asIdeal ≠ 0
⊢ ↑v.asIdeal = ↑v.asIdeal
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ 1 * y ≤ x * z ↔ y ≤ x * z

Tactic:
one_mul

Goal state after:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ y ≤ x * z ↔ y ≤ x * z
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ 1 * (a * b⁻¹) = a * b⁻¹

Tactic:
one_mul

Goal state after:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * b⁻¹ = a * b⁻¹
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)) = -count K v (I ^ n)

Tactic:
by
  by_cases hI : I = 0
  · by_cases hn : n = 0
    · rw [hn, neg_zero, zpow_zero, count_one, neg_zero]
    · rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_zero]
  · rw [eq_neg_iff_add_eq_zero, ← count_mul K v (zpow_ne_zero _ hI) (zpow_ne_zero _ hI),
      ← zpow_add₀ hI, neg_add_cancel, zpow_zero]
    exact count_one K v

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

Goal state before:
pp: case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

Tactic:
have : a = 0 := by simpa [h0] using h

Goal state after:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a ≤ 1 * a

Tactic:
one_mul

Goal state after:
a : ℝ≥0∞
⊢ a ≤ a
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
exact ENNReal.div_le_of_le_mul h

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 w : HeightOneSpectrum R
hw : w ≠ v
⊢ ↑w.asIdeal = 1 * ↑w.asIdeal

Tactic:
one_mul

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
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
⊢ ↑w.asIdeal = ↑w.asIdeal
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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 :=
    coeIdeal_ne_zero.mpr w.ne_bot

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
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ count K v ↑w.asIdeal = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ 1 * b⁻¹ = b⁻¹

pp: a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞

Tactic:
one_mul

Goal state after:
a b : ℝ≥0∞
h : a * b = 1
⊢ b⁻¹ = b⁻¹

a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ 1 * b

Tactic:
one_mul

Goal state after:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ a = b

Tactic:
← (eq_div_iff hb₀ hb₁).mp h.symm,

Goal state after:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ b * 1 = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹.toReal = a.toReal⁻¹

Tactic:
simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ x ∈ closedBall x ε

Tactic:
mem_closedBall,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ dist x x ≤ ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
mem_closedBall,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ dist y x ≤ ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ⋃ n, s ∩ closedBall x ↑n = s

Tactic:
rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]

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

Goal state before:
pp: x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)

Tactic:
mem_closedBall,

Goal state after:
x r y : ℝ
⊢ dist y x ≤ r ↔ y ∈ Icc (x - r) (x + r)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)

Tactic:
rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add',
    sub_le_comm]

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:
nhds_basis_closedBall.tendsto_right_iff

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.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst✝¹] t
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
refine ⟨t, htc, fun x hx => ?_⟩

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst✝¹] t
x : X
hx : x ∈ s
⊢ x ∈ ⋃ x ∈ t, ball x U
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 (f '' s)

Tactic:
rw [image_eq_range, ← 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.Pi

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (Pi.single i a k) (Pi.single j b k) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp only [Pi.single_apply]

Goal state after:
case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ‖r‖ₑ = ‖|r|‖ₑ

Tactic:
enorm_abs

Goal state after:
r : ℝ
⊢ ‖r‖ₑ = ‖r‖ₑ
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:
apply (countable_image_lt_image_Ioi_within s f).mono

Goal state after:
α : 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} ⊆ {x | x ∈ s ∧ ∃ z, f x < z ∧ ∀ y ∈ s, x < y → z ≤ f y}
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖1 * a‖ = ‖a‖

Tactic:
one_mul

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a‖ = ‖a‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖1 * v‖

Tactic:
one_mul

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖v‖
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩
  rsuffices ⟨R, R0, H⟩ : ∃ R > 0, ∀ n, dist (u n) (u N) < R
  · exact ⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩
  let R := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
  refine ⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => ?_⟩
  rcases le_or_gt N n with h | h
  · exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)
  · have : _ ≤ R := Finset.le_sup (Finset.mem_range.2 h)
    exact lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r

Tactic:
mem_closedBall,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ dist b a ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ closedBall 1 r ↔ ‖a‖ ≤ r

Tactic:
mem_closedBall,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ dist a 1 ≤ r ↔ ‖a‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Tactic:
mem_closedBall,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ dist b a ≤ r ↔ ‖b / a‖ ≤ r
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
⊢ ∀ x_1 ∈ s ∩ Ico x y, s ∈ 𝓝[>] x_1

Tactic:
rintro z ⟨zs, hz⟩

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
z : α
zs : z ∈ s
hz : z ∈ Ico x y
⊢ s ∈ 𝓝[>] z
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ (mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)) ⊆ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset

Tactic:
intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
by
  simp only [dist_comm c, tendsto_dist_right_atTop_iff]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsCobounded s ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Tactic:
← isBounded_compl_iff,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsBounded sᶜ ↔ ∃ r, (closedBall c r)ᶜ ⊆ s
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 ≤ 1 * max b 0

Tactic:
one_mul

Goal state after:
α : 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
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : a ≤ b
⊢ f '' Ico a b = Ico (f a) (f b)

Tactic:
exact hf_c.continuousOn.image_Ico_of_strictMonoOn hab (hf.strictMonoOn _)

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h✝ : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
⊢ g / a ^ k < a

Tactic:
by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : 1 * g ^ m ∈ Ioc a (a * g)
⊢ ∃ c ∈ ↑S, c ∈ Ioo a b

Tactic:
one_mul

Goal state after:
case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : g ^ m ∈ Ioc a (a * g)
⊢ ∃ c ∈ ↑S, c ∈ Ioo a b
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
p : ℚ≥0 × R
| p.1 • p.2

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ]

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
p : ℚ≥0 × R
| ↑p.1 • p.2
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff]

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

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

Tactic:
real_coe_toENNReal

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ENNReal.ofReal (a✝¹ + a✝) = ENNReal.ofReal a✝¹ + ENNReal.ofReal a✝
Module: Mathlib.Data.EReal.Operations

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

Tactic:
rcases h'.eq_or_lt with (rfl | hlt)

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

case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I ↦ sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x

Tactic:
exact hI ▸ le_sSup (mem_image_of_mem _ hi)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ p x ∨ ¬p x) = limsup u f

Tactic:
or_not,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ True) = limsup u f
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:
simp only [liminf_eq_iSup_iInf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
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
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
rcases hf (g x) with ⟨Kf, u, hu, hfL⟩

Goal state after:
α : 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
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ liminf u f \ a = liminf (fun b ↦ u b \ a) f

Tactic:
by
  simp only [_root_.sdiff_eq, inf_comm _ aᶜ, inf_liminf]

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

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

Tactic:
simp [top_mul_coe_of_neg h]

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

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

Tactic:
simp_all [← EReal.coe_mul]

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

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

Tactic:
{· 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:
simp_all [← EReal.coe_mul]

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

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

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

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

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

Tactic:
simp_all [← EReal.coe_mul]

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

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

Tactic:
{· 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:
simp_all [← EReal.coe_mul]

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

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

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

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

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

Tactic:
simp_all [← EReal.coe_mul]

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

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

Tactic:
{· 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:
simp_all [← EReal.coe_mul]

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

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

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

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

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

Tactic:
simp_all [← EReal.coe_mul]

Goal state after: