awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (hypothesis)
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
    (fun (x : ℝ × (Fin n → ℝ)) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
    (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
have this : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
  (fun (θ : Fin (n + 1) → ℝ) ↦
    HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
  (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) volume
Tactic: have := hf.function_integrable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin (n + 1) → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
    (fun (x : ℝ × (Fin n → ℝ)) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
    (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
have hf₁ : ∀
  (this :
    IntegrableOn.{0, u_1} (α := ℝ × (Fin n → ℝ)) (ε := E) (mα := Prod.instMeasurableSpace)
      ((fun (θ : Fin (n + 1) → ℝ) ↦
          HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ))) ∘
        (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ))
      (preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
        (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π))
      volume),
  IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
    (fun (x : ℝ × (Fin n → ℝ)) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
    (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
Tactic: rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h : MeasurableSet s
⊢ MeasurableSet s
have rw : MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
Tactic: rw [map_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
have pos : ∀ (h : b ∈ s), MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h : MeasurableSet s
pos : ∀ (h : b ∈ s), MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
have neg : ∀ (h : b ∉ s), MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
Tactic: by_cases h : b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
have pos : b ∈ s → MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
Tactic: by_cases b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
pos : b ∈ s → MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
have neg : b ∉ s → MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
Tactic: by_cases b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) s : Set (Set α)) t
⊢ MeasurableSet t
have rcases : ∀ (P : Finset (Set α)) (hP : P.Nonempty) (PC : (↑P : Set (Set α)) ⊆ s), MeasurableSet (P.sup' hP id)
Tactic: rcases ht with ⟨P, hP, PC, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : (↑P : Set (Set α)) ⊆ s
⊢ MeasurableSet (P.sup' hP id)
have rw : MeasurableSet (⋃₀ (↑P : Set (Set α)))
Tactic: rw [Finset.sup'_eq_sup, Finset.sup_id_set_eq_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Measurable f
have a : Nontrivial β
Tactic: nontriviality β
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h : Nontrivial β
⊢ Measurable f
have inhabit : ∀ (inhabited_h : Inhabited β), Measurable f
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f
have h : ∀ (x : β), f x = f default
Tactic: convert! @measurable_const α β _ _ (f default) using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
⊢ Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) ↔ MeasurableSet s
have mp : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) → MeasurableSet s
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
mp : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) → MeasurableSet s
⊢ Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) ↔ MeasurableSet s
have mpr : MeasurableSet s → Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
⊢ MeasurableSet s
have h₁ : s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
Tactic: convert! h (MeasurableSet.singleton (0 : β)).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
⊢ s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
have h₁ : ∀ (a : α), a ∈ s ↔ a ∈ preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
Tactic: ext a
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (g ⁻¹' t)
have this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
Tactic: have : g ⁻¹' t = g ⁻¹' t ∩ { x | f x = g x }ᶜ ∪ g ⁻¹' t ∩ { x | f x = g x } := by
    simp [← inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (g ⁻¹' t)
have rw : MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x})
have refine : MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x})
Tactic: refine (h.mono inter_subset_right).measurableSet.union ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
have h₁ : ∀ (x : α), x ∈ g ⁻¹' t ∩ {x : α | f x = g x} ↔ x ∈ f ⁻¹' t ∩ {x : α | f x = g x}
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x})
have this₁ : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
Tactic: have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } := by
    ext x
    simp +contextual
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this_1 : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
this : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x})
have rw : MeasurableSet (f ⁻¹' t ∩ {x : α | f x = g x})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
have rcases : ∀ (s : ℕ → Set α) (h1s : ∀ (n : ℕ), s n ∈ C) (h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ) (t : ℕ → Set β)
  (h1t : ∀ (n : ℕ), t n ∈ D) (h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ),
  IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
Tactic: rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
Cleared hypotheses: hC, hD
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
⊢ IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
have refine : Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
Tactic: refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
have rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n) = univ
Tactic: rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n) = univ
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
have rw₁ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), t n) = univ
Tactic: rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n) = univ
rw₁ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), t n) = univ
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
have rw₂ : SProd.sprod (α := Set α) (β := Set β) univ univ = univ
Tactic: rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n) = univ
rw₁ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), t n) = univ
rw₂ : SProd.sprod (α := Set α) (β := Set β) univ univ = univ
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
have rw₃ : Eq (α := Set (α × β)) univ univ
Tactic: rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ generateMeasurableRec s i
have unfold : s ⊆
  have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
  s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α)
Tactic: unfold generateMeasurableRec
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆
    have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α)
have h : s ⊆ s
Tactic: apply_rules [subset_union_of_subset_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∅ ∈ generateMeasurableRec s i
have unfold : Membership.mem (γ := Set (Set α))
  (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
  s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
  ∅
Tactic: unfold generateMeasurableRec
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ tᶜ ∈ generateMeasurableRec s i
have unfold : Membership.mem (γ := Set (Set α))
  (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
  s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
  tᶜ
Tactic: unfold generateMeasurableRec
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
⊢ ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
have unfold : Membership.mem (γ := Set (Set α))
  (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
  s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
  (⋃ (n : ℕ), f n)
Tactic: unfold generateMeasurableRec
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j
have inl : ∀ (h : i ≤ i), x ∈ generateMeasurableRec s i
Tactic: rcases h.eq_or_lt with (rfl | h)
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
inl : ∀ (h : i ≤ i), x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j
have inr : ∀ (h : i < j), x ∈ generateMeasurableRec s j
Tactic: rcases h.eq_or_lt with (rfl | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h_1 : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j
have h₁ : x = ⋃ (n : ℕ), x
Tactic: convert! iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
⊢ t ∈ generateMeasurableRec s i → p t
have suffices : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t
Tactic: suffices H : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t from H i le_rfl t
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k : Ordinal.{u_1}
⊢ k ≤ i → ∀ t ∈ generateMeasurableRec s k, p t
have apply : ∀ (x : Ordinal.{u_1}),
  (∀ y < x, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t) → x ≤ i → ∀ t ∈ generateMeasurableRec s x, p t
Tactic: apply WellFoundedLT.induction k
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
IH : ∀ y < k, y ≤ i → ∀ t ∈ generateMeasurableRec s y, p t
hk : k ≤ i
t : Set α
⊢ t ∈ generateMeasurableRec s k → p t
have IH₁ : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
Tactic: replace IH := fun j hj => IH j hj (hj.le.trans hk)
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
⊢ t ∈ generateMeasurableRec s k → p t
have unfold : Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    t →
  p t
Tactic: unfold generateMeasurableRec
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (hypothesis)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : Membership.mem (γ := Set (Set α)) (compl '' ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < k), generateMeasurableRec s j) t
⊢ p t
have ht₁ : ∃ (x : Set α), (∃ (i : Ordinal.{u_1}) (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t
Tactic: simp_rw [mem_image, mem_iUnion₂] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Card (goal)
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t_1 : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)
k_1 k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ (j : Ordinal.{u_1}) (hj : j < k), ∀ t ∈ generateMeasurableRec s j, p t
ht : ∃ (x : Set α), (∃ (i : Ordinal.{u_1}) (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t
⊢ p t
have inl : ∀ (u : Set α) (j : Ordinal.{u_1}) (hj : j < k) (hj' : u ∈ generateMeasurableRec s j), p uᶜ
Tactic: obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht
Cleared hypotheses: t, ht