mathlib-initiative/mathlib-tactics huggingface dataset:
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 * p.asIdeal * ∏ x ∈ s \ {p}, x.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1

Tactic:
mul_right_comm _ p.asIdeal

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 * ∏ x ∈ s \ {p}, x.asIdeal) * p.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ x - y ≤ |x - y|

Tactic:
le_abs

Goal state after:
x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨅ i, f i) * r = ⨅ i, f i * r

Tactic:
simp only [Real.mul_iInf_of_nonneg ha, mul_comm]

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

Goal state before:
pp: ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a

Tactic:
by
  rw [mul_iSup]
  exact ciSup_le' H

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

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

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, dist_self]

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 : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y ∩ s) ∧ Tendsto u atTop (𝓝 x)

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

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

Goal state before:
pp: n : ℕ
⊢ ‖↑n‖ₑ = ↑n

Tactic:
simp [enorm]

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

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

Tactic:
simp [enorm]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

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

Goal state before:
pp: ε : Type u_9
inst✝ : ENorm ε
x : ε
⊢ ‖‖x‖ₑ‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

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
m' n' : ℕ
hm' : (m', n').1 ≥ n
hn' : (m', n').2 ≥ n
⊢ (fun p ↦ dist (s p.1) (s p.2)) (m', n') ≤ ε / 2

Tactic:
exact le_of_lt (hN _ (le_trans hn hm') _ (le_trans hn hn'))

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ ‖x‖ₑ.toReal = ‖x‖

Tactic:
simp [enorm]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ

Tactic:
simp [enorm]

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ ‖a / b‖ = 0 ↔ a = b

Tactic:
rw [norm_eq_zero', div_eq_one]

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

Goal state before:
pp: 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
x✝¹ : Fintype { v // v.asIdeal ∣ map (algebraMap S R) p } := hF
x✝ : { v // v.asIdeal ∣ map (algebraMap S R) p }
v : HeightOneSpectrum R
property✝ : v.asIdeal ∣ map (algebraMap S R) p
this : v.asIdeal.LiesOver p
⊢ (↑⟨v, property✝⟩).maxPowDividing (map (algebraMap S R) p) =
    ↑((equivPrimesOver R hp) ⟨v, property✝⟩) ^ (↑((equivPrimesOver R hp) ⟨v, property✝⟩)).ramificationIdx S

Tactic:
simp [maxPowDividing_eq_pow_multiset_count _ h, ramificationIdx_eq_factors_count p v h]

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 * 1

Tactic:
{ rw [mul_one]
      exact le_max_left _ _ }

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

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

Tactic:
by
  rcases le_or_gt a b with hab | hab
  · exact hf_c.continuousOn.image_Icc_of_monotoneOn hab (hf.monotone.monotoneOn _)
  · simp [not_le.mpr hab, not_le.mpr (hf hab)]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : MetricSpace α
hs2 : Bornology.IsBounded s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ 0 < diam s

Tactic:
exact (dist_pos.mpr hxy).trans_le <| Metric.dist_le_diam_of_mem hs2 hx hy

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

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

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

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
convert! tendsto_atBot_isLUB h_anti.dual ha.dual using 1

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

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
ih

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ (𝓟 s).limsSup = sSup s

Tactic:
by
  simp only [limsSup, eventually_principal]; exact csInf_upperBounds_eq_csSup h hs

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

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

Tactic:
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ (n + 1) • x = ↑(n + 1) * x

Tactic:
succ_nsmul,

Goal state after:
case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ n • x + x = ↑(n + 1) * x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : IsEmpty β
⊢ ∏'[L] (b : β), f b = 1

Tactic:
convert! tprod_one (L := L)

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝³ : CommGroupWithZero K
inst✝² : TopologicalSpace K
f g : α → K
L : SummationFilter α
inst✝¹ : ContinuousInv₀ K
inst✝ : ContinuousMul K
a b : K
hf : HasProd f a L
hg : HasProd g b L
hb : b ≠ 0
⊢ HasProd (fun x ↦ f x / g x) (a / b) L

Tactic:
by
  simp only [div_eq_mul_inv]
  exact hf.mul <| hg.inv₀ hb

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : HasSum f a₁ L
⊢ HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) L

Tactic:
by
  simpa only using! h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  · exact ((Homeomorph.mulLeft₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulLeft a)).symm

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

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n ↦ f ↑n) ∧ Multipliable fun n ↦ f (-(↑n + 1))

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩

Goal state after:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f ↑n

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f (-(↑n + 1))
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)

Tactic:
simp only [pow_add, even_two, Even.mul_right, Even.neg_pow, one_pow, pow_one, mul_neg, mul_one,
      neg_mul, one_mul]

