[Merged by Bors] - chore: make some induction_on* compatible with induction

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -210,16 +210,6 @@ instance (priority := 100) BorelSpace.countablyGenerated {α : Type*} [Topologic
   borelize α
   exact hb.borel_eq_generateFrom
 
-theorem MeasurableSet.induction_on_open [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
-    {C : Set α → Prop} (h_open : ∀ U, IsOpen U → C U)
-    (h_compl : ∀ t, MeasurableSet t → C t → C tᶜ)
-    (h_union :
-      ∀ f : ℕ → Set α,
-        Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C (f i)) → C (⋃ i, f i)) :
-    ∀ ⦃t⦄, MeasurableSet t → C t :=
-  MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen
-    (h_open _ isOpen_empty) h_open h_compl h_union
-
 section
 
 variable [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β]
@@ -232,6 +222,16 @@ theorem IsOpen.measurableSet (h : IsOpen s) : MeasurableSet s :=
 theorem IsOpen.nullMeasurableSet {μ} (h : IsOpen s) : NullMeasurableSet s μ :=
   h.measurableSet.nullMeasurableSet
 
+@[elab_as_elim]
+theorem MeasurableSet.induction_on_open {C : ∀ s : Set γ, MeasurableSet s → Prop}
+    (isOpen : ∀ U (hU : IsOpen U), C U hU.measurableSet)
+    (compl : ∀ t (ht : MeasurableSet t), C t ht → C tᶜ ht.compl)
+    (iUnion : ∀ f : ℕ → Set γ, Pairwise (Disjoint on f) → ∀ (hf : ∀ i, MeasurableSet (f i)),
+      (∀ i, C (f i) (hf i)) → C (⋃ i, f i) (.iUnion hf)) :
+    ∀ t (ht : MeasurableSet t), C t ht := fun t ht ↦
+  MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen
+    (isOpen _ isOpen_empty) isOpen compl iUnion t ht
+
 instance (priority := 1000) {s : Set α} [h : HasCountableSeparatingOn α IsOpen s] :
     CountablySeparated s := by
   rw [CountablySeparated.subtype_iff]
@@ -265,8 +265,8 @@ theorem IsCompact.nullMeasurableSet [T2Space α] {μ} (h : IsCompact s) : NullMe
 then they can't be separated by a Borel measurable set. -/
 theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ}
     (hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
-  hs.induction_on_open (C := fun s ↦ (x ∈ s ↔ y ∈ s)) (fun _ ↦ h.mem_open_iff) (fun _ _ ↦ Iff.not)
-    fun _ _ _ h ↦ by simp [h]
+  MeasurableSet.induction_on_open (fun _ ↦ h.mem_open_iff) (fun _ _ ↦ Iff.not)
+    (fun _ _ _ h ↦ by simp [h]) s hs
 
 /-- If `K` is a compact set in an R₁ space and `s ⊇ K` is a Borel measurable superset,
 then `s` includes the closure of `K` as well. -/

Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

@@ -593,11 +593,10 @@ lemma ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero {μ : Measure β} {f : 
     have I : ∫ x, f x ∂μ = 0 := by rw [← setIntegral_univ]; exact h'f _ isClosed_univ
     simpa [ht, I] using integral_add_compl t_meas hf
   intro s hs
-  refine MeasurableSet.induction_on_open (fun U hU ↦ ?_) A (fun g g_disj g_meas hg ↦ ?_) hs
-  · rw [← compl_compl U]
-    exact A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
-  · rw [integral_iUnion g_meas g_disj hf.integrableOn]
-    simp [hg]
+  induction s, hs using MeasurableSet.induction_on_open with
+  | isOpen U hU => exact compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
+  | compl s hs ihs => exact A s hs ihs
+  | iUnion g g_disj g_meas hg => simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]
 
 @[deprecated (since := "2024-04-17")]
 alias ae_eq_zero_of_forall_set_integral_isClosed_eq_zero :=

Mathlib/MeasureTheory/Group/Measure.lean

@@ -603,13 +603,10 @@ theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [Noncom
 @[to_additive]
 lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s) :
     s * (closure {1} : Set G) = s := by
-  apply MeasurableSet.induction_on_open (C := fun t ↦ t • (closure {1} : Set G) = t) ?_ ?_ ?_ hs
-  · intro U hU
-    exact hU.mul_closure_one_eq
-  · rintro t - ht
-    exact compl_mul_closure_one_eq_iff.2 ht
-  · rintro f - - h''f
-    simp only [iUnion_smul, h''f]
+  induction s, hs using MeasurableSet.induction_on_open with
+  | isOpen U hU => exact hU.mul_closure_one_eq
+  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
+  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]
 
 @[to_additive (attr := simp)]
 lemma measure_mul_closure_one (s : Set G) (μ : Measure G) :

Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

