awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
s_mem : s ∈ generateSetAlgebra 𝒜
base :
  ∀ (u : Set α) (u_mem : u ∈ 𝒜),
    ∃ (A : Set (Set (Set α))),
      A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
empty :
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧
      (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ Eq.{u_1 + 1} (α := Set α) ∅ (⋃ a ∈ A, ⋂ t ∈ a, t)
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t
have compl : ∀ (u : Set α),
  generateSetAlgebra 𝒜 u →
    ∀
      (u_ind :
        ∃ (A : Set (Set (Set α))),
          A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t),
      ∃ (A : Set (Set (Set α))),
        A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
Tactic: induction s_mem with
  | base u u_mem =>
    refine ⟨{{u}}, finite_singleton {u},
      fun a ha ↦ eq_of_mem_singleton ha ▸ finite_singleton u,
      fun a ha t ht ↦ ?_, by simp⟩
    rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *
    exact Or.inl u_mem
  | empty => exact ⟨∅, finite_empty, fun _ h ↦ (notMem_empty _ h).elim,
    fun _ ha _ _ ↦ (notMem_empty _ ha).elim, by simp⟩
  | compl u _ u_ind =>
    rcases u_ind with ⟨A, A_fin, mem_A, hA, u_eq⟩
    have := finite_coe_iff.2 A_fin
    have := fun a : A ↦ finite_coe_iff.2 <| mem_A a.1 a.2
    refine ⟨{{(f a).1ᶜ | a : A} | f : (Π a : A, ↑a)}, finite_coe_iff.1 inferInstance,
      fun a ⟨f, hf⟩ ↦ hf ▸ finite_coe_iff.1 inferInstance, fun a ha t ht ↦ ?_, ?_⟩
    · rcases ha with ⟨f, rfl⟩
      rcases ht with ⟨a, rfl⟩
      rw [compl_compl, or_comm]
      exact hA a.1 a.2 (f a).1 (f a).2
    · ext x
      simp only [u_eq, compl_iUnion, compl_iInter, mem_iInter, mem_iUnion, mem_compl_iff,
        exists_prop, Subtype.exists, mem_setOf_eq, iUnion_exists, iUnion_iUnion_eq',
        iInter_exists]
      constructor <;> intro hx
      · choose f hf using hx
        exact ⟨fun ⟨a, ha⟩ ↦ ⟨f a ha, (hf a ha).1⟩, fun _ a ha h ↦ by rw [← h]; exact (hf a ha).2⟩
      · rcases hx with ⟨f, hf⟩
        exact fun a ha ↦ ⟨f ⟨a, ha⟩, (f ⟨a, ha⟩).2, hf (f ⟨a, ha⟩)ᶜ a ha rfl⟩
  | union u v _ _ u_ind v_ind =>
    rcases u_ind with ⟨Au, Au_fin, mem_Au, hAu, u_eq⟩
    rcases v_ind with ⟨Av, Av_fin, mem_Av, hAv, v_eq⟩
    refine ⟨Au ∪ Av, Au_fin.union Av_fin, ?_, ?_, by rw [u_eq, v_eq, ← biUnion_union]⟩
    · rintro a (ha | ha)
      · exact mem_Au a ha
      · exact mem_Av a ha
    · rintro a (ha | ha) t ht
      · exact hAu a ha t ht
      · exact hAv a ha t ht
Cleared hypotheses: s_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ ℬ.Countable
have apply : Set.Countable.{u_1} (α := Set α) {s : Set α | sᶜ ∈ 𝒜}
Tactic: apply h.union
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}
have h₁ : ∀ (s : Set α), s ∈ compl '' 𝒜 ↔ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ 𝒜} s
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ Set.Countable.{u_1} (α := Set α) {s : Set α | sᶜ ∈ 𝒜}
have this : compl '' 𝒜 = {s : Set α | sᶜ ∈ 𝒜}
Tactic: have : compl '' 𝒜 = {s | sᶜ ∈ 𝒜} := by
      ext s
      simpa using ⟨fun ⟨x, x_mem, hx⟩ ↦ by simp [← hx, x_mem], fun hs ↦ ⟨sᶜ, hs, by simp⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
