mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

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

Tactic:
zero_mul

Goal state after:
case top_pos
x : ℝ
x_pos : 0 < x
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = 0 * (↑x)⁻¹

Tactic:
zero_mul

Goal state after:
case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-|a|⁻¹) = (↑a)⁻¹

Tactic:
← coe_inv a,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-|a|⁻¹) = ↑a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ (↑a)⁻¹

Tactic:
← coe_inv a,

Goal state after:
case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ ↑a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : ↑a ≤ 0
⊢ (↑a)⁻¹ ≤ 0

Tactic:
← coe_inv a,

Goal state after:
case coe
a : ℝ
h : ↑a ≤ 0
⊢ ↑a⁻¹ ≤ 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ (↑b)⁻¹ < (↑a)⁻¹

Tactic:
← coe_inv a,

Goal state after:
b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ (↑b)⁻¹ < ↑a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0 * ⊤
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤

Tactic:
zero_mul

Goal state after:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal
hx : x < ⊤
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x

Tactic:
rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩

Goal state after:
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

Tactic:
suffices ∀ i ∈ I, IsClosed (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i) by
      simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i)
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
· simpa only [← abs_pow] using! (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h

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

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i ↦ ε' ↑i) c ∧ c ≤ ε

Tactic:
classical
  have := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]

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:
rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact hf.inf hg

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

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

Tactic:
rw [← nhdsWithin_univ] at bdd

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ UpperSemicontinuousWithinAt f s a

Tactic:
upperSemicontinuousWithinAt_iff

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ S ∩ S ∈ {S}

Tactic:
Set.inter_self,

Goal state after:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ S ∈ {S}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ S ∈ {S}

Tactic:
Set.mem_singleton_iff

Goal state after:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ S = S
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ m (⋃ i, s i) = ∑' (i : ℕ), m (s i)

Tactic:
by
  refine le_antisymm (measure_iUnion_le s) ?_
  rw [ENNReal.tsum_eq_iSup_nat]
  refine iSup_le fun n => ?_
  have := @isCaratheodory_sum _ m _ h hd univ n
  simp only [inter_comm, inter_univ, univ_inter] at this; simp only [this]
  exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k ↦ {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k ∈ S, s k = t}

Tactic:
exact ⟨m, hI hm, (hf m hm).symm⟩

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 =ᵐ[μ] ∅ ↔ s ∩ t =ᵐ[μ] ∅ ∩ t

Tactic:
empty_inter

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅ ↔ s ∩ t =ᵐ[μ] ∅
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0

Tactic:
exact Filter.Eventually.and hf_eq hp

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
by
  rw [← compl_iff, compl_iInter]
  exact .iUnion_of_monotone (compl_anti.comp hsm) fun i ↦ (hs i).compl

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ (sum fun i ↦ (m i).trim) s ≤ (sum m).trim s

Tactic:
by
  simp only [sum_apply, trim_eq_iInf, le_iInf_iff]
  exact fun t st ht =>
    ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

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:
intro i j hne x hi hU hj

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
x : α
hi : x ∈ s i
hU : x ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)
hj : x ∈ s j
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : 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 α := ⋯
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := ⋯
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
h : y ∉ f '' F^[n] univ
⊢ g y ∈ g '' (f '' F^[n] univ)ᶜ

Tactic:
exact ⟨y, h, rfl⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ t + μ (s \ t) = μ (s ∩ t) + μ (s \ t) + μ t

Tactic:
add_right_comm

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ (s \ t) + μ t = μ (s ∩ t) + μ (s \ t) + μ t
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ (mapₗ f) μ = 0 ↔ μ = 0

Tactic:
by
  rw [mapₗ_apply_of_measurable hf, map_eq_zero_iff hf.aemeasurable]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (preimage f)^[n] s =ᵐ[μ] s

Tactic:
simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
⊢ comap Subtype.val (𝓝[<] b) = atTop

