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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
by
  simp only [← not_eventually, not_imp_not, SemicontinuousWithinAt, SemicontinuousOn]

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

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

Tactic:
left

Goal state after:
case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
⊢ SemicontinuousWithinAt (r ⊔ r') s x

Tactic:
intro b hab
  obtain hb | hb' := hab
  · exact (h b hb).mono fun _ hx ↦ Or.inl hx
  · exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
⊢ SemicontinuousAt (r ⊔ r') x

Tactic:
intro b hab
  obtain hb | hb' := hab
  · exact (h b hb).mono fun _ hx ↦ Or.inl hx
  · exact (h' b hb').mono fun _ hx ↦ Or.inr hx

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

Goal state before:
pp: ⊢ 1⁻¹ = 1

Tactic:
← coe_one,

Goal state after:
⊢ (↑1)⁻¹ = 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

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

Goal state before:
pp: a b c d : EReal
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

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

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

Tactic:
by
  unfold ENNReal.ofReal
  rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]
  exact hf.toNNReal

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

Goal state before:
pp: case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
· obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)
    exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
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
A2 : min (g z) (g x) ∈ v
⊢ f z + g z > y

Tactic:
have : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v := ⟨A1, A2⟩

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
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
A2 : min (g z) (g x) ∈ v
this : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v
⊢ f z + g z > y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
by
  refine le_antisymm ?_ ?_
  · refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_
    apply sInf_le hμ
  · refine le_sInf ?_
    intro μ hμ t
    exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

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

Goal state before:
pp: case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι

Goal state after:
case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ ↑a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuous f⁻¹ ↔ UpperSemicontinuous f

Tactic:
simp [← upperSemicontinuousOn_univ_iff, ← lowerSemicontinuousOn_univ_iff]

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ UpperSemicontinuous f⁻¹ ↔ LowerSemicontinuous f

Tactic:
simp [← upperSemicontinuousOn_univ_iff, ← lowerSemicontinuousOn_univ_iff]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t : Set α
h_in_pi : t ∈ generatePiSystem S
⊢ MeasurableSet t

Tactic:
induction h_in_pi with

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x ↦ s) x ∈ π x

pp: case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x

Tactic:
· rw [Finset.mem_singleton] at hx
        rwa [hx]

Goal state after:
case refine_2.inl.refine_3
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ x ∈ {i}, (fun x ↦ s) x
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : μ s ≠ ∞
ht : μ t ≠ ∞
⊢ μ (s ∪ t) ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs_finite : μ s ≠ ∞
⊢ μ (s ∩ t) < ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht_finite : μ t ≠ ∞
⊢ μ (s ∩ t) < ∞

Tactic:
finiteness

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

Goal state before:
pp: case mp
α : Type u_1
s : Set α
x : Set Prop
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
by_cases hT : True ∈ x

Goal state after:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ s'f ∩ s'g ⊆ sf ∩ sg

Tactic:
exact inter_subset_inter hs'sf hs'sg

Goal state after:
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 α := ⋯
⊢ iInter X ⊆ F (iInter X)

Tactic:
rintro x hx ⟨y, hy, rfl⟩

Goal state after:
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 α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : g y ∈ iInter X
⊢ False
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

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

Tactic:
union_sdiff_right,

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
⊢ μ (t ∪ s) = μ s + μ t

Tactic:
measure_union₀ hs (AEDisjoint.symm hd),

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
⊢ μ t + μ s = μ s + μ t
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
⊢ map f μ = map g μ

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : ¬AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
· have hg : AEMeasurable g μ := hf.congr h
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
    exact
      mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : ¬AEMeasurable f μ
⊢ map f μ = map g μ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ (map f μ) s ≤ μ (f ⁻¹' s)

Tactic:
have hst : s ⊆ t := by
    rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
    exact image_mono (subset_toMeasurable _ _)

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ (map f μ) s ≤ μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
union_sdiff_right,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ t + μ (s \ t) + μ (s ∩ t) = μ s + μ t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : μ s ≠ ∞
⊢ μ sᶜ = μ univ - μ s

Tactic:
by
  rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ t ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ s ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ μ univ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
s : Set α
h_univ : μ s + μ sᶜ = ν s + ν sᶜ
hs : MeasurableSet s
x✝ : s.Nonempty
h_lt : μ s < ν s
h_disj : Disjoint s sᶜ
⊢ μ sᶜ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
h : μ s = μ univ
⊢ μ univ ≠ ∞

Tactic:
finiteness

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

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

Tactic:
rw [← restrict_congr_set hs.toMeasurable_ae_eq,
    restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]

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 t + μ.restrict ((s ∪ t) \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
union_sdiff_right,

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ μ (s ∪ t) ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ μ (t ∪ s) ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ s ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ t ≠ ∞

Tactic:
finiteness

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
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
⊢ IsLocallyFiniteMeasure (c • μ)

Tactic:
refine ⟨fun x => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
⊢ (c • μ).FiniteAtFilter (𝓝 x)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ TopologicalSpace.IsTopologicalBasis {s | IsOpen[inst✝¹] s ∧ μ s < ∞}

Tactic:
by
  refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_
  intro x s xs hs
  rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩
  refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩
  exact measure_mono inter_subset_left

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
r : ℝ
⊢ μ (Metric.ball x r) < ∞

Tactic:
finiteness

Goal state after:
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_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, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)

Tactic:
rw [← Antitone.measure_iInter]
  · rw [iInter_comm]
    exact congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm
  · exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl
  · exact fun i ↦ .biInter (to_countable _) fun _ _ ↦ h _
  · 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.Typeclasses.Finite

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ μ t ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ ν t ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = 0

Tactic:
eq_empty_of_isEmpty s,

Goal state after:
α : Type u_1
inst✝ : IsEmpty α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ ∅ = 0
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm₂).trim hm₁₂) t = (μ.trim ⋯) t

Tactic:
rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]

Goal state after:
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)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∑' (n : ℕ), μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) = ∑' (n : ℕ), μ (t ∩ disjointed w n ∩ u)

Tactic:
congr 1
        ext1 n
        apply measure_toMeasurable_inter hu
        apply ne_of_lt
        calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)

Tactic:
refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm
  · refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm
    rwa [measure_toMeasurable t]
  · simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht
    exact ht.1

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)

Tactic:
rw [add_comm] at ht ⊢

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (ν + μ) t ≠ ∞
⊢ ν (toMeasurable (ν + μ) t ∩ s) = ν (t ∩ s)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
⊢ memPartitionSet f n a = s ↔ a ∈ s

Tactic:
refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
⊢ memPartitionSet f n a = s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ s ⊆ ⋃ y ∈ s, measurableAtom y

pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s

Tactic:
· intro x hx
        simpa using ⟨x, hx, by simp⟩

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (⋃ i, Subtype.val '' f i) μ

Tactic:
exact .iUnion hf

Goal state after: