mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n

Tactic:
exact h.comap _

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n

Tactic:
exact h.comap _

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

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n

Tactic:
exact h.comap _

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

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n

Tactic:
exact h.comap _

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

Goal state before:
pp: case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : a ≤ b
⊢ f '' Ico a b = Ico (f a) (f b)

pp: case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : b < a
⊢ f '' Ico a b = Ico (f a) (f b)

Tactic:
· exact hf_c.continuousOn.image_Ico_of_strictMonoOn hab (hf.strictMonoOn _)

Goal state after:
case inr
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : b < a
⊢ f '' Ico a b = Ico (f a) (f b)
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊

Tactic:
rw [floor_natCast, Nat.lt_ceil]
      linarith

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

Goal state before:
pp: ⊢ UniformContinuous (Rat.cast ∘ fun p ↦ p.1 + p.2)

Tactic:
simp only [Function.comp_def, Rat.cast_add]

Goal state after:
⊢ UniformContinuous fun x ↦ ↑x.1 + ↑x.2
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : ∀ k ∈ Finset.cons k₀ s k₀_notin_s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simp only [Finset.forall_mem_cons] at *

Goal state after:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal

Tactic:
try {· simp_all}

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
rw [eventually_map] at hc

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ + ↑a✝).toENNReal = ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
try {· simp_all}

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

Goal state before:
pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal

Tactic:
try {· simp_all}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝ + ⊥).toENNReal = (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
try {· simp_all}

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

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
try {· simp_all}

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
try {· simp_all}

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

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

Tactic:
try {· simp_all}

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

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

Tactic:
try {· simp_all}

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

Goal state before:
pp: case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
try {· simp_all}

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F = sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = -↑(-x)

pp: case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
coe_neg,

Goal state after:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = - -↑x

case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ p ((fun i ↦ g (b ↑i) ⋯) i) ∧ (fun i ↦ g (b ↑i) ⋯) i ∈ b ↑i

Tactic:
exact hg (b i) (hl.mem_of_mem i.2)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c, ∃ (_ : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}), b < c

Tactic:
exists_prop

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}, b < c
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}
⊢ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) ≤
    ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ

Tactic:
gcongr
      · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
      · exact hby
      · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)

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
⊢ f F.limsSup = liminf f F

Tactic:
apply le_antisymm

Goal state after:
case a
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
⊢ f F.limsSup ≤ liminf f F

case a
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
⊢ liminf f F ≤ f F.limsSup
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map (fun x ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop

Tactic:
apply le_antisymm

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map (fun x ↦ Finset.range (x + 1)) atTop ≤ Filter.map Finset.range atTop

case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map Finset.range atTop ≤ Filter.map (fun x ↦ Finset.range (x + 1)) atTop
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop = Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop ≤ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)

case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun a ↦ max (u a) (v a)) f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : 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
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f = s.sup' hs fun i ↦ limsup (F i) f

Tactic:
apply le_antisymm

Goal state after:
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
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f ≤ s.sup' hs fun i ↦ limsup (F i) f

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd (fun x ↦ f ↑((notMemRangeEquiv k).symm x)) g

Tactic:
coe_notMemRangeEquiv_symm

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd (fun x ↦ f ↑((fun j ↦ ⟨j + k, ⋯⟩) x)) g
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
s : Finset β
hf : mulSupport f ⊆ ↑s
⊢ ∏'[L] (b : β), f b = ∏ b ∈ s, f b

Tactic:
rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf]

Goal state after:
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
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
obtain ⟨N, hN⟩ := vanish e he
    exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

Goal state after:
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
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n ↦ f ↑n) ∧ Multipliable fun n ↦ f (-(↑n + 1))

Tactic:
by
  refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;>
  apply p.comp_injective
  exacts [Nat.cast_injective, @Int.negSucc.inj]

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

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

Tactic:
simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 ⊥).HasBasis (fun x ↦ ⊥ < x) fun ε ↦ Iic ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a))

Tactic:
apply continuousOn_sub.comp_continuous (by fun_prop)

Goal state after:
case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ ∀ (x : ℝ≥0∞), (x, a) ∈ {p | p ≠ (∞, ∞)}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
⊢ ∀ x ∈ s '' Ici n, ∀ y ∈ s '' Ici n, edist x y ≤ ε

Tactic:
rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩

Goal state after:
case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
k : β
hk : k ∈ Ici n
l : β
hl : l ∈ Ici n
⊢ edist (s k) (s l) ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖

Tactic:
by
  apply solid
  rw [abs]
  nth_rw 1 [← neg_neg a]
  rw [← neg_inf]
  rw [abs]
  nth_rw 1 [← neg_neg b]
  rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]

Goal state after:
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
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
by rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

Goal state after:
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‖}
hs₀ : ∀ x ∈ s, x ≠ 0
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
refine ⟨ε * r ^ 2, by positivity, fun x hx y hy hxy ↦ ?_⟩

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
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
⊢ Tendsto (fun y ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)

Tactic:
refine Tendsto.comp (uniformContinuousOn_inv₀ (s := (closedBall (0 : α) (r / 2))ᶜ)
    (by simp [closedBall_mem_nhds, hr₀])) <| tendsto_inf.mpr ⟨hF x hx, tendsto_principal.mpr ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
⊢ ∀ᶠ (a : ι × X) in l ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨k, hk⟩ := hu.norm_bddAbove

Goal state after:
case mpr.inr
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‖)
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = ⨆ i, (f i) s

Tactic:
by
  rw [iSup, sSup_apply, iSup_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
by
  have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) := by
    ext1 ⟨x, y⟩
    simp only [mem_preimage, mem_iUnion, mem_prod]
    refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
    rintro ⟨y', hy's, hy'⟩
    rwa [h'f y' y x hy']
  rw [this]
  exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))

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

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    MeasurableSpace.comap (fun b c ↦ g c b) (MeasurableSpace.comap (fun b ↦ b a) (inst✝ a))

Tactic:
measurability

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable fun x ↦ x

Tactic:
exact measurable_id

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

Goal state before:
pp: case refl
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
i : δ
⊢ Measurable ⋯.mp

Tactic:
exact measurable_id

Goal state after:
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 α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), Measurable fun n ↦ n = x

Tactic:
measurability

Goal state after: