mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q
hSq : IsDiscreteValuationRing (Localization.AtPrime q)
⊢ p.ramificationIdx' q =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q)).toNat

Tactic:
hSq.length_quotient_pow_maximalIdeal,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q
hSq : IsDiscreteValuationRing (Localization.AtPrime q)
⊢ p.ramificationIdx' q = (↑(p.ramificationIdx' q)).toNat
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ q.ramificationIdx R ∣ r.ramificationIdx R

Tactic:
use r.ramificationIdx S
  rw [← ramificationIdx_tower]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a}) → x ∈ ⨅ i, i.maxPowDividing (span {a})

Tactic:
simp only [mem_iInf]
      intro h i
      by_cases htop : i.maxPowDividing (span {a}) = ⊤ <;> simp_all [S]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
simp [sInf_def, sSup_empty]

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

Goal state before:
pp: case inl
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ≥0
⊢ motive ↑r

pp: case inr
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ≥0
⊢ motive (-↑r)

Tactic:
all_goals simp_all

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

Goal state before:
pp: case inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
⊢ motive 0

pp: case inr.inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive ↑r

pp: case inr.inr
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive (-↑r)

Tactic:
all_goals simp_all

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

Goal state before:
pp: case hbc
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ p (x✝¹ * x✝) ≤ p x✝¹ + p x✝

Tactic:
apply map_mul_le_add

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

Goal state before:
pp: case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑∞ = x

Tactic:
h_top

Goal state after:
case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑∞ = ⊤
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
cases b
  case top =>
    simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
      mul_top, inv_top, mul_zero]
  cases a
  case top =>
    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
  grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
    =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]

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

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

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

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

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
⊢ x ≤ y

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
  lift r to ℝ≥0 using ne_top_of_lt hr
  exact h r hr

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

Goal state before:
pp: case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton

Tactic:
· rw [closedBall_zero]
    exact subsingleton_singleton

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
⊢ 𝓤 PUnit.{u + 1} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | 0 < ε}

Tactic:
by
    simp +contextual [principal_univ, eq_top_of_neBot (𝓤 PUnit)]

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

Goal state before:
pp: x y : ℝ
⊢ Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)

Tactic:
Real.closedBall_eq_Icc,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc ((x + y) / 2 - (y - x) / 2) ((x + y) / 2 + (y - x) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
exact NNReal.nndist_zero_eq_val z

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ico a b) = Ioo a b

Tactic:
← Ici_inter_Iio,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ici a ∩ Iio b) = Ioo a b
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c

Tactic:
exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2

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
⊢ ‖single i y‖₊ = ‖y‖₊

Tactic:
by
  have H : ∀ b, ‖single i y b‖₊ = single (M := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
    intro b
    refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
    simp
  simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

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

Goal state before:
pp: case inr.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
z : α
zx : z < x
lz : l < f z
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)

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

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| Or.inr ?_

Goal state after:
case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z

Tactic:
exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))

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

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

Tactic:
rw [← dist_one_right, dist_self]

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

Goal state before:
pp: α : 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 : ℕ
⊢ dist (u n) (u N) < ↑R + 1

Tactic:
rcases le_or_gt N n with h | h

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

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.Topology.EMetricSpace.Diam

Goal state before:
pp: case h₁
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x ≤ ediam s

pp: case h₂
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist y b ≤ ediam t

Tactic:
exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]

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

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : EMetricSpace X
⊢ 0 < ediam s ↔ s.Nontrivial

Tactic:
simp only [pos_iff_ne_zero, Ne, ediam_eq_zero_iff, Set.not_subsingleton_iff]

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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : Fact (s ≤ t)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)

Tactic:
have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.domRestrict (Icc s t) f)
      hf_c.continuousOn.domRestrict hf_i.injOn.injective

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this✝ : Fact (s ≤ t)
this : StrictMono ((Icc s t).domRestrict f) ∨ StrictAnti ((Icc s t).domRestrict f)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' closedBall (↑x) r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Tactic:
Real.closedBall_eq_Icc,

Goal state after:
x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' Icc (↑x - r) (↑x + r) = Icc ⌈↑x - r⌉ ⌊↑x + r⌋
Module: Mathlib.Topology.Instances.Int

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

Tactic:
by
  rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
⊢ Dense ↑s ↔ ∀ (a : G), s ≠ zpowers a

Tactic:
by
  simp [xor_iff_iff_not.1 s.dense_xor_cyclic]

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

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ Nat.cast ⁻¹' closedBall (↑x) r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
Real.closedBall_eq_Icc,

Goal state after:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ Nat.cast ⁻¹' Icc (↑x - r) (↑x + r) = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
by
  obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd
  exact IsCobounded.of_frequently_ge <| f_incr.frequently_ge_map_of_frequently_ge hl

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:
simp_rw [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.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝ : ConditionallyCompleteLattice α
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
i : ι'
hi : p i
h'i : s i = ∅
⊢ liminf f v = sSup univ

Tactic:
by
  simp [hv.eq_bot_iff.2 ⟨i, hi, h'i⟩, liminf_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ LocallyLipschitzOn s f ↔ LocallyLipschitz (s.domRestrict f)

Tactic:
simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall',
    lipschitzOnWith_restrict,
    nhds_subtype_eq_comap_nhdsWithin, mem_comap]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ (∀ (x : ↑s), ∃ K, ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔
    ∀ (x : ↑s), ∃ K t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} ↔ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose h

Goal state after:
case refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

case refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : x ∉ t
⊢ t ∉ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

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

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

Tactic:
rw [← add_zero x]
    exact add_lt_add (by grind) (sub_pos.mpr h')

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

Goal state before:
pp: α : Type u_3
⊢ Tendsto Finset.powerset atTop atTop

Tactic:
by
  classical
  refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
  exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
have := hs.toFinset.multipliable f

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this : Multipliable (f ∘ Subtype.val)
⊢ Multipliable (f ∘ Subtype.val)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map f cofinite

Tactic:
rw [Filter.mem_map]

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ f ⁻¹' e ∈ cofinite
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))

Tactic:
simp [comap_comap, Function.comp_def]

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

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

Tactic:
le_zero_iff

Goal state after:
β : Type u_2
inst✝² : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst✝¹ : EMetricSpace α
inst✝ : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K = 0
⊢ K = 0
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inl α β)

Tactic:
by
  intro x y
  rw [Prod.edist_eq]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inr α β)

Tactic:
by
  intro x y
  rw [Prod.edist_eq]
  simp

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed[inst✝²] s

Tactic:
← closure_eq_iff_isClosed,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ closure[inst✝²] s = s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case h.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
z z' : X
hxz : d x z ≤ L.sum
hzz' : d z z' ≤ L.sum
hz'y : d z' y ≤ L.sum
⊢ d x y ≤ 2 * L.sum

Tactic:
hd x z z' y,

Goal state after:
case h.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
z z' : X
hxz : d x z ≤ L.sum
hzz' : d z z' ≤ L.sum
hz'y : d z' y ≤ L.sum
⊢ 2 * max (d x z) (max (d z z') (d z' y)) ≤ 2 * L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ ↑{a | a < ∞} ≃ₜ ℝ≥0

Tactic:
refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ {a | a < ∞} = {a | a ≠ ∞}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)

Tactic:
zero_tsub,

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc 0 (0 + ε)
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
intro l

Goal state after:
case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
l : ℕ
⊢ 0 < l → ‖v l‖ < b l
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + ↑K * (dist y ↑t + dist y z)

Tactic:
add_comm (dist y t)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + ↑K * (dist y z + dist y ↑t)