awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
have h₂ : ∀ (b_1 : k < b), MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
Tactic: apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
b_1 : k < b
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
have h₂ : ∀ (b_2 : b ≤ N), MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ
Tactic: apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
Tactic: repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
Tactic: repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₄ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₅ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₆ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₇ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₈ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₉ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₀ : k ≠ 0 → MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₁₁ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₁₂ : ∀ (b : ℕ), k < b → MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
Tactic: repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₄ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₅ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₆ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₇ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₈ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₉ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₀ : k ≠ 0 → MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₁₁ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₂ : ∀ (b : ℕ), k < b → MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
have h₁₃ : ∀ (b : ℕ), k < b → b ≤ N → MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ
Tactic: repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.find (p := p x) ⋯
have refine : ∀ (x : α),
  MeasurableSet.{u_1} (α := α) (preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := p x) sorry) {Nat.find (p := p x) sorry})
Tactic: refine measurable_to_nat fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
x : α
⊢ MeasurableSet.{u_1} (α := α) (preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := p x) ⋯) {Nat.find (p := p x) ⋯})
have rw : MeasurableSet.{u_1} (α := α) (disjointed (fun (k : ℕ) ↦ {x : α | p x k}) (Nat.find (p := p x) sorry))
Tactic: rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
p : α → Prop
inst_1 : MeasurableSingletonClass α
x : Subtype p
⊢ Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' {(↑x : α)}) {x}
have rw : Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' image (α := Subtype p) (val (p := p)) {x}) {x}
Tactic: rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
p : α → Prop
inst_1 : MeasurableSingletonClass α
x : Subtype p
rw : Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' image (α := Subtype p) (val (p := p)) {x}) {x}
⊢ Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' {(↑x : α)}) {x}
have rw₁ : Eq (α := Set (Subtype p)) {x} {x}
Tactic: rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u))
have rw : MeasurableSet (s ∩ u)
Tactic: rw [Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set (↑s : Type u_1)
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion (s := s) (t := t) h '' u)
have rcases : ∀ (u : Set α) (hu : MeasurableSet u),
  MeasurableSet (inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: rcases hu with ⟨u, hu, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
have h₁ : inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u =
  Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s
Tactic: convert! (measurable_subtype_coe hu).inter hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s
have h₁ : ∀ (x : α) (hx : x ∈ t),
  Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈
      inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u ↔
    Membership.mem (γ := Set (↑t : Type u_1))
      (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
htu : MeasurableSet (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
⊢ MeasurableSet u
have h₁ : u =
  image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ∪
    image (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
Tactic: convert! (hs.subtype_image hsu).union (ht.subtype_image htu)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ y ∈ s
have h₁ : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), y ∈ i
Tactic: simp only [measurableAtom, mem_iInter] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
⊢ MeasurableSet (measurableAtom x)
have this : ∀ y ∉ measurableAtom x, ∃ (s : Set β), x ∈ s ∧ MeasurableSet s ∧ y ∉ s
Tactic: have : ∀ (y : β), y ∉ measurableAtom x → ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s :=
    fun y hy ↦ by simpa [measurableAtom] using hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
this : ∀ y ∉ measurableAtom x, ∃ (s : Set β), x ∈ s ∧ MeasurableSet s ∧ y ∉ s
⊢ MeasurableSet (measurableAtom x)
have choose! : ∀ (s : (y : β) → Set β) (hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y),
  MeasurableSet (measurableAtom x)
Tactic: choose! s hs using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
have h₁ : measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
h₁ : measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
have h₂ : ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
⊢ Membership.mem (γ := Set β) (⋂ y ∈ (measurableAtom x)ᶜ, s y) z
have h₁ : ∀ (i : β) (i_1 : i ∉ measurableAtom x), z ∈ s i
Tactic: simp only [mem_iInter, mem_compl_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x
have h₂ : (measurableAtom x)ᶜ ⊆ (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ
Tactic: apply compl_subset_compl.1
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ (measurableAtom x)ᶜ
⊢ Membership.mem (γ := Set β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ z
have h₂ : ∃ i ∉ measurableAtom x, z ∉ s i
Tactic: simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ MeasurableSet (measurableAtom x)
have this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
Tactic: have : measurableAtom x = ⋂ (y ∈ (measurableAtom x)ᶜ), s y := by
    apply Subset.antisymm
    · intro z hz
      simp only [mem_iInter, mem_compl_iff]
      intro i hi
      exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1
    · apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet (measurableAtom x)
have rw : MeasurableSet.{u_2} (α := β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
z : β
hz : z ∈ measurableAtom x
⊢ z ∈ measurableAtom y
have simp : ∀ (hz : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), z ∈ i)
  (hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i) (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i),
  z ∈ i
Tactic: simp only [measurableAtom, mem_iInter] at hz hx ⊢
Cleared hypotheses: hx, hz
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x = measurableAtom y
have refine : measurableAtom y ⊆ measurableAtom x
Tactic: refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom y ⊆ measurableAtom x
have pos : ∀ (hy : y ∈ measurableAtom x), measurableAtom y ⊆ measurableAtom x
Tactic: by_cases hy : y ∈ measurableAtom x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
pos : ∀ (hy : y ∈ measurableAtom x), measurableAtom y ⊆ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x
have neg : ∀ (hy : y ∉ measurableAtom x), measurableAtom y ⊆ measurableAtom x
Tactic: by_cases hy : y ∈ measurableAtom x
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
⊢ False
have hx₁ : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
Tactic: simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
hx₁ : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
⊢ False
have hy₁ : ∃ (x_1 : Set β) (_ : x ∈ x_1) (_ : MeasurableSet x_1), y ∉ x_1
Tactic: simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
hy : ∃ (x_1 : Set β) (_ : x ∈ x_1) (_ : MeasurableSet x_1), y ∉ x_1
⊢ False
have neg : ∀ (s : Set β) (hxs : x ∈ s) (hs : MeasurableSet s) (hys : y ∉ s), False
Tactic: obtain ⟨s, hxs, hs, hys⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ False
have hx₁ : x ∈ sᶜ
Tactic: specialize hx sᶜ hys hs.compl
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ Disjoint (measurableAtom x) (measurableAtom y)
have rw : measurableAtom x ∩ measurableAtom y = ∅
Tactic: rw [Set.disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
⊢ measurableAtom x ∩ measurableAtom y = ∅
have h : ∀ (z : β), z ∈ measurableAtom x ∩ measurableAtom y ↔ Membership.mem (γ := Set β) ∅ z
Tactic: ext z
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
⊢ z ∈ measurableAtom x ∩ measurableAtom y ↔ Membership.mem (γ := Set β) ∅ z
have h : z ∈ measurableAtom x → z ∉ measurableAtom y
Tactic: simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
⊢ False
have h1 : measurableAtom z = measurableAtom x
Tactic: have h1 := measurableAtom_eq_of_mem hzx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
⊢ False
have h2 : measurableAtom z = measurableAtom y
Tactic: have h2 := measurableAtom_eq_of_mem hzy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False
have hx₁ : x ∉ measurableAtom x
Tactic: rw [← h2, h1] at hx
Cleared hypotheses: hx, hzx, hzy, h1, h2
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m
have rw : mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
Tactic: rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m
have rw : mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
Tactic: rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
have rcases : ∀ (x : α) (y : β) (hx : (x, y).1 ∈ s) (hy : (x, y).2 ∈ t), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
Tactic: rcases h with ⟨⟨x, y⟩, hx, hy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
have refine : ∀ (hst : MeasurableSet (s ×ˢ t)), MeasurableSet s ∧ MeasurableSet t
Tactic: refine ⟨fun hst => ?_, fun h => h.1.prod h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
have this : MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t)
Tactic: have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prodMk_right hst
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
have this₁ : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
Tactic: have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prodMk_left hst
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
have inl : ∀ (h : s ×ˢ t = ∅), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
Tactic: rcases (s ×ˢ t).eq_empty_or_nonempty with h | h