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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s

Tactic:
refine ⟨v, hv, ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ Tendsto v atTop (𝓝 x)
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
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩

Goal state after:
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 ∈ s, l ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
⊢ HasProd f a

Tactic:
apply le_nhds_of_cauchy_adhp h

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
⊢ ClusterPt a (Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] f

Tactic:
refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
h✝ : F.NeBot
⊢ limsup (fun i ↦ c - f i) F = c - liminf f F

Tactic:
exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

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 (fun i ↦ (u i).toReal) f = (liminf u f).toReal

Tactic:
have liminf_le : f.liminf u ≤ b := by
    apply liminf_le_of_le ⟨0, by simp⟩
    intro y h
    obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
    exact hi.1.trans hi.2
  have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
  have aux' : (f.liminf u).toReal = ENNReal.truncateToReal b (f.liminf u) := by
    rw [truncateToReal_eq_toReal b_ne_top liminf_le]
  simp_rw [liminf_congr aux, aux']
  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)⟩
  rw [key]
  rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
⊢ f z - ↑K * dist y z ∈ lowerBounds (range fun x ↦ f ↑x + ↑K * dist y ↑x)

Tactic:
rintro w ⟨t, rfl⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ (fun x ↦ f ↑x + ↑K * dist y ↑x) t
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x y₁ y₂ : ℝ
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa [Real.dist_eq, mul_sub] using (abs_mul x (y₁ - y₂)).le

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a✝ b✝ : E
r : ℝ
a b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a✝ a : α
ha : a ≠ 0
x y : α
⊢ edist (a * x) (a * y) = ↑‖a‖₊ * edist x y

Tactic:
by
    simp [edist_nndist, nndist_eq_nnnorm, ← mul_sub]

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ∞ = if c = 0 then 0 else ∞

Tactic:
← smul_one_mul,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • 1 * ∞ = if c = 0 then 0 else ∞
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ‖↑x‖₊ = x

Tactic:
by ext; simp [nnnorm]

Goal state after:
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 G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ContinuousOn f s
hg : ContinuousOn g s
hg₀ : ∀ x ∈ s, g x ≠ 0
⊢ TendstoLocallyUniformlyOn (F / G) (f / g) l s

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ContinuousOn f s
hg : ContinuousOn g s
hg₀ : ∀ x ∈ s, g x ≠ 0
⊢ TendstoLocallyUniformlyOn (F * G⁻¹) (f * g⁻¹) l s
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
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hg₀ : ∀ (x : X), g x ≠ 0
⊢ TendstoLocallyUniformly (F / G) (f / g) l

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hg₀ : ∀ (x : X), g x ≠ 0
⊢ TendstoLocallyUniformly (F * G⁻¹) (f * g⁻¹) l
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ IsCountablySpanning (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ ⋃ n, (fun n ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n = univ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ (Finset.univ.sup fun b ↦ ‖(a • f) b‖₊) ≤ ‖a‖₊ * Finset.univ.sup fun b ↦ ‖f b‖₊

Tactic:
NNReal.mul_finset_sup

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ (Finset.univ.sup fun b ↦ ‖(a • f) b‖₊) ≤ Finset.univ.sup fun a_1 ↦ ‖a‖₊ * ‖f a_1‖₊
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
⊢ False

Tactic:
have h1 := measurableAtom_eq_of_mem hzx

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
⊢ False
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) pi

Tactic:
simpa only [pi, comap_iSup] using le_iSup_of_le a <| by measurability

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp [Nat.cast_nonneg]

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

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) (∑' (b : β), ↑(f b))

Tactic:
exact ENNReal.summable.hasSum

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, (fun t ↦ ∑ a ∈ t, f a) (s i) = ⨆ s, ∑ a ∈ s, f a

Tactic:
exact (Finset.sum_mono_set f).iSup_comp_eq hs

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

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

Tactic:
exact ENNReal.summable.hasSum

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)

Tactic:
exact ENNReal.summable.hasSum

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf

Goal state after:
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), (fun i ↦ ↑(f i)) ↑b) atTop (𝓝 0)
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
simp_rw [lowerHemicontinuous_iff, lowerHemicontinuousAt_iff_frequently]

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

Goal state before:
pp: case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
⊢ sf < sg

Tactic:
lift f to α → ℝ≥0 using fun x =>
      ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))

Goal state after:
case neg
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
f : α → ℝ≥0
h : ∀ (a : α), (fun i ↦ ↑(f i)) a ≤ g a
hi : (fun i ↦ ↑(f i)) i < g i
hf : HasSum (fun i ↦ ↑(f i)) sf
⊢ sf < sg
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h' : ¬↑a = ⊤
h : 0 < a
⊢ 0 < a⁻¹

Tactic:
exact inv_pos_of_pos h

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (i : α), ↑(f i).toNNReal < ∞

Tactic:
rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun i ↦ (f i).toNNReal
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
  · rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

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

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun x ↦ ENNReal.ofReal x.toReal) x

Tactic:
h_bot,

Goal state after:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 ⊥, ENNReal.ofReal x'.toReal = (fun x ↦ ENNReal.ofReal x.toReal) ⊥
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
by
  simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
    using Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))

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

Goal state before:
pp: α : Type u_4
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌈↑x⌉₊

Tactic:
simp only [Nat.ceil_natCast, le_refl]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
⊢ f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
rw [← Set.preimage_inter] at hst ⊢

Goal state after:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    rw [le_div_iff₀ (zero_lt_one.trans_le hx)]
    exact Nat.le_ceil _

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ trim 0 = 0

Tactic:
ext s
  exact nonpos_iff_eq_zero.1 <| (measure_mono (subset_univ s)).trans_eq <| trim_eq _ .univ

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
⊢ MeasurableSet (F^[n] univ)

Tactic:
induction n with
    | zero => exact MeasurableSet.univ
    | succ n ih =>
      rw [Function.iterate_succ', Function.comp_apply]
      exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ map f (c • μa) ≪ c • μb

Tactic:
by rw [Measure.map_smul]; exact hf.2.smul c

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (s ∪ s')) t ≤ (μ.restrict s + μ.restrict s') t

Tactic:
simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (μ.restrict s) u + (μ.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)

Tactic:
by rw [hs, ht]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
⊢ (Measure.comap f μ) K < ∞

Tactic:
f_me.comap_apply

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
⊢ μ (f '' K) < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case hfin
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ ∃ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j) ≠ ∞

Tactic:
refine hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_
    rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst✝ : Decidable (x ∈ t)
⊢ μ (if x ∈ t then s else ∅) = t.indicator (fun x ↦ μ s) x

Tactic:
by split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := ⋯
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ T

Tactic:
rw [hf]

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ range f
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
⊢ (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s

Tactic:
by rw [coe_finsetSum, Finset.sum_apply]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ (memPartition f n).Finite

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [ofPred_exists, ← exists_prop, ofPred_exists, ofPred_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)

Tactic:
intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
⊢ x ∈ iUnion t'

Tactic:
by_cases hxt : x ∈ t

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ iUnion t'

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'