mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case hb
α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s = ∞ → ediam (s ∪ t) = ∞

Tactic:
exact fun h ↦ top_unique <| h ▸ ediam_mono subset_union_left

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ a ^ (n + 1) ≤ a ^ (m + 1)

Tactic:
grw [hnm]

Goal state after:
case ha
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ 1 ≤ a
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
· obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
    exact tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

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

Goal state before:
pp: a b : EReal
⊢ -a ≤ b ↔ -b ≤ a

Tactic:
← neg_le_neg_iff,

Goal state after:
a b : EReal
⊢ -b ≤ - -a ↔ -b ≤ a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a ≤ -b ↔ b ≤ -a

Tactic:
← neg_le_neg_iff,

Goal state after:
a b : EReal
⊢ - -b ≤ -a ↔ b ≤ -a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
n : ι
hna : u n ≤ a
hbn : b ≤ u n
⊢ b ≤ a

Tactic:
exact hbn.trans hna

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

Goal state before:
pp: a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ c ≤ a + b

Tactic:
← neg_le_neg_iff,

Goal state after:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -(a + b) ≤ -c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
⊢ ↑x * ⊤ = ⊤

Tactic:
by
  rw [EReal.mul_comm, top_mul_coe_ennreal hx]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset α)
⊢ s ∈ atTop → s ∈ map Finset.toLeft atTop

Tactic:
hs

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : s ∈ atTop
⊢ s ∈ map Finset.toLeft atTop
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset β)
⊢ s ∈ atTop → s ∈ map Finset.toRight atTop

Tactic:
hs

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ map Finset.toRight atTop
Module: Mathlib.Order.Filter.AtTopBot.Finset

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

Tactic:
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.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ ¬a * b = ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
mul_eq_bot

Goal state after:
a b : EReal
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

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

Tactic:
simp [tprod_def, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
⊢ ↑s ⊆ L.support → ∏ x ∈ s.preimage g ⋯, f (g x) = ∏ b ∈ s, f b

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : ↑s ⊆ L.support
⊢ ∏ x ∈ s.preimage g ⋯, f (g x) = ∏ b ∈ s, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

Tactic:
simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]
  refine tendsto_congr' ?_
  filter_upwards [L.eventually_le_support] with s hs
  rw [s.prod_preimage]
  exact fun x h h' ↦ hf x (hs h) h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter
s : Finset β
⊢ s ∈ ⋂ b ∈ L.support, {s | b ∈ s} → s ∈ ⋂ b ∈ L.supportᶜ, {s | b ∉ s} → ∏ b ∈ s, f b = ∏ b ∈ L.support.toFinset, f b

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter
s : Finset β
hs : s ∈ ⋂ b ∈ L.support, {s | b ∈ s}
⊢ s ∈ ⋂ b ∈ L.supportᶜ, {s | b ∉ s} → ∏ b ∈ s, f b = ∏ b ∈ L.support.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
by
  rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ ∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (b : β), m (s b)

Tactic:
rw [← tprod_extend_one (@encode_injective β _)]
  refine tprod_congr fun n ↦ ?_
  rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
  · simp [encode_injective.extend_apply]
  · rw [extend_apply' _ _ _ hn]
    rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
    simp [hn, m0]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L

Tactic:
classical
  exact Finset.induction_on s (by simp) <| by
    simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
    exact fun x s _ IH hx h ↦ hx.mul (IH h)

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

Goal state before:
pp: case e'_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ s₁ ⊔ s₂ = ⨆ b, bif b then s₁ else s₂

Tactic:
simp only [iSup_bool_eq, cond]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (x : β), f x = ∏' (x : ↑(mulSupport g)), g ↑x

Tactic:
← hi.tprod_eq hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x
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
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ Multipliable fun n ↦ f ↑↑n

Tactic:
multipliable_pnat_iff_multipliable_succ (f := (f ·)),

Goal state after:
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ Multipliable fun x ↦ f ↑(x + 1)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
simp only [bot_lt_iff_ne_bot]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
s : Finset β
⊢ {b} ⊆ s → 0 = ∏ b ∈ s, f b

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
s : Finset β
hs : {b} ⊆ s
⊢ 0 = ∏ b ∈ s, f b
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this✝ : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, y n_1 ∈ closure[inst✝¹] {x (φ n)}
ψ : ℕ → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), y (ψ n) ∈ closure[inst✝¹] {x (φ n)}
this : Tendsto ψ atTop atTop
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this✝ : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, y n_1 ∈ closure[inst✝¹] {x (φ n)}
ψ : ℕ → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), y (ψ n) ∈ closure[inst✝¹] {x (φ n)}
this : Tendsto ψ atTop atTop
n : ℕ
⊢ (x ∘ φ) n ⤳ (y ∘ ψ) n
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, y) ∈ t N ×ˢ t N