@@ -73,29 +73,22 @@ lemma MeasurableEmbedding.prodMap {α β γ δ : Type*} {mα : MeasurableSpace 
     {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β}
     {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
     MeasurableEmbedding (Prod.map g f) := by
-  have h_inj : Function.Injective fun x : γ × α => (g x.fst, f x.snd) := by
-    intro x y hxy
-    rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
-    simp only [Prod.mk.inj_iff] at hxy ⊢
-    exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
-  refine ⟨h_inj, ?_, ?_⟩
+  refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
   · exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)
-  · -- Induction using the π-system of rectangles
-    refine fun s hs =>
-      @MeasurableSpace.induction_on_inter _
-        (fun s => MeasurableSet ((fun x : γ × α => (g x.fst, f x.snd)) '' s)) _ _
-        generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ _ hs
-    · simp only [Set.image_empty, MeasurableSet.empty]
-    · rintro t ⟨t₁, ht₁, t₂, ht₂, rfl⟩
-      rw [← Set.prod_image_image_eq]
+  · intro s hs
+    -- Induction using the π-system of rectangles
+    induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
+    | empty =>
+      simp only [Set.image_empty, MeasurableSet.empty]
+    | basic s hs =>
+      obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := hs
+      simp_rw [Prod.map, ← prod_image_image_eq]
       exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
-    · intro t _ ht_m
-      rw [← Set.range_diff_image h_inj, ← Set.prod_range_range_eq]
-      exact
-        MeasurableSet.diff (MeasurableSet.prod hg.measurableSet_range hf.measurableSet_range) ht_m
-    · intro g _ _ hg
-      simp_rw [Set.image_iUnion]
-      exact MeasurableSet.iUnion hg
+    | compl s _ ihs =>
+      rw [← range_diff_image (hg.injective.prodMap hf.injective), range_prod_map]
+      exact .diff (.prod hg.measurableSet_range hf.measurableSet_range) ihs
+    | iUnion f _ _ ihf =>
+      simpa only [image_iUnion] using .iUnion ihf
 
 @[deprecated (since := "2024-12-11")]
 alias MeasurableEmbedding.prod_mk := MeasurableEmbedding.prodMap

Mathlib/MeasureTheory/Measure/GiryMonad.lean

@@ -69,11 +69,14 @@ theorem _root_.Measurable.measure_of_isPiSystem {μ : α → Measure β} [∀ a,
     (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s) (h_univ : Measurable fun a ↦ μ a univ) :
     Measurable μ := by
   rw [measurable_measure]
-  refine MeasurableSpace.induction_on_inter hgen hpi (by simp) h_basic ?_ ?_
-  · intro s hsm ihs
+  intro s hs
+  induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
+  | empty => simp
+  | basic s hs => exact h_basic s hs
+  | compl s hsm ihs =>
     simp only [measure_compl hsm (measure_ne_top _ _)]
     exact h_univ.sub ihs
-  · intro f hfd hfm ihf
+  | iUnion f hfd hfm ihf =>
     simpa only [measure_iUnion hfd hfm] using .ennreal_tsum ihf
 
 theorem _root_.Measurable.measure_of_isPiSystem_of_isProbabilityMeasure {μ : α → Measure β}

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -271,7 +271,8 @@ theorem _root_.MeasurableSpace.ae_induction_on_inter
         Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C x (f i)) → C x (⋃ i, f i)) :
     ∀ᵐ x ∂μ, ∀ ⦃t⦄, MeasurableSet t → C x t := by
   filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
-    using MeasurableSpace.induction_on_inter h_eq h_inter hx_empty hx_basic hx_compl hx_union
+    using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
+      h_eq h_inter hx_empty hx_basic hx_compl hx_union
 
 end ae
 

Mathlib/MeasureTheory/Measure/Prod.lean

@@ -70,23 +70,20 @@ variable {μ μ' : Measure α} {ν ν' : Measure β} {τ : Measure γ}
   a measurable function. `measurable_measure_prod_mk_left` is strictly more general. -/
 theorem measurable_measure_prod_mk_left_finite [IsFiniteMeasure ν] {s : Set (α × β)}
     (hs : MeasurableSet s) : Measurable fun x => ν (Prod.mk x ⁻¹' s) := by
-  classical
-  refine induction_on_inter (C := fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s))
-    generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ hs
-  · simp
-  · rintro _ ⟨s, hs, t, _, rfl⟩
-    simp only [mk_preimage_prod_right_eq_if, measure_if]
-    exact measurable_const.indicator hs
-  · intro t ht h2t
-    simp_rw [preimage_compl, measure_compl (measurable_prod_mk_left ht) (measure_ne_top ν _)]
-    exact h2t.const_sub _
-  · intro f h1f h2f h3f
-    simp_rw [preimage_iUnion]
-    have : ∀ b, ν (⋃ i, Prod.mk b ⁻¹' f i) = ∑' i, ν (Prod.mk b ⁻¹' f i) := fun b =>
-      measure_iUnion (fun i j hij => Disjoint.preimage _ (h1f hij)) fun i =>
-        measurable_prod_mk_left (h2f i)
-    simp_rw [this]
-    apply Measurable.ennreal_tsum h3f
+  induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
+  | empty => simp
+  | basic s hs =>
+    obtain ⟨s, hs, t, -, rfl⟩ := hs
+    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
+      using measurable_const.indicator hs
+  | compl s hs ihs =>
+    simp_rw [preimage_compl, measure_compl (measurable_prod_mk_left hs) (measure_ne_top ν _)]
+    exact ihs.const_sub _
+  | iUnion f hfd hfm ihf =>
+    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
+      rw [preimage_iUnion, measure_iUnion]
+      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prod_mk_left (hfm i)]
+    simpa only [this] using Measurable.ennreal_tsum ihf
 
 /-- If `ν` is an s-finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }`
   is a measurable function. -/

Mathlib/MeasureTheory/Measure/Restrict.lean

@@ -423,17 +423,18 @@ theorem ext_of_generateFrom_of_cover {S T : Set (Set α)} (h_gen : ‹_› = gen
   refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_
   ext1 u hu
   simp only [restrict_apply hu]
-  refine induction_on_inter h_gen h_inter ?_ (ST_eq t ht) ?_ ?_ hu
-  · simp only [Set.empty_inter, measure_empty]
-  · intro v hv hvt
+  induction u, hu using induction_on_inter h_gen h_inter with
+  | empty => simp only [Set.empty_inter, measure_empty]
+  | basic u hu => exact ST_eq _ ht _ hu
+  | compl u hu ihu =>
     have := T_eq t ht
-    rw [Set.inter_comm] at hvt ⊢
-    rwa [← measure_inter_add_diff t hv, ← measure_inter_add_diff t hv, ← hvt,
+    rw [Set.inter_comm] at ihu ⊢
+    rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
       ENNReal.add_right_inj] at this
     exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)
-  · intro f hfd hfm h_eq
-    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at h_eq ⊢
-    simp only [measure_iUnion hfd hfm, h_eq]
+  | iUnion f hfd hfm ihf =>
+    simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢
+    simp only [measure_iUnion hfd hfm, ihf]
 
 /-- Two measures are equal if they are equal on the π-system generating the σ-algebra,
   and they are both finite on an increasing spanning sequence of sets in the π-system.

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -1331,14 +1331,14 @@ theorem ext_on_measurableSpace_of_generate_finite {α} (m₀ : MeasurableSpace 
     constructor
     rw [← h_univ]
     apply IsFiniteMeasure.measure_univ_lt_top
-  refine induction_on_inter hA hC (by simp) hμν ?_ ?_ hs
-  · intro t h1t h2t
-    have h1t_ : @MeasurableSet α m₀ t := h _ h1t
-    rw [@measure_compl α m₀ μ t h1t_ (@measure_ne_top α m₀ μ _ t),
-      @measure_compl α m₀ ν t h1t_ (@measure_ne_top α m₀ ν _ t), h_univ, h2t]
-  · intro f h1f h2f h3f
-    have h2f_ : ∀ i : ℕ, @MeasurableSet α m₀ (f i) := fun i => h _ (h2f i)
-    simp [measure_iUnion, h1f, h3f, h2f_]
+  induction s, hs using induction_on_inter hA hC with
+  | empty => simp
+  | basic t ht => exact hμν t ht
+  | compl t htm iht =>
+    rw [measure_compl (h t htm) (measure_ne_top _ _), measure_compl (h t htm) (measure_ne_top _ _),
+      iht, h_univ]
+  | iUnion f hfd hfm ihf =>
+    simp [measure_iUnion, hfd, h _ (hfm _), ihf]
 
 /-- Two finite measures are equal if they are equal on the π-system generating the σ-algebra
   (and `univ`). -/

Mathlib/MeasureTheory/PiSystem.lean

@@ -664,26 +664,34 @@ theorem generateFrom_eq {s : Set (Set α)} (hs : IsPiSystem s) :
 
 end DynkinSystem
 
-theorem induction_on_inter {C : Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α]
-    (h_eq : m = generateFrom s) (h_inter : IsPiSystem s) (h_empty : C ∅) (h_basic : ∀ t ∈ s, C t)
-    (h_compl : ∀ t, MeasurableSet t → C t → C tᶜ)
-    (h_union :
-      ∀ f : ℕ → Set α,
-        Pairwise (Disjoint on f) → (∀ i, MeasurableSet (f i)) → (∀ i, C (f i)) → C (⋃ i, f i)) :
-    ∀ ⦃t⦄, MeasurableSet t → C t :=
+/-- Induction principle for measurable sets.
+If `s` is a π-system that generates the product `σ`-algebra on `α`
+and a predicate `C` defined on measurable sets is true
+
+- on the empty set;
+- on each set `t ∈ s`;
+- on the complement of a measurable set that satisfies `C`;
+- on the union of a sequence of pairwise disjoint measurable sets that satisfy `C`,
+
+then it is true on all measurable sets in `α`. -/
+@[elab_as_elim]
+theorem induction_on_inter {m : MeasurableSpace α} {C : ∀ s : Set α, MeasurableSet s → Prop}
+    {s : Set (Set α)} (h_eq : m = generateFrom s) (h_inter : IsPiSystem s)
+    (empty : C ∅ .empty) (basic : ∀ t (ht : t ∈ s), C t <| h_eq ▸ .basic t ht)
+    (compl : ∀ t (htm : MeasurableSet t), C t htm → C tᶜ htm.compl)
+    (iUnion : ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → ∀ (hfm : ∀ i, MeasurableSet (f i)),
+      (∀ i, C (f i) (hfm i)) → C (⋃ i, f i) (.iUnion hfm)) :
+    ∀ t (ht : MeasurableSet t), C t ht := by
   have eq : MeasurableSet = DynkinSystem.GenerateHas s := by
     rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
     rfl
-  fun t ht =>
-  have : DynkinSystem.GenerateHas s t := by rwa [eq] at ht
-  this.recOn h_basic h_empty
-    (fun {t} ht =>
-      h_compl t <| by
-        rw [eq]
-        exact ht)
-    fun {f} hf ht =>
-    h_union f hf fun i => by
-      rw [eq]
-      exact ht _
+  suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from
+    fun t ht ↦ this t (eq ▸ ht)
+  intro t ht
+  induction ht with
+  | basic u hu => exact basic u hu
+  | empty => exact empty
+  | @compl u hu ihu => exact compl _ (eq ▸ hu) ihu
+  | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf
 
 end MeasurableSpace

Mathlib/Probability/Independence/Kernel.lean

@@ -45,7 +45,7 @@ definitions in the particular case of the usual independence notion.
 * `ProbabilityTheory.Kernel.IndepSets.Indep`: variant with two π-systems.
 -/
 
-open MeasureTheory MeasurableSpace
+open Set MeasureTheory MeasurableSpace
 
 open scoped MeasureTheory ENNReal
 
@@ -479,32 +479,22 @@ theorem IndepSets.indep_aux {m₂ m : MeasurableSpace Ω}
     ∀ᵐ a ∂μ, κ a (t1 ∩ t2) = κ a t1 * κ a t2 := by
   rcases eq_zero_or_isMarkovKernel κ with rfl | h
   · simp
-  refine @induction_on_inter _ (fun t ↦ ∀ᵐ a ∂μ, κ a (t1 ∩ t) = κ a t1 * κ a t) _
-    m₂ hpm2 hp2 ?_ ?_ ?_ ?_ t2 ht2m
-  · simp only [Set.inter_empty, measure_empty, mul_zero, eq_self_iff_true,
-      Filter.eventually_true]
-  · exact fun t ht_mem_p2 ↦ hyp t1 t ht1 ht_mem_p2
-  · intros t ht h
-    filter_upwards [h] with a ha
-    have : t1 ∩ tᶜ = t1 \ (t1 ∩ t) := by
-      rw [Set.diff_self_inter, Set.diff_eq_compl_inter, Set.inter_comm]
-    rw [this,
-      measure_diff Set.inter_subset_left (ht1m.inter (h2 _ ht)).nullMeasurableSet
-        (measure_ne_top (κ a) _),
-      measure_compl (h2 _ ht) (measure_ne_top (κ a) t), measure_univ,
-      ENNReal.mul_sub (fun _ _ ↦ measure_ne_top (κ a) _), mul_one, ha]
-  · intros f hf_disj hf_meas h
-    rw [← ae_all_iff] at h
-    filter_upwards [h] with a ha
-    rw [Set.inter_iUnion, measure_iUnion]
-    · rw [measure_iUnion hf_disj (fun i ↦ h2 _ (hf_meas i))]
-      rw [← ENNReal.tsum_mul_left]
-      congr with i
-      rw [ha i]
-    · intros i j hij
-      rw [Function.onFun, Set.inter_comm t1, Set.inter_comm t1]
-      exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))
-    · exact fun i ↦ ht1m.inter (h2 _ (hf_meas i))
+  induction t2, ht2m using induction_on_inter hpm2 hp2 with
+  | empty => simp
+  | basic u hu => exact hyp t1 u ht1 hu
+  | compl u hu ihu =>
+    filter_upwards [ihu] with a ha
+    rw [← Set.diff_eq, ← Set.diff_self_inter,
+      measure_diff inter_subset_left (ht1m.inter (h2 _ hu)).nullMeasurableSet (measure_ne_top _ _),
+      ha, measure_compl (h2 _ hu) (measure_ne_top _ _), measure_univ, ENNReal.mul_sub, mul_one]
+    exact fun _ _ ↦ measure_ne_top _ _
+  | iUnion f hfd hfm ihf =>
+    rw [← ae_all_iff] at ihf
+    filter_upwards [ihf] with a ha
+    rw [inter_iUnion, measure_iUnion, measure_iUnion hfd fun i ↦ h2 _ (hfm i)]
+    · simp only [ENNReal.tsum_mul_left, ha]
+    · exact hfd.mono fun i j h ↦ (h.inter_left' _).inter_right' _
+    · exact fun i ↦ .inter ht1m (h2 _ <| hfm i)
 
 /-- The measurable space structures generated by independent pi-systems are independent. -/
 theorem IndepSets.indep {m1 m2 m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
@@ -515,26 +505,23 @@ theorem IndepSets.indep {m1 m2 m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ :
   rcases eq_zero_or_isMarkovKernel κ with rfl | h
   · simp
   intros t1 t2 ht1 ht2
-  refine @induction_on_inter _ (fun t ↦ ∀ᵐ (a : α) ∂μ, κ a (t ∩ t2) = κ a t * κ a t2) _ m1 hpm1 hp1
-    ?_ ?_ ?_ ?_ _ ht1
-  · simp only [Set.empty_inter, measure_empty, zero_mul, eq_self_iff_true,
-      Filter.eventually_true]
-  · intros t ht_mem_p1
-    have ht1 : MeasurableSet[m] t := by
-      refine h1 _ ?_
-      rw [hpm1]
-      exact measurableSet_generateFrom ht_mem_p1
-    exact IndepSets.indep_aux h2 hp2 hpm2 hyp ht_mem_p1 ht1 ht2
-  · intros t ht h
-    filter_upwards [h] with a ha
+  induction t1, ht1 using induction_on_inter hpm1 hp1 with
+  | empty =>
+    simp only [Set.empty_inter, measure_empty, zero_mul, eq_self_iff_true, Filter.eventually_true]
+  | basic t ht =>
+    refine IndepSets.indep_aux h2 hp2 hpm2 hyp ht (h1 _ ?_) ht2
+    rw [hpm1]
+    exact measurableSet_generateFrom ht
+  | compl t ht iht =>
+    filter_upwards [iht] with a ha
     have : tᶜ ∩ t2 = t2 \ (t ∩ t2) := by
       rw [Set.inter_comm t, Set.diff_self_inter, Set.diff_eq_compl_inter]
     rw [this, Set.inter_comm t t2,
       measure_diff Set.inter_subset_left ((h2 _ ht2).inter (h1 _ ht)).nullMeasurableSet
         (measure_ne_top (κ a) _),
       Set.inter_comm, ha, measure_compl (h1 _ ht) (measure_ne_top (κ a) t), measure_univ,
       mul_comm (1 - κ a t), ENNReal.mul_sub (fun _ _ ↦ measure_ne_top (κ a) _), mul_one, mul_comm]
-  · intros f hf_disj hf_meas h
+  | iUnion f hf_disj hf_meas h =>
     rw [← ae_all_iff] at h
     filter_upwards [h] with a ha
     rw [Set.inter_comm, Set.inter_iUnion, measure_iUnion]