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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x

Tactic:
liminf_eq

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
rcases f.eq_or_neBot with rfl | hbot

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)

case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ ∃ c, Tendsto u f (𝓝 c)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
rcases f.eq_or_neBot with rfl | hbot
  · exact ⟨sInf ∅, tendsto_bot⟩
  refine ⟨limsup u f, ?_⟩
  apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'
  by_contra! hlt
  obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s :=
    dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo
      (Set.nonempty_Ioo.2 hlt)
  obtain ⟨b, ⟨⟨ab, bu⟩, bs⟩⟩ : ∃ b, (a < b ∧ b < f.limsup u) ∧ b ∈ s :=
    dense_iff_inter_open.1 hs (Set.Ioo a (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 au)
  have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la
  have B : ∃ᶠ n in f, b < u n := frequently_lt_of_lt_limsup (IsBounded.isCobounded_le h') bu
  exact H a as b bs ab ⟨A, B⟩

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

Goal state before:
pp: α : Type u_3
⊢ atTop = ⨅ x, 𝓟 (Ici {x})

Tactic:
by
  refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_
  refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_
  simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]
  exact fun t => id

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f (map Finset.card atTop) l

Tactic:
tendsto_map'_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto (f ∘ Finset.card) atTop l
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f (map Finset.card atTop) l

Tactic:
tendsto_map'_iff

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto (f ∘ Finset.card) atTop l
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
le_iff_lt_or_eq,

Goal state after:
a b : EReal
⊢ 0 < a * b ∨ 0 = a * b ↔ (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)

Tactic:
exact neg_mul _ _

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case h₂
α : 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 : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
· apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminfReparam f s p j)

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

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
rcases eq_or_lt_of_le hx with (hx | hx)
    · simp [← hx]
    · simp_all [mul_top_of_pos hx]

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 : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Tendsto (fun x ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
refine tendsto_congr fun s ↦ ?_

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

Goal state before:
pp: case e_s
α : 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}
hs' : s ∈ ⋂ b ∈ L.supportᶜ, {s | b ∉ s}
⊢ s = L.support.toFinset

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq, Set.mem_compl_iff] at hs hs'

Goal state after:
case e_s
α : 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 : ∀ i ∈ L.support, i ∈ s
hs' : ∀ i ∉ L.support, i ∉ s
⊢ s = L.support.toFinset
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: 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₂ : α
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Tactic:
convert! rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂
  · simp only [iSup_bool_eq, cond]
  · rw [tprod_fintype, Fintype.prod_bool, cond, cond]

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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : Nonempty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

Tactic:
obtain ⟨x, hx⟩ := hprod

Goal state after:
case inr
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
h✝ : Nonempty ι
x : α
hx : HasProd (fun x ↦ 1 + f x) x
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'

Tactic:
uIcc_comm

Goal state after:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc x' y'
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'

Tactic:
uIcc_comm

Goal state after:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc x' y'
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
by
  simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
  norm_cast

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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse ([x] ++ l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
singleton_append,

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
x y : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse (x :: l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case h
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
n : ℕ
ihn : ∀ m < n, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
x y : X
l : List X
hn : l.length = n
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
subst n

Goal state after:
case h
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
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (map ofNNReal (𝓝 x)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l

Tactic:
tendsto_map'_iff

Goal state after:
α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto (f ∘ ofNNReal) (𝓝 x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (map ofNNReal (𝓝 a)) (𝓝 (↑a).toNNReal)

Tactic:
tendsto_map'_iff

Goal state after:
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
by
  simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt

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

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
| ε

Tactic:
← mul_one ε

Goal state after:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
| ε * 1
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ Tendsto (fun b ↦ f a✝ b * ∏ c ∈ s✝, f c b) x (𝓝 (a a✝ * ∏ c ∈ s✝, a c))

Tactic:
apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))

Goal state after:
case insert.ha
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ a a✝ ≠ 0 ∨ ∏ c ∈ s✝, a c ≠ ∞

case insert.hmb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ Tendsto (fun a ↦ ∏ c ∈ s✝, f c a) x (𝓝 (∏ c ∈ s✝, a c))

case insert.hb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ ∏ c ∈ s✝, a c ≠ 0 ∨ a a✝ ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (a, x)) {x | x ≠ ∞}

Tactic:
apply continuousOn_sub.comp (by fun_prop)

Goal state after:
a : ℝ≥0∞
⊢ MapsTo (fun x ↦ (a, x)) {x | x ≠ ∞} {p | p ≠ (∞, ∞)}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ Continuous fun x ↦ x - a

Tactic:
by
  by_cases a_infty : a = ∞
  · simp [a_infty, continuous_const, tsub_eq_zero_of_le]
  · rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
    apply continuousOn_sub.comp_continuous (by fun_prop)
    intro x
    simp only [a_infty, Ne, mem_ofPred_eq, Prod.mk_inj, and_false, not_false_iff]

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

Goal state before:
pp: E : Type u_4
inst✝ : NormedGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
apply (tendsto_norm_inv_mul_self a).inf
  apply tendsto_principal_principal.2 (fun _x hx => norm_pos_iff'.2 ?_)
  simpa [inv_mul_eq_one] using hx

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)
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)

Tactic:
have key := Monotone.map_liminf_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
          (continuous_truncateToReal b_ne_top).continuousAt
          (IsBoundedUnder.isCoboundedUnder_ge ⟨b, by simpa only [eventually_map] using le_b⟩)
          ⟨0, Eventually.of_forall (by simp)⟩

Goal state after:
ι : 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)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ min a (f x)

Tactic:
simpa [min_comm] using (hf.min_const a)

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

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

Tactic:
← dist_mul_right _ _ b,

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist (a / b * b) (c * b) = dist a (c * b)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)

Tactic:
have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
    intro n
    rw [add_comm]
    refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_
    simp [(hC _ _).le]

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑r * dist x y = ↑r * ↑(nndist x y)

Tactic:
coe_nndist

Goal state after:
α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑r * dist x y = ↑r * dist x y
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑r * dist x y = ↑r * ↑(nndist x y)

Tactic:
coe_nndist

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑r * dist x y = ↑r * dist x y
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
s : Set α
⊢ ediam (⇑f '' s) = ↑(ratio f) * ediam s

Tactic:
refine ((lipschitz f).ediam_image_le s).antisymm ?_
  apply ENNReal.mul_le_of_le_div'
  rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
  exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

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

Goal state before:
pp: case mk
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
this : List.map f l ≠ []
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Tactic:
simpa using! List.norm_prod_le' this

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

Goal state before:
pp: K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ ≤ ‖x‖

Tactic:
exact hx.le.trans' (hk (by simp))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n‖ * ‖x‖

Tactic:
rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
⊢ NoncompactSpace E

Tactic:
by_cases! H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1
  · let := NontriviallyNormedField.ofNormNeOne H
    exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩
  · rcases exists_ne (0 : E) with ⟨x, hx⟩
    suffices IsClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace
    refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_
    simp only [dist_eq_norm, ← sub_smul, norm_smul]
    rw [H, one_mul]
    rwa [sub_ne_zero, (Embedding.injective _).ne_iff]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
rcases hyf with ⟨y, rfl⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : β
hy : f y ∈ s
⊢ MeasurableSet (f ⁻¹' {f y})
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x = measurableAtom y

Tactic:
by
  refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_
  by_cases hy : y ∈ measurableAtom x
  · exact measurableAtom_subset_of_mem hy
  exfalso
  simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢
  obtain ⟨s, hxs, hs, hys⟩ := hy
  specialize hx sᶜ hys hs.compl
  exact hx hxs

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)

Tactic:
by
  simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0

Goal state after: