-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v'),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inl :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inr inr₁ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u'),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inr₂ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (hv : v ≤ v'),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inr₃ inr₄ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (hv : v' < v),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inr₅ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (hv : v' < v),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inr₆ : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (hv : v' < v),
  (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α)).PairwiseDisjoint id
Tactic: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind