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

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → x + ε < u b
⊢ ∃ n, x + ε < u ↑n

Tactic:
obtain ⟨n, hn⟩ := h

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → x + ε < u b
⊢ ∃ n, x + ε < u ↑n
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : x < 0
⊢ x * ⊥ = ⊤

Tactic:
exact mul_bot_of_neg h

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this✝ : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
this : ∃ a, ∀ (b : α), a ≤ b → u n b ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''

Tactic:
rcases this with ⟨r, hr⟩

Goal state after:
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r✝ : α
hr✝ : ∀ s ≥ r✝, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r✝ ≤ b''
n : ι
r : α
hr : ∀ (b : α), r ≤ b → u n b ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''
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
⊢ ContinuousOn f (s ×ˢ t)

Tactic:
by
  rintro ⟨x, y⟩ ⟨hx : x ∈ s, hy : y ∈ t⟩
  refine Metric.nhds_basis_closedEBall.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_
  replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
  obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
    ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'
  rw [← ENNReal.coe_pos] at δpos
  rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩
  have A : s ∩ Metric.eball x δ ∈ 𝓝[s] x :=
    inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ δpos)
  have B : t ∩ { b | edist (f (x', b)) (f (x', y)) ≤ ε / 2 } ∈ 𝓝[t] y :=
    inter_mem self_mem_nhdsWithin (ha x' hx' y hy (Metric.closedEBall_mem_nhds (f (x', y)) ε0))
  filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
  calc
    edist (f (a, b)) (f (x, y)) ≤ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) +
        edist (f (x', y)) (f (x, y)) := edist_triangle4 _ _ _ _
    _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
      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)
    _ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves _

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.LeAtTop

Tactic:
have hLs : L.support = Set.univ := by
    simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]
  exact ⟨L.support_eq_univ_iff.mp hLs⟩

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 α
f : β → α
a : α
L : SummationFilter γ
g : γ → β
hg : Injective g
⊢ HasProd f a (L.map { toFun := g, inj' := hg }) ↔ HasProd (f ∘ g) a L

Tactic:
by
  simp [HasProd, Function.comp_def]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
⊢ ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

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

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

Tactic:
· exact hg.hasProd.one_le h

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : ¬L.NeBot
⊢ 1 ≤ ∏'[L] (i : ι), g i
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
⊢ a * x = a' * f b

Tactic:
have h := hf.mul (hasProd_ite_eq b x L)

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ a * x = a' * f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
b' : β
hb' : b' ∉ {b}
⊢ b' ≠ b

Tactic:
simpa using hb'

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

Goal state before:
pp: case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

pp: case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
· rw [disjoint_iff_inf_le]
      rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩

Goal state after:
case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
codisjoint_iff_le_sup

Goal state after:
case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ ⊤ ⊆ Set.range Nat.cast ⊔ Set.range Int.negSucc
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
n✝ : ℕ
α : Type u_2
L : SummationFilter α
n : ℕ
hn : n ≠ 0
⊢ Tendsto (id ^ n) atBot atBot

Tactic:
by
      simpa [OrderBot.atBot_eq, pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

Tactic:
rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]

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

Goal state before:
pp: case inr.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ i, (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)

Tactic:
exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

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

Goal state before:
pp: a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 0)

Tactic:
refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)

Goal state after:
a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ∞), x.1 - x.2 = 0
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
· obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf
    obtain ⟨q, hq⟩ := exists_rat_lt R
    refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
    · simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q - 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx
    · refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)

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

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' ≤ edist (x, y) (x', y')

Tactic:
apply_rules [le_max_left, le_max_right]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist y y' ≤ edist (x, y) (x', y')

Tactic:
apply_rules [le_max_left, le_max_right]

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

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
x y : X
⊢ d x y = d y x

Tactic:
simp only [d, (U _).comm]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ r ≤ liminf u f ↔ ↑r ≤ liminf (fun i ↦ ↑(u i)) f

Tactic:
le_liminf_iff,

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ↑r ≤ liminf (fun i ↦ ↑(u i)) f
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y z : R
⊢ v (-x + z) ≤ v (-x + y) + v (-y + z)

Tactic:
simpa [neg_add_eq_sub, add_comm (v (y - x))] using v.sub_le z y x

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
⊢ updateFinset x s (s.restrict x) = x

Tactic:
ext i
  simp [updateFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
S : Set α
hS : MeasurableSet S
⊢ MeasurableSet S

Tactic:
rw [map_def, measurableSet_comap] at hS

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
S : Set α
hS : ∃ s', MeasurableSet s' ∧ g ⁻¹' s' = g ⁻¹' S
⊢ MeasurableSet S
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖

Tactic:
rw [norm_algebraMap, norm_one, mul_one]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k ↦ μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) = ⨆ n, μ (s n)

Tactic:
refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _
  set S := ⋃ n, s n
  set M := ⨆ n, μ (s n)
  have A : ∀ k, μ S ≤ M + μ (S \ s k) := fun k ↦ calc
    μ S ≤ μ (S ∩ s k) + μ (S \ s k) := measure_le_inter_add_sdiff _ _ _
    _ ≤ μ (s k) + μ (S \ s k) := by gcongr; apply inter_subset_right
    _ ≤ M + μ (S \ s k) := by gcongr; exact le_iSup (μ ∘ s) k
  have B : Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M) := by simpa using tendsto_const_nhds.add h0
  exact ge_of_tendsto' B A

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

Goal state before:
pp: α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ((map f) ma) s ≤ ((restrict (range f)) mb) s

Tactic:
simpa using h (s ∩ range f)

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Tactic:
· exact Nat.div_mul_le_self m _

Goal state after:
case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ x = y

Tactic:
← x.sign_mul_abs,

Goal state after:
case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign x) * ↑x.abs = y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
h : x ≤ y
hs : sign x = sign y
⊢ sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
    sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
← x.sign_mul_abs,

Goal state after:
case mp
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ y
hs : sign x = sign y
⊢ sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
    sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ x ≤ y

Tactic:
← x.sign_mul_abs,

Goal state after:
case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ x ≤ y

Tactic:
← x.sign_mul_abs,

Goal state after:
case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ x ≤ y

Tactic:
← x.sign_mul_abs,

Goal state after:
case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a * c / (b * c) = a / b

Tactic:
← mul_div_right a (b * c) c,

Goal state after:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a / (b * c) * c = a / b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ a = a'

Tactic:
← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h),

Goal state after:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ b * (a / b) = a'
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ (i : EReal), ⊥ < i → ∃ i', True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ

Tactic:
simp only [EReal.image_coe_Iic,
      true_and]

Goal state after:
case h
⊢ ∀ (i : EReal), ⊥ < i → ∃ i', Ioc ⊥ ↑i' ⊆ Iic i ∩ {⊥}ᶜ
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x

Tactic:
intro y hy

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuousWithinAt (fun z ↦ f z + g z) s x

Tactic:
intro y hy

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
c_ab : c > a * b
⊢ ∃ᶠ (a : α) in f, (u * v) a < c

Tactic:
refine (((frequently_lt_of_liminf_lt) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and
    <| hu.and hv).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
c_ab : c > a * b
x : α
x✝ : v x < b ∧ u x < a ∧ 0 x ≤ u x ∧ 0 x ≤ v x
x_v : v x < b
x_u : u x < a
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x < c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
A : Summable fun i ↦ if n ≤ i then 2⁻¹ ^ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Tactic:
have B : ((Finset.range n).sum fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
    Finset.sum_eq_zero fun i hi ↦
      ite_eq_right_iff.2 fun h ↦ (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim

Goal state after:
n : ℕ
A : Summable fun i ↦ if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i ∈ Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
by
  rcases lt_or_gt_of_ne h with a_neg | a_pos
  · exact neg_neg a ▸ continuousAt_mul_symm2 (continuousAt_mul_top_pos (neg_pos.2 a_neg))
  · exact continuousAt_mul_top_pos a_pos

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt (fun x ↦ min (f x) (g x)) a

Tactic:
by
  rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact hf.inf hg

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
intro y hy

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : (fun x' ↦ ⨆ i, f i x') x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x' ↦ ⨆ i, f i x') x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' ↦ ∑' (i : ι), f i x') x

Tactic:
by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact lowerSemicontinuousWithinAt_tsum h

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
⊢ ∀ t ∈ ⋃ n, p n, (t1 ∩ t).Nonempty → t1 ∩ t ∈ ⋃ n, p n

Tactic:
t2

Goal state after:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
⊢ t2 ∈ ⋃ n, p n → (t1 ∩ t2).Nonempty → t1 ∩ t2 ∈ ⋃ n, p n