awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
compl :
  ∀ (a : Set (Set α))
    (ha :
      Membership.mem (γ := Set (Set (Set α)))
        {x : Set (Set α) |
          ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
            {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
        a)
    (t : Set α) (ht : t ∈ a), t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
have compl₁ : uᶜ =
  ⋃ (a : Set (Set α)),
    ⋃ (_ :
      Membership.mem (γ := Set (Set (Set α)))
        {x : Set (Set α) |
          ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
            {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
        a),
      ⋂ t ∈ a, t
Tactic: 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 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
a : Set (Set α)
ha :
  Membership.mem (γ := Set (Set (Set α)))
    {x : Set (Set α) |
      ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
        {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
    a
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
have compl : ∀ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1))
  (ht : Membership.mem (γ := Set (Set α)) {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} t),
  t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
Tactic: rcases ha with ⟨f, rfl⟩
Cleared hypotheses: a, ha, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
t : Set α
f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)
ht : Membership.mem (γ := Set (Set α)) {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} t
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
have compl : ∀ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ ∈ 𝒜 ∨ (↑(f a) : Set α)ᶜᶜ ∈ 𝒜
Tactic: rcases ht with ⟨a, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)
a : (↑A : Type u_1)
⊢ (↑(f a) : Set α)ᶜ ∈ 𝒜 ∨ (↑(f a) : Set α)ᶜᶜ ∈ 𝒜
have compl : (↑(f a) : Set α) ∈ 𝒜 ∨ (↑(f a) : Set α)ᶜ ∈ 𝒜
Tactic: rw [compl_compl, or_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
⊢ uᶜ =
    ⋃ (a : Set (Set α)),
      ⋃ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {x : Set (Set α) |
            ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
              {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
          a),
        ⋂ t ∈ a, t
have compl : ∀ (x : α),
  x ∈ uᶜ ↔
    Membership.mem (γ := Set α)
      (⋃ (a : Set (Set α)),
        ⋃ (_ :
          Membership.mem (γ := Set (Set (Set α)))
            {x : Set (Set α) |
              ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
                {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
            a),
          ⋂ t ∈ a, t)
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
⊢ x ∈ uᶜ ↔
    Membership.mem (γ := Set α)
      (⋃ (a : Set (Set α)),
        ⋃ (_ :
          Membership.mem (γ := Set (Set (Set α)))
            {x : Set (Set α) |
              ∃ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
                {x : Set α | ∃ (a : (↑A : Type u_1)), (↑(f a) : Set α)ᶜ = x} = x}
            a),
          ⋂ t ∈ a, t)
      x
have compl : (∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2) ↔
  ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
⊢ (∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2) ↔
    ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
      ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
        (i :
          (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) :
                    (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) : Set (Set α)) : Type u_1)) :
                Set α)ᶜ =
            i_1),
        x ∈ i_1
have compl : (∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2) →
  ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
compl :
  (∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2) →
    ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
      ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
        (i :
          (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) :
                    (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) : Set (Set α)) : Type u_1)) :
                Set α)ᶜ =
            i_1),
        x ∈ i_1
⊢ (∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2) ↔
    ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
      ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
        (i :
          (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) :
                    (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) : Set (Set α)) : Type u_1)) :
                Set α)ᶜ =
            i_1),
        x ∈ i_1
have compl₁ : (∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1) →
  ∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
hx : ∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2
⊢ ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1
have compl : ∀ (f : (i : Set (Set α)) → (i : i ∈ A) → Set α) (hf : ∀ (i : Set (Set α)) (i_1 : i ∈ A), f i i_1 ∈ i ∧ x ∉ f i i_1),
  ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 sorry) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1
Tactic: choose f hf using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
f : (i : Set (Set α)) → (i : i ∈ A) → Set α
hf : ∀ (i : Set (Set α)) (i_1 : i ∈ A), f i i_1 ∈ i ∧ x ∉ f i i_1
x_1 : Set α
a : Set (Set α)
ha : a ∈ A
h :
  (↑((fun (x_2 : (↑A : Type u_1)) ↦
              (match (motive := (x : (↑A : Type u_1)) → (↑(↑x : Set (Set α)) : Type u_1)) x_2 with
                | ⟨a, ha⟩ =>
                  Subtype.mk (p := fun (x : Set α) ↦
                    x ∈ (↑(Subtype.mk (p := fun (x : Set (Set α)) ↦ x ∈ A) a ha) : Set (Set α))) (f a ha) ⋯ :
                (↑(↑x_2 : Set (Set α)) : Type u_1)))
            (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) a ⋯)) :
        Set α)ᶜ =
    x_1
