mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.Rat

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

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

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← ofNNReal_finsetSum, coe_inj]
  exact Real.toNNReal_sum_of_nonneg hf

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
by
  obtain ⟨t, ht⟩ := cobdd
  rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
  · exact ⟨t, .of_forall fun r ↦ tbot r⟩
  refine ⟨t', fun ev ↦ ?_⟩
  specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
  exact not_lt_of_ge ht ht'

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

Goal state before:
pp: y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + t ≤ y + t

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup (u ∘ v) f ≤ limsup u g

Tactic:
rw [limsup_comp]
  exact limsup_le_limsup_of_le hv

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
hb hu

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ q b → u b ≤ a ↔ q b → u b ≤ a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : ℝ
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
rcases le_total 0 x with (h | h)
  · lift x to ℝ≥0 using h
    rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero,
      coe_ennreal_zero, sub_zero]
    rfl
  · rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
      Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]
    exact neg_nonneg.2 h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]

Tactic:
by rw [pow_succ]; exact (LipschitzWith.iterate hf n).comp hf

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

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b - (a + ↑b) = -a

Tactic:
by
  cases a <;> norm_cast
  exact _root_.sub_add_cancel_right _ _

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
refine (edist_triangle _ (f a₂ b₁) _).trans ?_

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
Module: Mathlib.Topology.EMetricSpace.Lipschitz

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

Tactic:
have B : t ∩ { b | edist (f (x', b)) (f (x', y)) ≤ ε / 2 } ∈ 𝓝[t] y :=
    inter_mem self_mem_nhdsWithin (ha x' hx' y hy (Metric.closedEBall_mem_nhds (f (x', y)) ε0))

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

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

Tactic:
by gcongr

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

Goal state before:
pp: ⊢ (conditional ℕ).filter = Filter.map Finset.range atTop

Tactic:
by
  have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ_iff]
  simp only [conditional_filter_eq_map_Iic, funext this]
  apply le_antisymm <;>
      rw [← Tendsto] <;>
      simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage] <;>
      rintro s ⟨a, ha⟩
  · exact ⟨a + 1, fun b hb ↦ ha (b + 1) (by lia)⟩
  · exact ⟨a + 1, fun b hb ↦ by convert! ha (b - 1) (by lia); lia⟩

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f

Tactic:
· exact IsBounded.isBoundedUnder f_decr bdd_above

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, b < a
⊢ liminf f (𝓝[<] a) = ⨆ r, ⨆ (_ : r < a), f r

Tactic:
by
  rw [(nhdsLT_basis_of_exists_lt hb).liminf_eq_iSup_iInf]
  refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
  obtain ⟨b, hb⟩ := exists_between hr
  exact ⟨b, hb.2, iInf₂_le b hb⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
⊢ (s.sup' hs fun i ↦ limsup (F i) f) ≤ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f

Tactic:
· apply Finset.sup'_le hs (fun i ↦ limsup (F i) f)
    refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup
    simp only [le_sup'_iff]
    use i, i_s

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
⊢ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
e

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
⊢ e ∈ 𝓝 1 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
cauchySeq_finset_iff_prod_vanishing,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ 1

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ 1

Tactic:
· exact hf.hasProd.le_one h

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ 1
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 : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
by_cases hf : Summable f L

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : ¬Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: 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

Tactic:
apply p.comp_injective

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
⊢ Injective Nat.cast
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: 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))

Tactic:
apply p.comp_injective

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

Goal state before:
pp: 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)

Tactic:
apply p.comp_injective

Goal state after:
case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n ↦ -↑n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr

Tactic:
cases hn rfl

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 Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hx ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure[inst✝²] s
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
← coe_toNNReal ha

Goal state after:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 ↑a.toNNReal)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Tactic:
exact pkg.isDenseInducing.extend_eq hf.continuous a

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

Goal state before:
pp: case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a

Tactic:
refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_

Goal state after:
case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ ∀ (a : SeparationQuotient α), Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') ↑a) = ↑a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∀ ε > 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:
constructor
  · intro hs
    /- `s` is Cauchy sequence. Let `b n` be the diameter of the set `s '' Set.Ici n`. -/
    refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
    -- Prove that it bounds the distances of points in the Cauchy sequence
    · exact Metric.edist_le_ediam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)
    -- Prove that it tends to `0`, by using the Cauchy property of `s`
    · refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_
      rcases hs ε ε0 with ⟨N, hN⟩
      refine (eventually_ge_atTop N).mono fun n hn => Metric.ediam_le ?_
      rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩
      exact (hN _ (hn.trans hk) _ (hn.trans hl)).le
  · rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
    have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
    rcases this.exists with ⟨N, hN⟩
    refine ⟨N, fun m hm n hn => ?_⟩
    calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ edist x y ≤ ediam s

Tactic:
have : edist x y ∈ closure (Iic (ediam s)) :=
    map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_ediam_of_mem hx hy

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : edist x y ∈ closure (Iic (ediam s))
⊢ edist x y ≤ ediam s
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
⊢ ↑K * dist x y ≤ ↑K * r

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hK : K ≠ 0
hr : dist x y < r
⊢ ↑K * dist x y < ↑K * r

Tactic:
by gcongr

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

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ f i + g i ≤ b + g i

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x ↦ f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
choose g hg using this

Goal state after:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x ↦ f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.1 ≤ p.2} ↔ p ∈ (fun p ↦ p.2 - p.1) ⁻¹' {x | 0 ≤ x}

Tactic:
simp only [sub_nonneg, Set.preimage_ofPred_eq]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
by gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzWith C f
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)

Tactic:
inv_sub_inv' hz hw,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
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
n : ℕ
hn : n ≥ N
⊢ N + 1 ≤ n + 1

Tactic:
by gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
a b : E
r : ℝ
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
by gcongr

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
a b : E
r : ℝ
h : LipschitzWith C f
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
by gcongr

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

Goal state before:
pp: E : Type u_2
inst✝³ : SeminormedGroup E
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : DiscreteTopology X
inst✝ : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) Filter.cofinite atTop

Tactic:
by
  rw [← Filter.cocompact_eq_cofinite X]
  apply tendsto_norm_cocompact_atTop'.comp (Topology.IsClosedEmbedding.tendsto_cocompact he)

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

Goal state before:
pp: a✝ b✝ c✝ d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hab : a ≤ b
c : ℝ≥0
⊢ c • a ≤ c • b

Tactic:
by gcongr

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

Goal state before:
pp: a✝ b✝ c✝ d : ℝ≥0∞
r p q a b : ℝ≥0
hab : a ≤ b
c : ℝ≥0∞
⊢ a • c ≤ b • c

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a‖ * ‖1 - b‖ ≤ ‖c - a‖ + 1 * ‖1 - b‖

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
i : (a : α) → ι a
⊢ ∀ i_1 ∈ Finset.univ, 0 ≤ f i_1 (i i_1)

Tactic:
simp [hf₀]

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

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ 2 * r'

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
i : ℕ
⊢ s i ⊆ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
x

Goal state after:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
⊢ x ∈ s i → x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)