Tactic:
exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b

Tactic:
by simpa only [eventually_map] using le_b

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b

Tactic:
by simpa only [eventually_map] using le_b

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
⊢ LipschitzOnWith K f s

Tactic:
by
  simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_sphere]

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Tactic:
by
  simpa using norm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot

Tactic:
by
  rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
  rintro ε ε0
  rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
  refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩
  rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
⊢ ∃ x, c < ‖x‖

Tactic:
by
  rcases exists_ne (0 : E) with ⟨x, hx⟩
  rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
  use r • x
  rwa [norm_smul, ← div_lt_iff₀]
  rwa [norm_pos_iff]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet {x | Nat.findGreatest (p x) N = k}

Tactic:
simp only [Nat.findGreatest_eq_iff, ofPred_and, ofPred_forall, ← compl_ofPred]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ i, ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a | p a i}ᶜ))
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ ∑' (i : ℕ), μ (disjointed t i) ≤ ∑' (i : ℕ), μ (t i)

Tactic:
by gcongr; exact disjointed_subset ..

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet (⋂ y ∈ (measurableAtom x)ᶜ, s y)

Tactic:
exact MeasurableSet.biInter (to_countable (measurableAtom x)ᶜ) (fun i hi ↦ (hs i hi).2.1)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y z : β
hz : ∀ (i : Set β), x ∈ i → MeasurableSet i → z ∈ i
hx : ∀ (i : Set β), y ∈ i → MeasurableSet i → x ∈ i
⊢ ∀ (i : Set β), y ∈ i → MeasurableSet i → z ∈ i

Tactic:
exact fun s hys hs ↦ hz s (hx s hys hs) hs

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (s.pi t)

Tactic:
by
  rw [pi_def]
  exact MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∃ i, p i a}

Tactic:
ofPred_exists

Goal state after:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), ↑(f b) ≠ ∞ ↔ Summable f

Tactic:
refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩

Goal state after:
β : Type u_2
f : β → ℝ≥0
h : ∑' (b : β), ↑(f b) ≠ ∞
⊢ Summable f
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b

Tactic:
← neg_le_neg_iff,

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -(c * b) ≤ -(c * a)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -(b⁻¹ * a) ≤ -(b⁻¹ * a')

Tactic:
← neg_mul b⁻¹ a,

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -b⁻¹ * a ≤ -(b⁻¹ * a')
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Tactic:
rw [mul_div b a b, mul_comm a b]

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
· refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
⊢ False

case refine_2
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Nonempty → ⊤ s ≤ ⊤ s

Tactic:
hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2

Tactic:
have a2_pos : 0 < ((a / 2 : ℝ) : EReal) := by rw [EReal.coe_pos]; linarith

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
⊢ ↑x < p.1 * p.2
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z ↦ ∑ i ∈ a, f i z) s x

Tactic:
induction a using Finset.induction_on with

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
⊢ s ∈ insert ∅ S → ∀ t ∈ insert ∅ S, (s ∩ t).Nonempty → s ∩ t ∈ insert ∅ S

Tactic:
hs

Goal state after:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
⊢ ∀ t ∈ insert ∅ S, (s ∩ t).Nonempty → s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
⊢ s ∈ insert univ S → ∀ t ∈ insert univ S, (s ∩ t).Nonempty → s ∩ t ∈ insert univ S

Tactic:
hs

Goal state after:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
⊢ ∀ t ∈ insert univ S, (s ∩ t).Nonempty → s ∩ t ∈ insert univ S
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ Continuous[inst✝³, inst✝¹] f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f

Tactic:
simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]

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

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
⊢ s ⊆ t → (inducedOuterMeasure m P0 m0) s ≤ m t ht

Tactic:
hs

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure m P0 m0) s ≤ m t ht