awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
rcases rcases₁ : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
rcases₂ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → α ≃ᵐ β
rcases₃ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) →
          MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
rcases₄ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
rcases₅ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → (this : Aᶜ = g '' Bᶜ) → MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
⊢ α ≃ᵐ β
have rcases₆ : (A : Set α) →
  (Ameas : MeasurableSet A) →
    (Afp : F A = A) →
      let B := f '' A;
      (Bmeas : MeasurableSet B) →
        (this : Aᶜ = g '' Bᶜ) → MeasurableEquiv.{u_1, u_2} (↑(g '' Bᶜ) : Type u_1) (↑Bᶜ : Type u_2)
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
⊢ α ≃ᵐ β
have suffices : (A : Set α) ×' MeasurableSet A ∧ F A = A
Tactic: suffices Σ' A : Set α, MeasurableSet A ∧ F A = A by
    classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
have Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
Tactic: have Fmono : ∀ {A B}, A ⊆ B → F A ⊆ F B := fun h =>
    compl_subset_compl.mpr <| Set.image_mono <| compl_subset_compl.mpr <| Set.image_mono h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
have refine_1 : MeasurableSet (iInter X)
Tactic: refine ⟨iInter X, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
refine_1 : MeasurableSet (iInter X)
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
have refine_2 : F (iInter X) = iInter X
Tactic: refine ⟨iInter X, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
⊢ MeasurableSet (iInter X)
have refine_1 : ∀ (n : ℕ), MeasurableSet (F^[n] univ)
Tactic: refine MeasurableSet.iInter fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F^[n + 1] univ)
have refine_1 : MeasurableSet (F (F^[n] univ))
Tactic: rw [Function.iterate_succ', Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
⊢ MeasurableSet (F^[n] univ)
have refine_1 : MeasurableSet (F^[0] univ)
Tactic: induction n with
    | zero => exact MeasurableSet.univ
    | succ n ih =>
      rw [Function.iterate_succ', Function.comp_apply]
      exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
refine_1 : MeasurableSet (F^[0] univ)
⊢ MeasurableSet (F^[n] univ)
have refine_1₁ : ∀ (n : ℕ) (ih : MeasurableSet (F^[n] univ)), MeasurableSet (F^[n + 1] univ)
Tactic: induction n with
    | zero => exact MeasurableSet.univ
    | succ n ih =>
      rw [Function.iterate_succ', Function.comp_apply]
      exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
⊢ F (iInter X) = iInter X
have refine_2 : F (iInter X) ⊆ iInter X
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
refine_2 : F (iInter X) ⊆ iInter X
⊢ F (iInter X) = iInter X
have refine_2₁ : iInter X ⊆ F (iInter X)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
⊢ F (iInter X) ⊆ iInter X
have refine_2 : ∀ (i : ℕ), F (iInter X) ⊆ F^[i] univ
Tactic: apply subset_iInter
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
⊢ F (iInter X) ⊆ F^[n] univ
have refine_2 : F (iInter X) ⊆ F^[0] univ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
refine_2 : F (iInter X) ⊆ F^[0] univ
⊢ F (iInter X) ⊆ F^[n] univ
have refine_2₁ : ∀ (n : ℕ), F (iInter X) ⊆ F^[n + 1] univ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
n : ℕ
⊢ F (iInter X) ⊆ F^[n + 1] univ
have refine_2 : F (iInter X) ⊆ F (F^[n] univ)
Tactic: rw [Function.iterate_succ', Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : g y ∈ iInter X
⊢ False
have hx₁ : ∀ (i : ℕ), g y ∈ F^[i] univ
Tactic: rw [mem_iInter] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ False
have refine_2 : y ∈ f '' iInter X
Tactic: apply hy
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ f '' iInter X
have refine_2 : Membership.mem (γ := Set β) (⋂ (i : ℕ), f '' F^[i] univ) y
Tactic: rw [hf.injective.injOn.image_iInter_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ Membership.mem (γ := Set β) (⋂ (i : ℕ), f '' F^[i] univ) y
have refine_2 : ∀ (i : ℕ), y ∈ f '' F^[i] univ
Tactic: rw [mem_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
n : ℕ
⊢ y ∈ f '' F^[n] univ
have hx₁ : g y ∈ F^[n.succ] univ
Tactic: specialize hx n.succ
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F^[n.succ] univ
⊢ y ∈ f '' F^[n] univ
have hx₁ : g y ∈ F (F^[n] univ)
Tactic: rw [Function.iterate_succ', Function.comp_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
⊢ y ∈ f '' F^[n] univ
have refine_2 : ∀ (h : y ∉ f '' F^[n] univ), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun (n : ℕ) ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
h : y ∉ f '' F^[n] univ
⊢ False
have refine_2 : g y ∈ g '' (f '' F^[n] univ)ᶜ
Tactic: apply hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ (hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) = x
have nth_rw : Eq.{u_1 + 1} (α := α)
  ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry) : α)
  ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α)
      ((hf.equivRange : (a : α) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2)) :
    α)
Tactic: nth_rw 3 [← hf.equivRange.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ Eq.{u_1 + 1} (α := α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) : α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α)
        ((hf.equivRange : (a : α) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2)) :
      α)
have rw : Eq.{u_1 + 1} (α := α)
  ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry) : α)
  ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry) : α)