⊢ x ∈ x_1
have rw : Membership.mem (γ := Set α)
  (↑((fun (x_2 : (↑A : Type u_1)) ↦
            (match (motive := (x : (↑A : Type u_1)) → (↑(↑x : Set (Set α)) : Type u_1)) x_2 with
              | ⟨a, ha⟩ =>
                Subtype.mk (p := fun (x : Set α) ↦
                  x ∈ (↑(Subtype.mk (p := fun (x : Set (Set α)) ↦ x ∈ A) a ha) : Set (Set α))) (f a ha) sorry :
              (↑(↑x_2 : Set (Set α)) : Type u_1)))
          (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) a sorry)) :
      Set α)ᶜ
  x
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this_1 : Finite.{u_1 + 1} (↑A : Type u_1)
this : ∀ (a : (↑A : Type u_1)), Finite.{u_1 + 1} (↑(↑a : Set (Set α)) : Type u_1)
x : α
hx :
  ∃ (i : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1)),
    ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A)
      (i :
        (↑(i (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_2 ⋯) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i_1),
      x ∈ i_1
⊢ ∀ (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2
have compl : ∀ (f : (a : (↑A : Type u_1)) → (↑(↑a : Set (Set α)) : Type u_1))
  (hf :
    ∀ (i : Set α) (i_1 : Set (Set α)) (i_2 : i_1 ∈ A)
      (i_3 :
        (↑(f (Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_1 sorry) :
                  (↑(↑(Subtype.mk (p := fun (a : Set (Set α)) ↦ a ∈ A) i_1 sorry) : Set (Set α)) : Type u_1)) :
              Set α)ᶜ =
          i),
      x ∈ i)
  (i : Set (Set α)) (i_1 : i ∈ A), ∃ i_2 ∈ i, x ∉ i_2
Tactic: rcases hx with ⟨f, hf⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
u_ind :
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
v_ind :
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ v = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
have union : ∀ (Au : Set (Set (Set α))) (Au_fin : Au.Finite) (mem_Au : ∀ a ∈ Au, a.Finite) (hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜)
  (u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t),
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
Tactic: rcases u_ind with ⟨Au, Au_fin, mem_Au, hAu, u_eq⟩
Cleared hypotheses: u_ind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
v_ind :
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ v = ⋃ a ∈ A, ⋂ t ∈ a, t
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
have union : ∀ (Av : Set (Set (Set α))) (Av_fin : Av.Finite) (mem_Av : ∀ a ∈ Av, a.Finite) (hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜)
  (v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t),
  ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
Tactic: rcases v_ind with ⟨Av, Av_fin, mem_Av, hAv, v_eq⟩
Cleared hypotheses: v_ind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ u ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
have rw : (⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
Tactic: rw [u_eq, v_eq, ← biUnion_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
rw : (⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
⊢ u ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
have rw₁ : Eq.{u_1 + 1} (α := Set α) ((⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ ⋃ a ∈ Av, ⋂ t ∈ a, t) (⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t)
Tactic: rw [u_eq, v_eq, ← biUnion_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
rw : (⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
rw₁ : Eq.{u_1 + 1} (α := Set α) ((⋃ a ∈ Au, ⋂ t ∈ a, t) ∪ ⋃ a ∈ Av, ⋂ t ∈ a, t) (⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t)
⊢ u ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t
have rw₂ : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ Au ∪ Av, ⋂ t ∈ x, t) (⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t)
Tactic: rw [u_eq, v_eq, ← biUnion_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
have union : ∀ a ∈ Au ∪ Av, a.Finite
Tactic: refine ⟨Au ∪ Av, Au_fin.union Av_fin, ?_, ?_, by rw [u_eq, v_eq, ← biUnion_union]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs : generateSetAlgebra 𝒜 u
ht : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
union : ∀ a ∈ Au ∪ Av, a.Finite
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t
have union₁ : ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
Tactic: refine ⟨Au ∪ Av, Au_fin.union Av_fin, ?_, ?_, by rw [u_eq, v_eq, ← biUnion_union]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetAlgebra (goal)
Goal:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
s_mem : s ∈ generateSetAlgebra 𝒜
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t
have 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
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 α)
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
⊢ ∃ (A : Set (Set (Set α))),
    A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t
have 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)
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