mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f Finset.univ) = {f zero, f neg, f pos}

Tactic:
univ_eq

Goal state after:
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ (match a * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match a with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

Tactic:
by
    cases a <;> cases b <;> rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ s.topologicalClosure.carrier

Tactic:
by
    simp only [Subsemiring.coe_carrier_toSubmonoid, Subsemiring.topologicalClosure_coe,
      Subalgebra.coe_toSubsemiring]
    apply subset_closure
    exact algebraMap_mem s r

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

Goal state before:
pp: case pos_bot
x : ℝ
x_pos : 0 < x
⊢ (↑x * ⊥)⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
| pos_bot x x_pos =>

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

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

Tactic:
mul_comm (-b⁻¹) a,

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * -b⁻¹ ≤ -b⁻¹ * a'
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

Tactic:
intro h; unfold LowerSemicontinuousWithinAt at h
    by_contra! hf
    obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi
    exact ltz.not_ge
      (le_liminf_of_le (by isBoundedDefault) ((h y ylt).mono fun _ h₂ =>
        le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : LowerSemicontinuousOn f s
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfs

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (add_lt_add a_x b_x)

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

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

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

Tactic:
· refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
        obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))
        exact ⟨n, le_of_lt hn⟩

Goal state after:
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n ↦ |r| ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r ≠ ∞

Tactic:
refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))
    exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩

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

Goal state before:
pp: a : ℝ
⊢ HasSum (fun n ↦ a / 2 / 2 ^ n) a

Tactic:
convert!
    HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1

Goal state after:
case e'_5
a : ℝ
⊢ (fun n ↦ a / 2 / 2 ^ n) = fun i ↦ a / 2 * (1 / 2) ^ i

case e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ (comap f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯

Tactic:
refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_
  · rw [comap_apply]
    apply ofFunction_le
  · rw [comap_apply, ofFunction_apply, ofFunction_apply]
    refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩
    refine iInf_mono' fun ht => ?_
    rw [Set.image_subset_iff, preimage_iUnion] at ht
    refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
    rcases h with hl | hr
    exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]

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

Goal state before:
pp: case pos
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

pp: case neg
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
· obtain ⟨z₂, z₂lt, h₂⟩ : ∃ z₂ < g x, Ioc z₂ (g x) ⊆ v :=
        exists_Ioc_subset_of_mem_nhds (v_open.mem_nhds xv) hx₂
      filter_upwards [hg z₂ z₂lt] with z h₂z
      have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩
      have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
      calc
        y < f x + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (hx₁ (f z)) (min_le_left _ _)

Goal state after:
case neg
α : 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
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / 2 ^ n

Tactic:
convert! dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
  simp only [add_comm n, pow_add, ← div_div]
  symm
  exact ((hasSum_geometric_two' C).div_const _).tsum_eq

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

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

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact hf.add' hg hcont

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
    by_cases! Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
      rcases le_or_gt (f a) (f x) with h | h
      · exact hl ⟨lfa, h⟩
      · exact hu ⟨le_of_lt h, fau⟩
    · filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case base
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ S

Tactic:
| base h_s =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case base
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ generatePiSystem T

Tactic:
| base h_s =>

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case base
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s✝ : Set α
h_s : s✝ ∈ S
⊢ MeasurableSet s✝

Tactic:
| base h_s =>

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] t ↔ s ∪ t =ᵐ[μ] ∅ ∪ t

Tactic:
rw [empty_union]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ i, ⋂ j, ⋂ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
⊢ i ≠ j →
    ∀ ⦃a : α⦄,
      a ∈ s i → a ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j) → a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)

Tactic:
hne

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
⊢ ∀ ⦃a : α⦄,
    a ∈ s i → a ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j) → a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f μ
hg : f =ᵐ[μ] g
⊢ NullMeasurable g μ

Tactic:
rw [nullMeasurable_iff_eventuallyMeasurable]
  exact EventuallyMeasurable.congr hf hg.symm

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ s ⊆ toMeasurable (map f μ) s

Tactic:
apply subset_toMeasurable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map (g ∘ f) μa ≪ μc

Tactic:
by
    rw [← map_map hg.1 hf.1]
    exact (hf.2.map hg.1).trans hg.2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ μ s + μ (t \ s) = μ (s ∪ t)

Tactic:
by
  rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_sdiff_self]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
⊢ μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞

Tactic:
hμuv

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
hμuv : μ (u ∆ v) ≠ ∞
⊢ μ u = ∞ → μ v = ∞
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Ioi a)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
by
  rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]

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

Goal state before:

Tactic:
μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=
      measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
    _ = μ US + μ ((u ∩ t) \ US) := (measure_add_sdiff hm.nullMeasurableSet _).symm
    _ = restrict μ s u + restrict μ t (u \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_sdiff_assoc]
    _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
    _ = ν US + ν ((u ∩ t) \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_sdiff_assoc]
    _ = ν (US ∪ u ∩ t) := measure_add_sdiff hm.nullMeasurableSet _
    _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ ∅, IsOpen[inst✝¹] U ∧ μ U < ∞

pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞

pp: case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄,
    (∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞) →
      (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s ∪ t, IsOpen[inst✝¹] U ∧ μ U < ∞

pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
· use ∅
    simp

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞

case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄,
    (∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞) →
      (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s ∪ t, IsOpen[inst✝¹] U ∧ μ U < ∞

case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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)
n : ℕ
⊢ μ (t ∩ v n) < ∞

Tactic:
exact (h'v n).lt_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x✝ : MeasurableSpace α
c : R
μ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ (c • μ.toOuterMeasure) (⋃ i, s i) = ∑' (i : ℕ), (c • μ.toOuterMeasure) (s i)

Tactic:
simp only [smul_apply, coe_toOuterMeasure, ENNReal.tsum_const_smul,
          measure_iUnion hd hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x

Tactic:
ae_restrict_uIoc_eq,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᶠ (x : α) in ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)), P x) ↔
    (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = ∅
⊢ False

Tactic:
absurd hx

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = ∅
⊢ f a₁ ∉ s
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : mk f H x ∉ t
⊢ x ∈ s

Tactic:
apply subset_toMeasurable

Goal state after:
case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := ⋯
g : α → β := ⋯
x : α
hx : mk f H x ∉ t
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ

Tactic:
apply subset_toMeasurable

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := ⋯
g : α → β := ⋯
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
h : NullMeasurable f 0
hft : ∀ᵐ (x : α) ∂0, f x ∈ ∅
⊢ AEMeasurable f 0

Tactic:
apply aemeasurable_zero_measure

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ sᶜ ⊆ toMeasurable μ sᶜ

Tactic:
apply subset_toMeasurable

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Tactic:
have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ico a x)) atTop (𝓝 (μ (Ici a)))

Tactic:
← iUnion_Ico_right

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ico a x)) atTop (𝓝 (μ (⋃ b, Ico a b)))
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable fun p ↦ p.2 • p.1

Tactic:
refine measurable_from_prod_countable_left fun n => ?_

Goal state after:
α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
n : ℕ
⊢ Measurable fun x ↦ (x, n).2 • (x, n).1