Goal state after:
case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ -f (2 * k + 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
a : G
⊢ HasProd (fun x ↦ f ↑x) a ↔ HasProd f (a * f 0)

Tactic:
simp [hasProd_pnat_iff_hasProd_succ, hasProd_nat_add_iff]

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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoEMetricSpace β
α : Type u_4
inst✝¹ : EMetricSpace α
inst✝ : Nontrivial α
f : α → β
hf : AntilipschitzWith 0 f
h₀ : 0 ≤ 0
⊢ False

Tactic:
exact not_subsingleton α hf.subsingleton

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ ↑K * edist (g x) (g y)

Tactic:
by simpa only [hg _] using hf (g x) (g y)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y

Tactic:
by rw [← h, hg _, hg _]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam (⇑h ⁻¹' s) = Metric.ediam s

Tactic:
rw [← image_symm, ediam_image]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ (Finset.univ.sup fun b ↦ edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b)) =
    Finset.univ.sup fun b ↦ edist (x1 b) (x2 b)

Tactic:
Finset.sup_univ_eq_iSup

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ ⨆ b, edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b) = ⨆ b, edist (x1 b) (x2 b)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
ys_in_fK : ∀ (n : ℕ), ys n ∈ f '' K
⊢ ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)

Tactic:
choose xs xs_in_K fxs_eq_ys using ys_in_fK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
xs : ℕ → X
xs_in_K : ∀ (n : ℕ), xs n ∈ K
fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n
⊢ ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V

Tactic:
simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
    simpa only [forall_and, forall_mem_image, not_and] using! seq_of_forall_finite_exists h

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

Goal state before:
pp: case inr.refine_1
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩

Goal state after:
case inr.refine_1.refine_1
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ (a, b).1 < x - min ε ↑δ

case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + min ε ↑δ < (a, b).2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf

Goal state after:
case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
by
  simp [projIcc, Subtype.ext_iff, h.not_ge]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩

Goal state after:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n m N : β
hn : N ≤ n
hm : N ≤ m
⊢ edist (s n) (s m) ≤ (fun N ↦ ediam (s '' Ici N)) N

case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ Tendsto (fun N ↦ ediam (s '' Ici N)) atTop (𝓝 0)
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) x = f x

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
· lift x to Icc a b using ⟨hax, hxb⟩
      rw [IccExtend_val, comp_apply]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf f u

Tactic:
refine le_antisymm ?_ <| liminf_le_liminf <| .of_forall <| by simp
  refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_
  rw [Filter.le_liminf_iff']
  rintro a hab
  filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos]
    with i hfg hg
  exact ENNReal.le_of_add_le_add_right (hg.trans_lt <| by simp).ne <|
    (add_le_of_le_tsub_left_of_le hab.le <| hg.trans <| min_le_left ..).trans hfg

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedGroup E
inst✝³ : SeminormedGroup F
inst✝² : FunLike 𝓕 E F
inst✝¹ : IsometryClass 𝓕 E F
inst✝ : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ ‖f x‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a * b⁻¹) (a * c⁻¹) = edist b c

Tactic:
edist_mul_left,

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist b⁻¹ c⁻¹ = edist b c
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Tactic:
exact preimage_smul_ball (MulOpposite.op a) b r

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ (fun n ↦ ∏ k ∈ range (n + 1), u k) = d * fun n ↦ ∏ k ∈ range (n + 1), v k

Tactic:
ext n; simp [d]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝¹.toFun x) (toEquiv✝¹.toFun y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv✝.toFun x) (toEquiv✝.toFun y) = ↑r * edist x y
h :
  ⇑{ toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ }.toEquiv =
    ⇑{ toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }.toEquiv
⊢ toEquiv✝¹ = toEquiv✝

Tactic:
exact DFunLike.ext' h

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ∞ = if c = 0 then 0 else ∞

Tactic:
rw [← smul_one_mul, mul_top']

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ∞) = if c = 0 then 0 else ∞
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
inst✝¹ : One G
inst✝ : NormOneClass G
⊢ ‖1‖ₑ = 1

Tactic:
simp [enorm]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

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

Goal state before:
pp: x : ℝ≥0
⊢ ‖↑x‖ₑ = ↑x

Tactic:
simp [enorm]

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

Goal state before:
pp: α : Type u_2
inst✝² : SeminormedAddCommGroup α
inst✝¹ : Mul α
inst✝ : NormMulClass α
a b : α
⊢ ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

Tactic:
simp [enorm]

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

Goal state before:
pp: α : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormMulClass α
a : α
n : ℕ
⊢ ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

Tactic:
simp [enorm]

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Tactic:
simpa only [dist_eq_norm_neg_add, add_zero, norm_neg] using dist_smul_pair s x y

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)

Tactic:
gcongr; apply norm_smul_le

Goal state after: