mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable fun x ↦ a = f x

Tactic:
enter [1, x]; rw [eq_comm]

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| f x = a
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ s a

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ t a

Tactic:
by fun_prop

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

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
inst✝ : MeasurableSpace X
⊢ Measurable uncurry

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a

Tactic:
refine
    ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
      fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ #(univ.sigma fun a ↦ range (f ↑a).natAbs) = ∑ a ∈ s, (f a).natAbs

case refine_2
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ a ∈ s,
    (∑ b ∈ univ.sigma fun a ↦ range (f ↑a).natAbs,
        if (fun a ↦ ↑a.fst) b = a then ↑((fun a ↦ sign (f ↑a.fst)) b) else 0) =
      f a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case ofNat.zero
⊢ (ofNat 0).sign = ↑(SignType.sign (ofNat 0))

Tactic:
simp [sign, negSucc_lt_zero]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case ofNat.succ
n✝ : ℕ
⊢ (ofNat (n✝ + 1)).sign = ↑(SignType.sign (ofNat (n✝ + 1)))

Tactic:
simp [sign, negSucc_lt_zero]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case negSucc
a✝ : ℕ
⊢ -[a✝+1].sign = ↑(SignType.sign -[a✝+1])

Tactic:
simp [sign, negSucc_lt_zero]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun i ↦ (f i).toNNReal

Tactic:
exact hf.toNNReal

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

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

Tactic:
← inv_neg b

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (Ioo ⊥ ⊤).OrdConnected

Tactic:
exact ordConnected_Ioo

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
this : μ (s i) < μ (s i) + ↑(ε' i)
⊢ ∃ f, s i ⊆ ⋃ i, f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + ↑(ε' i)

Tactic:
rcases iInf_lt_iff.mp this with ⟨t, ht⟩

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
this : μ (s i) < μ (s i) + ↑(ε' i)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) < μ (s i) + ↑(ε' i)
⊢ ∃ f, s i ⊆ ⋃ i, f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + ↑(ε' i)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup (u + v) f = ⊥

Tactic:
apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
  · rw [h]; exact .inl bot_ne_top
  · rw [h, bot_add]

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

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
· rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (comap f) (boundedBy m) = boundedBy fun s ↦ m (f '' s)

Tactic:
by
  refine (comap_ofFunction _ ?_).trans ?_
  · refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
    have ht : t.Nonempty := hs.mono hst
    exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)
  · dsimp only [boundedBy]
    congr with s : 1
    rw [image_nonempty]

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

Goal state before:
pp: case pos
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : i ∈ s
⊢ 0 < f ⟨i, h✝⟩

pp: case neg
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : i ∉ s
⊢ 0 < 1

Tactic:
exacts [hf0 _, zero_lt_one]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case zero
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ ∃ m, s m ⊆ dissipate s 0

Tactic:
use 0; simp [dissipate_def]

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

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

Tactic:
add_zero

Goal state after:
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x ↦ ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
rw [le_div_iff₀ (zero_lt_one.trans_le hx)]

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a * x ≤ ↑⌈a * x⌉₊
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s

Tactic:
rw [toMeasurable_def]; split_ifs with hs h's
  exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

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 ≤ᵐ[μ] t
⊢ μ t + 0 = μ t

Tactic:
add_zero

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᵐ[μ] t
⊢ μ t = μ t
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 (ms + 0))
⊢ m (⋂ n, t n) = ms

Tactic:
add_zero

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ m (⋂ n, t n) = ms
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 γ
s : Set α
t : Set β
⊢ Measurable fun x ↦ (↑x.1, ↑x.2)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Nonempty α
hf : MeasurableEmbedding f
⊢ Measurable ⇑hf.equivRange.symm

Tactic:
by fun_prop

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

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

Tactic:
add_zero

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ c • (mapₗ (AEMeasurable.mk f hfc)) μ = c • (mapₗ (AEMeasurable.mk f hf)) μ

Tactic:
congr 1

Goal state after:
case pos.e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ (mapₗ (AEMeasurable.mk f hfc)) μ = (mapₗ (AEMeasurable.mk f hf)) μ
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ((if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s) then
          liftLinear (OuterMeasure.comap f) ⋯
        else 0)
        μ)
      s =
    μ (f '' s)

Tactic:
dif_pos,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ((liftLinear (OuterMeasure.comap f) ⋯) μ) s = μ (f '' s)

case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun i ↦ m i)

Tactic:
simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun p ↦ sfiniteSeq (m p.1) p.2)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
⊢ posmeas.Countable

Tactic:
set fairmeas := fun n : ℕ => { i : ι | as n ≤ μ (As i) }

Goal state after:
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
⊢ posmeas.Countable
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ ⨆ i, μ (s k \ s i) = ⨆ i, μ (s k) - μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ μ (s ∩ (t ∩ u)) = μ (u ∩ s)

Tactic:
congr 1

Goal state after:
case e_6
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ s ∩ (t ∩ u) = u ∩ s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
⊢ ⋃ i, f ⁻¹' Metric.ball x ↑i = univ

Tactic:
rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : ∃ b, a ⋖ b
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
rcases ha with ⟨b, hab⟩

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
b : ι
hab : a ⋖ b
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
by
  rw [sigmaFinite_bot_iff]
  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩ <;> have h_univ := h.measure_univ_lt_top
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

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

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
⊢ (fun n ↦ μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)) = fun n ↦ μ (t ∩ disjointed w n ∩ 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)
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) = ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n)

Tactic:
congr 1

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
⊢ (fun n ↦ μ (t ∩ disjointed w n ∩ u)) = fun n ↦ (μ.restrict (t ∩ u)) (disjointed w n)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f (n + 1) a ∈ memPartition f (n + 1)

Tactic:
classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]

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

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

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

Tactic:
add_zero

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

α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
simp [ht']

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

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

Tactic:
simp [ht']

Goal state after: