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

Goal state before:
pp: a : SignType
⊢ -a = a ↔ a = 0

Tactic:
by decide +revert

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

Goal state before:
pp: a : SignType
⊢ -a = 0 ↔ a = 0

Tactic:
by decide +revert

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

Goal state before:
pp: a b : SignType
⊢ -a ≤ -b ↔ b ≤ a

Tactic:
by decide +revert

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

Goal state before:
pp: a b : SignType
⊢ -a < -b ↔ b < a

Tactic:
by decide +revert

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

Goal state before:
pp: f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
by
  rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]
  norm_cast

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

Goal state before:
pp: β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g

Tactic:
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)
  lift g to β → ℝ≥0 using hg
  rw [NNReal.summable_coe] at hf ⊢
  exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

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

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)

Tactic:
simp only [lt_top_iff_ne_top]

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

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

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
  rw [← ENNReal.coe_zero]
  norm_cast at *
  apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
⊢ f ⁻¹' s ⊆ iUnion t → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
ht

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
⊢ m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) = m (t n)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

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

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
⊢ t ∈ insert ∅ S → (s ∩ t).Nonempty → s ∩ t ∈ insert ∅ S

Tactic:
ht

Goal state after:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
⊢ (s ∩ t).Nonempty → s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
⊢ t ∈ insert univ S → (s ∩ t).Nonempty → s ∩ t ∈ insert univ S

Tactic:
ht

Goal state after:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ (s ∩ t).Nonempty → s ∩ t ∈ insert univ S
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
⊢ ∀ (i : P t), s ⊆ t → (inducedOuterMeasure m P0 m0) s ≤ m t i

Tactic:
ht

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
⊢ s ⊆ t → (inducedOuterMeasure m P0 m0) s ≤ m t ht
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ μ (⋃ i ∈ s, f i) < ∞

Tactic:
by
  convert! (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3
  · ext
    rw [Finite.mem_toFinset]
  · simpa only [ENNReal.sum_lt_top, Finite.mem_toFinset]

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
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0

Tactic:
by
  simp [EventuallyEq, eventually_iff, ae, compl_ofPred]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
⊢ ∀ (ht : DynkinSystem.GenerateHas s t), C t ⋯

Tactic:
ht

Goal state after:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ C t ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ x ⊆ ∅

Tactic:
intro p hp

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ p ∈ ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e '' ⇑e ⁻¹' s = s

Tactic:
rw [← coe_toEquiv, Equiv.image_preimage]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s

Tactic:
refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.Map

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

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]
  exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
⊢ (map f ν) t = 0 → (map f μ) t = 0

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : (map f ν) t = 0
⊢ (map f μ) t = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
h' : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ))
⊢ comap f (c • μ) = c • comap f μ

Tactic:
simp [comap_undef, h, h']

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ (sum fun n ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ

Tactic:
rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (ν.restrict s) u + (μ.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)

Tactic:
ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (ν.restrict s) u + (ν.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
⊢ t ∈ measurableAtom '' s → ∀ ⦃y : Set α⦄, y ∈ measurableAtom '' s → t ≠ y → Disjoint t y

Tactic:
ht

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
ht : t ∈ measurableAtom '' s
⊢ ∀ ⦃y : Set α⦄, y ∈ measurableAtom '' s → t ≠ y → Disjoint t y
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
⊢ t ∈ T → ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)

Tactic:
ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
⊢ ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ 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)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ ⋃ i, t ∩ w i

Tactic:
refine mem_iUnion.2 ⟨n, ?_⟩

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)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ t ∩ w n
Module: Mathlib.MeasureTheory.Measure.Trim

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

Tactic:
refine @Measure.ext _ m _ _ (fun t ht => ?_)
  rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]

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

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x

Tactic:
· rwa [Pi.div_apply, Pi.one_apply, div_eq_one]

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

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
A : t' ∩ s =ᵐ[μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᵐ[μ] s
B : t' ∩ s' =ᵐ[μ] t' ∩ s
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
exact (ht'.inter hs').nullMeasurableSet.congr (B.trans A)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet t μ

Tactic:
obtain ⟨t', t'_subs, ht', t't⟩ : ∃ t' ⊆ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
    h.exists_measurable_subset_ae_eq

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
⊢ NullMeasurableSet t μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ : ∀ s ∈ S, μ s < ∞
hU : ⋃₀ S = univ
⊢ SigmaFinite μ

Tactic:
obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ ⋃ n, s n = univ :=
    (@exists_seq_cover_iff_countable _ (fun x => μ x < ∞) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ✝ : ∀ s ∈ S, μ s < ∞
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), μ (s n) < ∞
hs : ⋃ n, s n = univ
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
⊢ μ univ < ∞

Tactic:
have hs_univ : ⋃ i, s i = Set.univ := iUnion_spanningSets μ

Goal state after:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet t →
    ∀ (x : (ℕ → Prop) → Prop),
      (t = ⋃ p, if x p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
ht

Goal state after:
case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∀ (x : (ℕ → Prop) → Prop),
    (t = ⋃ p, if x p then countablyGeneratedAtom α p else ∅) →
      ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
⊢ (∀ (n : ℕ), MeasurableSet (t n)) →
    (∀ (n : ℕ), ∃ q, t n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
      ∃ q, ⋃ i, t i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
ht

Goal state after:
case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ (∀ (n : ℕ), ∃ q, t n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
    ∃ q, ⋃ i, t i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
⊢ CountablySeparated α

Tactic:
simp_rw [countablySeparated_def] at *

Goal state after:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ SeparatesPoints α

Tactic:
refine ⟨fun x y h ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
⊢ ∑ i ∈ F, (μ.restrict (s i)) t ≤ (M • μ.restrict (⋃ i, s i)) t

Tactic:
have iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i := by
    intro x hx
    simp_rw [Cs, Finset.mem_sdiff, mem_iUnion] at hx
    have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx
    have ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.mpr <| Finset.notMem_singleton.mp C_nonempty
    exact ⟨s i, ⟨i, rfl⟩, hxC.1 (s i) ⟨i, by simp [hi]⟩⟩

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
⊢ ∑ i ∈ F, (μ.restrict (s i)) t ≤ (M • μ.restrict (⋃ i, s i)) t
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u

Tactic:
simp only [mem_range] at hu
    obtain ⟨n, rfl⟩ := hu
    exact generateFrom_mono (subset_iUnion _ _) _ (measurableSet_generateFrom_memPartition t n)

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
⊢ MeasurableSet t → MeasurableSet ((⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t)

Tactic:
ht

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet ((⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑b) = min (μ (t' ↑b)) (ν (t' ↑b))

pp: case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑b) = min (μ (t' ↑b)) (ν (t' ↑b))

Tactic:
· rw [Subtype.forall]
        intro n hn; simpa

Goal state after:
case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑b) = min (μ (t' ↑b)) (ν (t' ↑b))