Tactic:
rw [comap_coe_nhdsLT_eq_atTop_iff]
  refine ⟨hsb, fun hsne a ha ↦ ?_⟩
  rcases hs hsne with ⟨c, hcb, hcs⟩
  rcases hb.lt_iff_exists_lt.mp (max_lt ha hcb) with ⟨x, hxb, hacx⟩
  rw [max_lt_iff] at hacx
  exact ⟨x, hcs ⟨hacx.2, hxb⟩, hacx.1, hxb⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict t + μ.restrict (s \ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t

Tactic:
add_right_comm

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
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)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ n, t ∩ disjointed w n

Tactic:
rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]

Goal state after:
α : 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)
⊢ t ⊆ ⋃ i, t ∩ w i
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ (μ.trim hm) (t ∩ s) = (μ.restrict s) t

Tactic:
Measure.restrict_apply (hm t ht),

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ (μ.trim hm) (t ∩ s) = μ (t ∩ s)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton

Tactic:
intro x hx y hy

Goal state after:
case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ (⋃ i, f '' spanningSets μ i) ∪ (range f)ᶜ = univ

Tactic:
← Set.image_iUnion,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ (f '' ⋃ i, spanningSets μ i) ∪ (range f)ᶜ = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ MeasurableSet s ↔ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨S, hS_subset, hS_eq⟩ ↦ ?_⟩
  · induction s, h using generateFrom_induction with
    | hC u hu _ => exact ⟨{u}, by simp [hu], by simp⟩
    | empty => exact ⟨∅, by simp, by simp⟩
    | compl u _ hu =>
      obtain ⟨S, hS_subset, rfl⟩ := hu
      refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
      · simp only [Finset.coe_sdiff, coe_toFinset]
        exact sdiff_subset
      · simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_sdiff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_sdiff huV) |>.symm
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]
    | iUnion f _ h =>
      choose S hS_subset hS_eq using h
      have : Fintype (⋃ n, (S n : Set (Set α))) := by
        refine (Finite.subset (finite_memPartition t n) ?_).fintype
        simp only [iUnion_subset_iff]
        exact hS_subset
      refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
      · simp only [coe_toFinset, iUnion_subset_iff]
        exact hS_subset
      · simp only [coe_toFinset, sUnion_iUnion, hS_eq]
  · rw [hS_eq, sUnion_eq_biUnion]
    refine MeasurableSet.biUnion ?_ (fun t ht ↦ ?_)
    · exact S.countable_toSet
    · exact measurableSet_generateFrom (hS_subset ht)

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

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ map f (μ.restrict (AEMeasurable.mk f hf ⁻¹' s)) = map f (μ.restrict (f ⁻¹' s))

Tactic:
apply congr_arg

Goal state after:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal (ε + δ)

Tactic:
ENNReal.ofReal_add hε hδ

Goal state after:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) → infEDist x s < ENNReal.ofReal (ε + δ)

Tactic:
ENNReal.ofReal_add hε hδ

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal (ε + δ)

Tactic:
ENNReal.ofReal_add hε hδ

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal (ε + δ)

Tactic:
ENNReal.ofReal_add hε hδ

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
rw [restrict_of_not_measurable hs] at hr
    exact (h0 <| eq_zero_of_mem_range_zero hr).elim

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ∞

Tactic:
exact WithTop.top_pos

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)

Tactic:
rw [ennrealRatEmbed_encode q]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ↑(↑q).toNNReal ≤ f a), ↑(↑q).toNNReal
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
H : (s \ interior s).Countable
⊢ MeasurableSet s

Tactic:
by
    have : s = interior s ∪ s \ interior s := by rw [union_sdiff_cancel interior_subset]
    rw [this]
    exact isOpen_interior.measurableSet.union H.measurableSet

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (nearestPtInd e (N + 1)) x ≤ N + 1

Tactic:
simp only [nearestPtInd_succ]

Goal state after:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x) ≤ N + 1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

Tactic:
by
  rw [lintegral, lintegral]
  exact iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this✝⁴ : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x ↦ g (f x)) μ
G : β → ↑(range g) := rangeFactorization g
hG : IsClosedEmbedding G
this : AEMeasurable (G ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
s t : Set α
⊢ AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aestronglyMeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

Goal state after: