awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
insert :
  μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ x ∈ s, t x) = ν.restrict (⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)
insert₁ insert₂ :
  μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ x ∈ s, t x) = ν.restrict (⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i)
⊢ μ.restrict (t i ∪ ⋃ x ∈ s, t x) = ν.restrict (t i ∪ ⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)

Tactic:
rw [restrict_union_congr, ← hs]

Premises used: MeasureTheory.Measure.restrict_union_congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
empty :
  μ.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) =
      ν.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) ↔
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → μ.restrict (t i) = ν.restrict (t i)
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)),
        μ.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) ↔
          ∀ i_1 ∈ Insert.insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]

Premises used: Insert.insert, Finset.mem_insert, forall_eq_or_imp, Set.iUnion_iUnion_eq_or_left, MeasureTheory.Measure.restrict_union_congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
empty :
  μ.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) =
      ν.restrict (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) ↔
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → μ.restrict (t i) = ν.restrict (t i)
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)),
        μ.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) = ν.restrict (⋃ i_1 ∈ Insert.insert i s, t i_1) ↔
          ∀ i_1 ∈ Insert.insert i s, μ.restrict (t i_1) = ν.restrict (t i_1)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]

Premises used: Insert.insert, Finset.mem_insert, forall_eq_or_imp, Set.iUnion_iUnion_eq_or_left, MeasureTheory.Measure.restrict_union_congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
⊢ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩

Premises used: MeasureTheory.Measure.restrict_congr_mono, Set.subset_iUnion, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
refine :
  ∀ (h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)), μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
⊢ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
h₁ :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((ν.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (t : Finset ι) ↦ ⋃ i ∈ t, s i

Tactic:
have D : Directed (· ⊆ ·) fun t : Finset ι => ⋃ i ∈ t, s i :=
    Monotone.directed_le fun t₁ t₂ ht => biUnion_subset_biUnion_left ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (t : Finset ι) ↦ ⋃ i ∈ t, s i
h₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [iUnion_eq_iUnion_finset]

Premises used: Set.iUnion_eq_iUnion_finset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (t : Finset ι) ↦ ⋃ i ∈ t, s i
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((ν.restrict (⋃ (t : Finset ι), ⋃ i ∈ t, s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_biUnion_finset_congr.2 fun i _ => h i]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, MeasureTheory.Measure.restrict_biUnion_finset_congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
haveI :
  ∀ (this : Encodable (↑s : Type u_6)),
    μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
haveI := hc.toEncodable
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Set ι
t : ι → Set α
hc : s.Countable
this : Encodable (↑s : Type u_6)
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
simp only [biUnion_eq_iUnion, SetCoe.forall', restrict_iUnion_congr]

Premises used: Set.biUnion_eq_iUnion, MeasureTheory.Measure.restrict_iUnion_congr, SetCoe.forall'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
rw : μ.restrict (⋃ i ∈ S, i) = ν.restrict (⋃ i ∈ S, i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
rw₁ rw₂ : (∀ i ∈ S, μ.restrict i = ν.restrict i) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
⊢ μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

Tactic:
rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]

Premises used: Set.sUnion_eq_biUnion, MeasureTheory.Measure.restrict_biUnion_congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (sInf m).restrict t = sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((fun (x : Measure α) ↦ (x.restrict t).toOuterMeasure) '' m) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
h₄ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf
              ((fun (a : Measure α) ↦
                  (OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) a.toOuterMeasure) ''
                m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₅ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((⇑(OuterMeasure.restrict t) : (a : OuterMeasure α) → OuterMeasure α) '' toOuterMeasure '' m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₆ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    ((((OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) (sInf (toOuterMeasure '' m)) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]

Premises used: Set.image_image, MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict, MeasureTheory.Measure.sInf_apply, MeasureTheory.Measure.toOuterMeasure, Set.Nonempty.image, MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict, MeasureTheory.OuterMeasure.restrict_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
rw : ∀ (hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s) {p : α → Prop} (hp : ∀ᵐ (x : α) ∂μ.restrict s, p x), ∃ x ∈ s, p x
⊢ ∃ x ∈ s, p x

Tactic:
rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs

Premises used: MeasureTheory.Measure.restrict_apply_self, MeasureTheory.frequently_ae_mem_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
(hs.and_eventually hp).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
exact (hs.and_eventually hp).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
⊢ map f (μ.restrict s) ≪ ν.restrict t

Tactic:
AbsolutelyContinuous.mk fun u hum ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
refine :
  ∀ (u : Set β) (hum : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((ν.restrict t : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) (((map f (μ.restrict s) : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ map f (μ.restrict s) ≪ ν.restrict t

Tactic:
refine AbsolutelyContinuous.mk fun u hum ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
this :
  Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.restrict t : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map f (μ.restrict s) : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [hum, hf.measurable, hf.measurable hum]

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
suffices :
  Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.restrict t : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map f (μ.restrict s) : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
refine : ∀ (hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)), f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)

Tactic:
rw [preimage_inter]

Premises used: Set.preimage_inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ : s ⊆ f ⁻¹' t
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ⊆ f ⁻¹' t

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
hs : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
rw : μ = ν ↔ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
rw₂ : μ = ν ↔ μ = ν.restrict univ
rw₃ rw₄ : μ = ν ↔ μ = ν
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]

Premises used: MeasureTheory.Measure.restrict_iUnion_congr, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, s i) univ
rw : μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
rw₂ : μ = ν ↔ μ = ν.restrict univ
rw₃ rw₄ : μ = ν ↔ μ = ν
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)

Tactic:
rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]

Premises used: MeasureTheory.Measure.restrict_biUnion_congr, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
hs rwa rwa₁ rwa₂ rwa₃ : ⋃₀ S = univ
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, i) univ

Tactic:
rwa [← sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext_of_sUnion_eq_univ hc hU fun t ht => ?_

Premises used: MeasureTheory.Measure.ext_of_sUnion_eq_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine : ∀ (t : Set α) (ht : t ∈ T), μ.restrict t = ν.restrict t
⊢ μ = ν

Tactic:
refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_

Premises used: MeasureTheory.Measure.ext_of_sUnion_eq_univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
h :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
⊢ μ.restrict t = ν.restrict t

Tactic:
ext1 u hu
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [restrict_apply hu]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞)

Tactic:
simp only [Set.empty_inter, measure_empty]

Premises used: Set.empty_inter, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u_1 u : Set α
hu : u ∈ S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)

Tactic:
ST_eq _ ht _ hu
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u_1 u : Set α
hu : u ∈ S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)

Tactic:
exact ST_eq _ ht _ hu