⊢ (generateSetAlgebra 𝒜).Countable
have count_ℬ : ℬ.Countable
Tactic: have count_ℬ : ℬ.Countable := by
    apply h.union
    have : compl '' 𝒜 = {s | sᶜ ∈ 𝒜} := by
      ext s
      simpa using ⟨fun ⟨x, x_mem, hx⟩ ↦ by simp [← hx, x_mem], fun hs ↦ ⟨sᶜ, hs, by simp⟩⟩
    exact this ▸ h.image compl
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
⊢ (generateSetAlgebra 𝒜).Countable
have count_𝒞 : 𝒞.Countable
Tactic: have count_𝒞 : 𝒞.Countable := countable_setOf_finite_subset (countable_coe_iff.1 count_ℬ)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
⊢ (generateSetAlgebra 𝒜).Countable
have count_𝒟 : 𝒟.Countable
Tactic: have count_𝒟 : 𝒟.Countable := countable_setOf_finite_subset (countable_coe_iff.1 count_𝒞)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
s : Set α
s_mem : s ∈ generateSetAlgebra 𝒜
⊢ s ∈ f '' 𝒟
have rcases : ∀ (A : Set (Set (Set α))) (A_fin : A.Finite) (mem_A : ∀ a ∈ A, a.Finite) (hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜)
  (s_mem : ⋃ a ∈ A, ⋂ t ∈ a, t ∈ generateSetAlgebra 𝒜), ⋃ a ∈ A, ⋂ t ∈ a, t ∈ f '' 𝒟
Tactic: rcases mem_generateSetAlgebra_elim s_mem with ⟨A, A_fin, mem_A, hA, rfl⟩
Cleared hypotheses: s, s_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (hypothesis)
Goal:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s : Set α | s ∈ 𝒜} ∪ {s : Set α | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun (A : Set (Set (Set α))) ↦ ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a : Set (Set α) | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A : Set (Set (Set α)) | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
⊢ (generateSetAlgebra 𝒜).Countable
have this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟
Tactic: have : generateSetAlgebra 𝒜 ⊆ f '' 𝒟 := by
    intro s s_mem
    rcases mem_generateSetAlgebra_elim s_mem with ⟨A, A_fin, mem_A, hA, rfl⟩
    exact ⟨A, ⟨A_fin, fun a ha ↦ ⟨mem_A a ha, hA a ha⟩⟩, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have obtain : ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
  (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
Tactic: obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_1 : I.sup id = s \ t
Tactic: refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_1 : I.sup id = s \ t
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_2 : (↑((Finpartition.ofErase (a := s \ t) I sorry sorry).parts (a := s \ t)) : Set (Set α)) ⊆ C
Tactic: refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
⊢ I.sup id = s \ t
have refine_1 : sSup (↑I : Set (Set α)) = s \ t
Tactic: rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_1 : sSup (↑I : Set (Set α)) = s \ t
⊢ I.sup id = s \ t
have refine_1₁ : ⋃₀ (↑I : Set (Set α)) = s \ t
Tactic: rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_1 : sSup (↑I : Set (Set α)) = s \ t
refine_1₁ : ⋃₀ (↑I : Set (Set α)) = s \ t
⊢ I.sup id = s \ t
have refine_1₂ : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑I : Set (Set α))
Tactic: rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
⊢ (↑((Finpartition.ofErase (a := s \ t) I ⋯ ⋯).parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_2 : (↑(I.erase ⊥) : Set (Set α)) ⊆ C
Tactic: grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
I : Finset (Set α)
hIC : (↑I : Set (Set α)) ⊆ C
hI : (↑I : Set (Set α)).PairwiseDisjoint id
hst : s \ t = ⋃₀ (↑I : Set (Set α))
refine_2 : (↑(I.erase ⊥) : Set (Set α)) ⊆ C
refine_2₁ : (↑I : Set (Set α)) ⊆ C
⊢ (↑((Finpartition.ofErase (a := s \ t) I ⋯ ⋯).parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_2₂ : C ⊆ C
Tactic: grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have obtain : ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
  (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
Tactic: classical
  obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht
  refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
  · rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
  · grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
obtain :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_1 : ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
  (hst : s \ t = ⋃₀ (↑I : Set (Set α))), I.sup id = s \ t
Tactic: classical
  obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht
  refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
  · rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
  · grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
obtain :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
refine_1 :
  ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
    (hst : s \ t = ⋃₀ (↑I : Set (Set α))), I.sup id = s \ t
⊢ ∃ (P : Finpartition (s \ t)), (↑(P.parts (a := s \ t)) : Set (Set α)) ⊆ C
have refine_2 : ∀ (I : Finset (Set α)) (hIC : (↑I : Set (Set α)) ⊆ C) (hI : (↑I : Set (Set α)).PairwiseDisjoint id)
  (hst : s \ t = ⋃₀ (↑I : Set (Set α))),
  (↑((Finpartition.ofErase (a := s \ t) I sorry sorry).parts (a := s \ t)) : Set (Set α)) ⊆ C
Tactic: classical
  obtain ⟨I, hIC, hI, hst⟩ := hC.diff_eq_sUnion' s hs t ht
  refine ⟨.ofErase I (supIndep_iff_pairwiseDisjoint.mpr hI) ?_, ?_⟩
  · rw [sup_id_eq_sSup, sSup_eq_sUnion, hst]
  · grw [Finpartition.ofErase_parts, Finset.erase_subset, hIC]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup' hS id)), (↑(P.parts (a := S.sup' hS id)) : Set (Set α)) ⊆ C
have rw : ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
Tactic: rw [sup'_eq_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑(insert s S) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
have hSC₁ : s ∈ C ∧ (↑S : Set (Set α)) ⊆ C
Tactic: rw [coe_insert, insert_subset_iff] at hSC
Cleared hypotheses: hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : s ∈ C ∧ (↑S : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
have hsC : s ∈ C
Tactic: obtain ⟨hsC, hSC⟩ := hSC
Cleared hypotheses: hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : s ∈ C ∧ (↑S : Set (Set α)) ⊆ C
hsC : s ∈ C
⊢ ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
have hSC₁ : (↑S : Set (Set α)) ⊆ C
Tactic: obtain ⟨hsC, hSC⟩ := hSC
Cleared hypotheses: hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
have insert : ∀ (P : Finpartition (S.sup id)) (hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C),
  ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
Tactic: obtain ⟨P, hP⟩ := ih hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s S).sup id)) : Set (Set α)) ⊆ C
have insert : ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
Tactic: rw [sup_insert, sup_comm, id]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
have insert : ⊥ ∉ S → ∀ (hsC : ⊥ ∈ C), ∃ (P : Finpartition (S.sup id ⊔ ⊥)), (↑(P.parts (a := S.sup id ⊔ ⊥)) : Set (Set α)) ⊆ C
Tactic: rcases eq_or_ne s ⊥ with rfl | hs
Cleared hypotheses: s, h, hsC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
insert :
  ⊥ ∉ S → ∀ (hsC : ⊥ ∈ C), ∃ (P : Finpartition (S.sup id ⊔ ⊥)), (↑(P.parts (a := S.sup id ⊔ ⊥)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
have insert₁ : ∀ (hs : s ≠ ⊥), ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
Tactic: rcases eq_or_ne s ⊥ with rfl | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
h : ⊥ ∉ S
hsC : ⊥ ∈ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ ⊥)), (↑(P.parts (a := S.sup id ⊔ ⊥)) : Set (Set α)) ⊆ C
have insert : ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
Tactic: rw [sup_bot_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
⊢ ∀ t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s),
    ∃ (Q : Finpartition t), (↑(Q.parts (a := t)) : Set (Set α)) ⊆ C
have simp_rw : ∀ (t : Set α),
  (∃ d ∈ P.parts (a := S.sup id), ¬d ≤ s ∧ d \ s = t) → ∃ (Q : Finpartition t), (↑(Q.parts (a := t)) : Set (Set α)) ⊆ C
Tactic: simp_rw [Finpartition.mem_avoid]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
have insert : ∀ (Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t)
  (hQ :
    ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
      (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C),
  ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
Tactic: choose Q hQ using show ∀ t ∈ (P.avoid s).parts, ∃ Q : Finpartition t, ↑Q.parts ⊆ C by
        simp_rw [Finpartition.mem_avoid]
        rintro _ ⟨t, ht, -, rfl⟩
        exact hC.exists_finpartition_diff (hP ht) hsC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
have insert : (↑((((P.avoid (a := S.sup id) s).bind (a := S.sup id \ s) Q).extend (a := S.sup id \ s) (b := s) (c := S.sup id ⊔ s) hs
            sorry sorry).parts
        (a := S.sup id ⊔ s)) :
    Set (Set α)) ⊆
  C
Tactic: exists P.avoid s |>.bind Q |>.extend hs disjoint_sdiff_left (sdiff_sup_self _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
⊢ (↑((((P.avoid (a := S.sup id) s).bind (a := S.sup id \ s) Q).extend (a := S.sup id \ s) (b := s) (c := S.sup id ⊔ s)
              hs ⋯ ⋯).parts
          (a := S.sup id ⊔ s)) :
      Set (Set α)) ⊆
    C
have insert : s ∈ C ∧
  ∀ (a : Set α) (b : a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s))
    (j :
      Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b ∈
        (↑(P.avoid (a := S.sup id) s).parts (a := S.sup id \ s).attach : Set ↥(P.avoid s).parts)),
    (↑(Finpartition.parts (a :=
            (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
              Set α))
            (Q
              (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                Set α)
              sorry)) :
        Set (Set α)) ⊆
      C
Tactic: rw [Finpartition.extend_parts, coe_insert, insert_subset_iff, Finpartition.bind_parts,
        coe_biUnion, iUnion₂_subset_iff, Subtype.forall]