mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mpr.inl
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)

Tactic:
exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ (map f (map (fun i ↦ i + k) atTop)).limsInf = (map f atTop).limsInf

Tactic:
map_add_atTop_eq_nat

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ (map f atTop).limsInf = (map f atTop).limsInf
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : ι → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
induction ι using Finite.induction_empty_option with

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ limsup s cofinite = {x | {n | x ∈ s n}.Infinite}

Tactic:
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
rw [if_neg H']

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
by
  rw [← hg.hasProd_iff, extend_comp hg]
  exact extend_apply' _ _

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

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g 1 = 1

pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ ¬Multipliable (fun i ↦ g (f i)) L

Tactic:
map_one

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ 1 = 1

case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ ¬Multipliable (fun i ↦ g (f i)) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ (i : { x // x ∈ β }), f ↑i ≤ f ↑i

Tactic:
by simp only [le_refl, implies_true]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
· rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
⊢ Tendsto (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Tactic:
intro e

Goal state after:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
⊢ e ∈ 𝓝 1 → e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop
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
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
ht : t ⊆ {n | (if h : s.Nonempty then s.max' h + 1 else 0) ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

Tactic:
split_ifs at ht with h

Goal state after:
case pos
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : s.Nonempty
ht : t ⊆ {n | s.max' h + 1 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

case neg
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : ¬s.Nonempty
ht : t ⊆ {n | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s
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
⊢ Tendsto f cofinite (𝓝 1)

Tactic:
intro e

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
⊢ e ∈ 𝓝 1 → e ∈ Filter.map f cofinite
Module: Mathlib.Topology.Instances.NNReal.Lemmas

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

Tactic:
by cases n; (· cases hn rfl); · ext (_ | _) <;> rfl

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
⊢ d a c = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
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₄))
x y : X
l : List X
a b c : X
hab : d a b = 0
hbc : d b c = 0
⊢ d a c ≤ 0
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (uncurry (pkg.extend₂ pkg' f))

Tactic:
AbstractCompletion.extend₂,

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (uncurry (Function.curry ((pkg.prod pkg').extend (uncurry f))))
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
    uniformity_lift_le_swap
      (monotone_principal.comp
        (monotone_ofPred fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
      (by
        have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
        simp only [Function.comp, h, mem_map, f]
        exact le_rfl)

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

Tactic:
refine fun hcon => hbdd ↑(q - 1) ?_

Goal state after:
case inr.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i ↦ x i < ↑(q - 1)) x_1
⊢ ∀ᶠ (a : ι) in l, ↑(q - 1) ≤ x a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
a b : ℝ
h : a < b
⊢ ENNReal.ofReal (sSup (Ioo a b) - sInf (Ioo a b)) = ENNReal.ofReal (b - a)

Tactic:
csSup_Ioo h,

Goal state after:
case inr
a b : ℝ
h : a < b
⊢ ENNReal.ofReal (b - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
refine mul_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Goal state after:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
⊢ ∀ᶠ (a : ι) in f, c < (u * v) a
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
⊢ LipschitzWith (LipschitzMul.C β) fun p ↦ p.1 * p.2

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
x₁ x₂ y₁ y₂ : ↥s
⊢ edist ((fun p ↦ p.1 * p.2) (x₁, x₂)) ((fun p ↦ p.1 * p.2) (y₁, y₂)) ≤ ↑(LipschitzMul.C β) * edist (x₁, x₂) (y₁, y₂)
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzAdd.C ℝ) fun p ↦ p.1 + p.2

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist ((fun p ↦ p.1 + p.2) (x₁, x₂)) ((fun p ↦ p.1 + p.2) (y₁, y₂)) ≤ ↑(LipschitzAdd.C ℝ) * edist (x₁, x₂) (y₁, y₂)
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧ dist (F n y) 0 < C + 1 ∧ dist (G n y) 0 < C + 1

Tactic:
grw [dist_triangle_left (F n y) 0 (f y), dist_triangle_left (G n y) 0 (g y)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧
    dist (f y) (F n y) + dist (f y) 0 < C + 1 ∧ dist (g y) (G n y) + dist (g y) 0 < C + 1
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = ‖b‖

Tactic:
by
  rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (a / b) a = ‖b‖

Tactic:
by
  rw [dist_comm, dist_self_div_right]

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist x y ≤ dist (f x * g x) (f y * g y) / ↑(Kf⁻¹ - Kg)

Tactic:
rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist x y * ↑(Kf⁻¹ - Kg) ≤ dist (f x * g x) (f y * g y)
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖

Tactic:
intro e

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ ↑(ratio f) * edist y x ≤ ↑(ratio f) * r'

Tactic:
gcongr; exact hy

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x < ε ∧ s • x_1 = p) → dist p (s • x) < ‖s‖ * ε

pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) < ‖s‖ * ε → ∃ x_1, dist x_1 x < ε ∧ s • x_1 = p

Tactic:
· rintro ⟨y, h1, rfl⟩
    simpa [dist_smul₀] using mul_lt_mul_of_pos_left h1 (norm_pos_iff.mpr hs)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) < ‖s‖ * ε → ∃ x_1, dist x_1 x < ε ∧ s • x_1 = p
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun x ↦ s • x) '' closedBall x ε = closedBall (s • x) (‖s‖ * ε)

Tactic:
ext p
  simp_rw [Set.mem_image, mem_closedBall]
  constructor
  · rintro ⟨y, h1, rfl⟩
    simpa [dist_smul₀] using mul_le_mul_of_nonneg_left h1 (norm_nonneg s)
  · refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
    refine le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)
    rw [← dist_smul₀]
    simpa [smul_smul, hs] using h

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case fst
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.elim ⋯ = w.1

Tactic:
hvw,

Goal state after:
case fst
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ w.elim ⋯ = w.1
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ v.elim ⋯ = TProd.elim w.2 hj

Tactic:
hvw,

Goal state after:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ w.elim ⋯ = TProd.elim w.2 hj
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
have hs₀ : ∀ x ∈ s, x ≠ 0 := fun x hx ↦ norm_pos_iff.mp <| hr₀.trans_le (hr hx)

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]
    refine Or.inl ⟨1, zero_lt_one, ?_⟩
    contrapose! H
    refine H.imp ?_
    -- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
    simp +contextual [ne_of_lt]

Goal state after:
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n = ↑0 ↔ n = 0

Tactic:
toENNReal_inj

Goal state after:
n : ℕ∞
⊢ n = 0 ↔ n = 0
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 : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
rcases Nat.findX this with ⟨j, hj, hlt⟩

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 : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ {s | ↑s ∈ {↑S}} = {S}

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ toSpanSingleton R 1 = algebraMapCLM R A

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
⊢ sign a = -1 ↔ a < 0

Tactic:
refine ⟨fun h => ?_, fun h => sign_neg h⟩
  rw [sign_apply] at h
  split_ifs at h
  assumption

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
by
  rw [← hasSum_iff_tendsto_nat]
  exact ENNReal.summable.hasSum

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

Goal state before:
pp: f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]

Goal state after:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: r : ℝ
f : ℕ → ℝ≥0
⊢ HasSum (fun i ↦ ↑(f i)) r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (fun i ↦ ↑(f i)) i) atTop (𝓝 r)

Tactic:
simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']

Goal state after:
r : ℝ
f : ℕ → ℝ≥0
⊢ (∃ (hx : 0 ≤ r), Tendsto (fun a ↦ ∑ i ∈ a, f i) (SummationFilter.unconditional ℕ).filter (𝓝 ⟨r, hx⟩)) ↔
    ∃ (hx : 0 ≤ r), Tendsto (fun a ↦ ∑ i ∈ Finset.range a, f i) atTop (𝓝 ⟨r, hx⟩)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
a' : EReal
ha' : c / b < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
exact ⟨a', ⟨(div_nonneg hc b0.le).trans_lt ha', aa'⟩, (div_lt_iff b0 b_top).1 ha'⟩

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_
  rcases lt_or_ge d 0 with d0 | d0
  · exact d0.le.trans hc
  obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab
  obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab
  exact dab.le.trans (h a' aa' b' bb')

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ ≤ 0