mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H] using h₂ ⟨h₂z, H⟩

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
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H] using h₂ ⟨h₂z, H⟩

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

Goal state before:
pp: α : Type u_1
⊢ boundedBy 0 ≤ ⊥

Tactic:
apply boundedBy_le

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 *

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt (fun z ↦ f z + g z) univ x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun z ↦ ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z ↦ ∑ i ∈ a, f i z) univ x
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
by
  simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]

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
    rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
    filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)

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 : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' ↦ ⨆ i, f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Goal state after:
α : 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
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:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ∑' (i : ι), f i x') univ x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
    exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s✝ : Set α
h_gen_s : generatePiSystem (⋃ b, g b) s✝
h_s : ∃ T f, s✝ = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
h_nonempty : (s✝ ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ ∃ T f, s✝ ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩

Goal state after:
case inter
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ ∃ T f, (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k ↦ {s k}) S

Tactic:
rintro _ ⟨k, hk, rfl⟩
    refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
    · rw [Finset.mem_coe, Finset.mem_singleton] at hm
      rwa [hm]
    · exact Set.mem_singleton _
    · simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]

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

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ

Tactic:
· exact AEMeasurable.eval

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap

Goal state after:
α : Type u_1
s t : Set α
⊢ { MeasurableSet' := fun s_1 ↦ ∃ s', MeasurableSet s' ∧ (fun x ↦ x ∈ s) ⁻¹' s' = s_1, measurableSet_empty := ⋯,
          measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }.1
      t ↔
    t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : 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 : β → α
hf : MeasurableEmbedding f
⊢ ↑(f '' univ) = ↑(range f)

Tactic:
by rw [image_univ]

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

Goal state before:
pp: α : 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 : β → α
hf : MeasurableEmbedding f
⊢ Subtype.instMeasurableSpace ≍ Subtype.instMeasurableSpace

Tactic:
by rw [image_univ]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
⊢ μ (limsup s cofinite) = 0

Tactic:
by
  refine bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_
  calc
    μ (limsup s cofinite) ≤ μ (⋃ i : {i // i ∉ t}, s i) := by
      gcongr
      rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
      exact iInter₂_subset _ t.finite_toSet
    _ ≤ ∑' i : {i // i ∉ t}, μ (s i) := measure_iUnion_le _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0

Tactic:
h_eq_α

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) (s \ t ∪ t \ s) = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
s : Set α
hs : MeasurableSet s
⊢ (comap f (comap g μ)) s = (comap (g ∘ f) μ) s

Tactic:
comap_apply _ hf hf' _ hs,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
s : Set α
hs : MeasurableSet s
⊢ (comap g μ) (f '' s) = (comap (g ∘ f) μ) s
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
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ a ≤ c

Tactic:
simpa using hac

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i : ι
hi : μ (t i) = ∞
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
calc
      μ (⋃ i, t i) ≤ ∞ := le_top
      _ ≤ μ (s i) := hi ▸ h_le i
      _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t

Tactic:
by
  rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ {i | 0 < μ (As i)}.Countable

Tactic:
rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢
  have obs : { i : ι | 0 < sum (sfiniteSeq μ) (As i) }
      ⊆ ⋃ n, { i : ι | 0 < sfiniteSeq μ n (As i) } := by
    intro i hi
    by_contra con
    simp only [mem_iUnion, mem_ofPred_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
    rw [sum_apply₀] at hi
    · simp_rw [con] at hi
      simp at hi
    · exact As_mble i
  apply Countable.mono obs
  refine countable_iUnion fun n ↦ ?_
  apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
  · exact fun i ↦ (As_mble i).mono (le_sum _ _)
  · exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)
  · exact measure_ne_top _ (⋃ i, As i)

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
⊢ ∀ {u v : Set α}, u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
intro u v hu hv huv

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
⊢ Disjoint u v
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
⊢ ∀ {u v : Set α}, u ∈ memPartition f (n + 1) → v ∈ memPartition f (n + 1) → u ≠ v → Disjoint u v

Tactic:
intro u v hu hv huv

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Disjoint u v
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : 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 α := ⋯
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋯
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n) ≠ ∞

Tactic:
apply ne_of_lt

Goal state after:
case e_f
α : 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 α := ⋯
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋯
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n) < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : 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
n : ℕ
⊢ μ (t ∩ disjointed w n ∩ u) = μ (disjointed w n ∩ (t ∩ u))

pp: case e_f
α : 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
n : ℕ
⊢ MeasurableSet (disjointed w n)

Tactic:
inter_comm t _,

Goal state after:
case e_f
α : 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
n : ℕ
⊢ μ (disjointed w n ∩ t ∩ u) = μ (disjointed w n ∩ (t ∩ u))

case e_f
α : 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
n : ℕ
⊢ MeasurableSet (disjointed w n)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
⊢ HasCountableSeparatingOn α p t

Tactic:
rcases h.1 with ⟨S, hSc, hSq, hS⟩
  choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
  refine ⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
  refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)
  rw [← hV U hU]
  exact h _ (mem_image_of_mem _ hU)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff, ← compl_ofPred, restrict_apply₀' hs]
  rw [iff_iff_eq]; congr with x; simp [and_comm]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
rw [← generateFrom_natGeneratingSequence α] at hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
⊢ μ (f '' t ∩ s) = μ (f '' (t ∩ f ⁻¹' s))

Tactic:
image_inter_preimage

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
⊢ μ (f '' t ∩ s) = μ (f '' t ∩ s)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_1
α : 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)
⊢ Measurable g

pp: case refine_2
α : 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)
⊢ range g ⊆ t

pp: case refine_3
α : 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)
⊢ f =ᵐ[μ] g

Tactic:
· exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk

Goal state after:
case refine_2
α : 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)
⊢ range g ⊆ t

case refine_3
α : 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)
⊢ f =ᵐ[μ] g
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
    h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᵐ[μ] g
⊢ AEMeasurable (codRestrict f s hfs) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Iio a)

Tactic:
· apply H

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

Goal state before:
pp: case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)

Tactic:
have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)

Goal state after:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)