awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
refine : MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
⊢ α ≃ᵐ β

Tactic:
refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))

Premises used: MeasurableEquiv.symm, MeasurableEquiv.trans, MeasurableEquiv.sumCompl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
apply : MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
⊢ MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))

Tactic:
apply MeasurableEquiv.sumCongr (hf.equivImage _)

Premises used: MeasurableEquiv.sumCongr, MeasurableEmbedding.equivImage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
a : Aᶜᶜ = (g '' Bᶜ)ᶜ
⊢ Aᶜ = g '' Bᶜ

Tactic:
apply compl_injective

Premises used: compl_injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
a : (F A)ᶜᶜ = (g '' Bᶜ)ᶜ
⊢ Aᶜᶜ = (g '' Bᶜ)ᶜ

Tactic:
rw [← Afp]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ (F A)ᶜᶜ = (g '' Bᶜ)ᶜ

Tactic:
simp [F, B]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ Aᶜ = g '' Bᶜ

Tactic:
have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
rw : MeasurableEquiv.{u_1, u_2} (↑(g '' Bᶜ) : Type u_1) (↑Bᶜ : Type u_2)
⊢ MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ MeasurableEquiv.{u_1, u_2} (↑(g '' Bᶜ) : Type u_1) (↑Bᶜ : Type u_2)

Tactic:
exact (hg.equivImage _).symm

Premises used: MeasurableEquiv.symm, MeasurableEmbedding.equivImage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)
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

Premises used: MeasurableEquiv.symm, MeasurableEquiv.sumCongr, MeasurableEmbedding.equivImage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)ᶜ)ᶜ
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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)
refine_2 : F (iInter X) = iInter X
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A

Tactic:
refine ⟨iInter X, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)

Tactic:
MeasurableSet.iInter fun n ↦ ?_

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 : ∀ (n : ℕ), MeasurableSet (F^[n] univ)
⊢ MeasurableSet (iInter X)

Tactic:
refine MeasurableSet.iInter fun n ↦ ?_

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[0] univ)

Tactic:
MeasurableSet.univ

Premises used: Nat.iterate, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[0] univ)

Tactic:
exact MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)
refine_1 : MeasurableSet (F (F^[n] univ))
⊢ MeasurableSet (F^[n + 1] univ)

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[n] univ))

Tactic:
(hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[n] univ))

Tactic:
exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)
refine_1₁ : ∀ (n : ℕ) (ih : MeasurableSet (F^[n] univ)), MeasurableSet (F^[n + 1] univ)
⊢ MeasurableSet (F^[n] 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

Premises used: Function.iterate_succ', Function.comp_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
refine_2₁ : iInter X ⊆ F (iInter X)
⊢ F (iInter X) = iInter X

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 : ∀ (i : ℕ), F (iInter X) ⊆ F^[i] univ
⊢ F (iInter X) ⊆ iInter X

Tactic:
apply subset_iInter

Premises used: Set.subset_iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
refine_2₁ : ∀ (n : ℕ), F (iInter X) ⊆ F^[n + 1] univ
⊢ F (iInter X) ⊆ F^[n] univ

Tactic:
cases n
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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) ⊆ F^[0] univ

Tactic:
subset_univ _

Premises used: Set.subset_univ, Nat.iterate
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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) ⊆ F^[0] univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[n] univ)
⊢ F (iInter X) ⊆ F^[n + 1] univ

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[n] univ)

Tactic:
Fmono (iInter_subset _ _)

Premises used: Set.iInter_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 (F^[n] univ)

Tactic:
exact Fmono (iInter_subset _ _)

Premises used: Set.iInter_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
⊢ ∀ (i : ℕ), g y ∈ F^[i] univ

Tactic:
rw [mem_iInter] at hx

Premises used: Set.mem_iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
refine_2 : y ∈ f '' iInter X
⊢ False

Tactic:
apply hy
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
refine_2 : Membership.mem (γ := Set β) (⋂ (i : ℕ), f '' F^[i] univ) y
⊢ y ∈ f '' iInter X

Tactic:
rw [hf.injective.injOn.image_iInter_eq]

Premises used: Function.Injective.injOn, Set.InjOn.image_iInter_eq, MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
refine_2 : ∀ (i : ℕ), y ∈ f '' F^[i] univ
⊢ Membership.mem (γ := Set β) (⋂ (i : ℕ), f '' F^[i] univ) y

Tactic:
rw [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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 : ℕ
⊢ g y ∈ F^[n.succ] univ

Tactic:
specialize hx n.succ

Premises used: Nat.succ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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
⊢ g y ∈ F (F^[n] univ)

Tactic:
rw [Function.iterate_succ', Function.comp_apply] at hx

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
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)
refine_2 : ∀ (h : y ∉ f '' F^[n] univ), False
⊢ y ∈ f '' F^[n] univ

Tactic:
by_contra h