Tactic: rw [hf.equivRange_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
⊢ MeasurableSpace.comap.{u_1, u_2} (β := β) (fun (a : α) ↦ (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance
have rw : MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
Tactic: rw [← Function.comp_def, ← MeasurableSpace.comap_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
have e_m : Eq.{u_2 + 1} (α := MeasurableSpace β) (MeasurableSpace.comap compl inferInstance) inferInstance
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s_1 t : Set α
l : Filter α
inst : CountableInterFilter l
s : ℕ → Set α
hs : ∀ (i : ℕ), ∃ (t : Set α), MeasurableSet t ∧ s i =ᶠ[l] t
⊢ ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t
have choose : ∀ (t : (i : ℕ) → Set α) (ht : ∀ (i : ℕ), MeasurableSet (t i)) (hts : ∀ (i : ℕ), s i =ᶠ[l] t i),
  ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t
Tactic: choose t ht hts using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
⊢ EventuallyMeasurableSet m l s
have rcases : ∀ (t' : Set α) (ht' : MeasurableSet t') (htt' : t =ᶠ[l] t'), EventuallyMeasurableSet m l s
Tactic: rcases ht with ⟨t', ht', htt'⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Instances (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
⊢ MeasurableSingletonClass α
have refine : ∀ (i : α), MeasurableSet (α := α) {i}
Tactic: refine ⟨fun i => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Instances (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ MeasurableSet (α := α) {i}
have h : Eq (α := Set α) {i} Set.univ
Tactic: convert! MeasurableSet.univ
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ f ∘ g ⁻¹' s = s
have rw : g ⁻¹' f ⁻¹' s = s
Tactic: rw [preimage_comp, hs.1.2, hs.2.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
rw : g ⁻¹' f ⁻¹' s = s
⊢ f ∘ g ⁻¹' s = s
have rw₁ : g ⁻¹' s = s
Tactic: rw [preimage_comp, hs.1.2, hs.2.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
rw : g ⁻¹' f ⁻¹' s = s
rw₁ : g ⁻¹' s = s
⊢ f ∘ g ⁻¹' s = s
have rw₂ : s = s
Tactic: rw [preimage_comp, hs.1.2, hs.2.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
n : ℕ
⊢ invariants f ≤ invariants f^[n]
have zero : invariants f ≤ invariants f^[0]
Tactic: induction n with
  | zero => simp [invariants_le]
  | succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
n : ℕ
zero : invariants f ≤ invariants f^[0]
⊢ invariants f ≤ invariants f^[n]
have succ : ∀ (n : ℕ) (ihn : invariants f ≤ invariants f^[n]), invariants f ≤ invariants f^[n + 1]
Tactic: induction n with
  | zero => simp [invariants_le]
  | succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
⊢ Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s
have simp : (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
  ∀ (x : Set β) (x_1 : MeasurableSet x), MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x
Tactic: simp only [Measurable, ← forall_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw : g ∘ fa ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Invariants (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
rw : g ∘ fa ⁻¹' s = g ⁻¹' s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s
have rw₁ : fb ∘ g ⁻¹' s = g ⁻¹' s
Tactic: rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]