awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Measurable (_root_.id ∘ f)), Measurable f
⊢ Measurable f

Tactic:
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Premises used: Function.RightInverse.comp_eq_id, Set.rightInverse_rangeSplitting, MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
suffices : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ Measurable f

Tactic:
suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)

Tactic:
hg.measurable_rangeSplitting.comp H.subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasurableEmbedding.measurable_rangeSplitting, Classical.choose, Set.rangeSplitting
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)

Tactic:
exact hg.measurable_rangeSplitting.comp H.subtype_mk

Premises used: Measurable.comp, Measurable.subtype_mk, MeasurableEmbedding.measurable_rangeSplitting
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ MeasurableSet (i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s)

Tactic:
(hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
h₁ : s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s
⊢ MeasurableSet s

Tactic:
convert! (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

Premises used: Set.univ_subset_iff, Set.image_preimage_eq_range_inter, Iff.mp, Set.union_inter_distrib_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ MeasurableSet (i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s ∪ i₃ '' i₃ ⁻¹' s)

Tactic:
(hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union
      (hi₃.measurableSet_image' hs₃)

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
h₁ : s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s ∪ i₃ '' i₃ ⁻¹' s
⊢ MeasurableSet s

Tactic:
convert!
    (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union
      (hi₃.measurableSet_image' hs₃)

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s ∪ i₃ '' i₃ ⁻¹' s

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

Premises used: Set.univ_subset_iff, Set.image_preimage_eq_range_inter, Iff.mp, Set.union_inter_distrib_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
f : α → β
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hf₁ : Measurable (f ∘ i₁)
hf₂ : Measurable (f ∘ i₂)
⊢ Measurable f

Tactic:
fun _s hs ↦ .of_union_range_cover hi₁ hi₂ h (hf₁ hs) (hf₂ hs)

Premises used: Measurable, MeasurableSet.of_union_range_cover
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mβ : MeasurableSpace β
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
f : α → β
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hf₁ : Measurable (f ∘ i₁)
hf₂ : Measurable (f ∘ i₂)
hf₃ : Measurable (f ∘ i₃)
⊢ Measurable f

Tactic:
fun _s hs ↦ .of_union₃_range_cover hi₁ hi₂ hi₃ h (hf₁ hs) (hf₂ hs) (hf₃ hs)

Premises used: Measurable, MeasurableSet.of_union₃_range_cover
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
s : Set α
x : MeasurableSpace α
hs : MeasurableSet s
hne : s.Nonempty
⊢ ∃ (f : α → (↑s : Type u_1)), Measurable f ∧ ∀ (x : (↑s : Type u_1)), f (↑x : α) = x

Tactic:
let ⟨f, hfm, hf⟩ :=
    (MeasurableEmbedding.subtype_coe hs).exists_measurable_extend measurable_id fun _ =>
      hne.to_subtype
  ⟨f, hfm, congr_fun hf⟩

Premises used: measurable_id, Measurable, Set.Nonempty.to_subtype, Exists, MeasurableEmbedding.exists_measurable_extend, And, _private.0.MeasurableSet.exists_measurable_proj.match_1, And.intro, Exists.intro, congr_fun, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e₁ : α ≃ β
measurable_toFun : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e₁ : (a : α) → β)
measurable_invFun : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e₁.symm : (a : β) → α)
measurable_toFun_1 : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e₁ : (a : α) → β)
measurable_invFun_1 : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e₁.symm : (a : β) → α)
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun, measurable_invFun := measurable_invFun : α ≃ᵐ β } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun_1, measurable_invFun := measurable_invFun_1 }

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Eq (α := (a : α) → β) (⇑e.toEquiv : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.measurable_toFun

Premises used: MeasurableEquiv.measurable_toFun
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ β
h1 : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)
h2 : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ Eq (α := (a : α) → β) (⇑{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 : α ≃ᵐ β } : (a : α) → β)
    (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
ab : α ≃ᵐ β
bc : β ≃ᵐ γ
⊢ Eq (α := (a : α) → γ) (⇑(ab.trans bc) : (a : α) → γ)
    (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑bc : (a : β) → γ) (⇑ab : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Eq (α := (a : β) → α) (⇑e.symm : (a : β) → α) (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e₁ e₂ : α ≃ᵐ β
h : Eq (α := (a : α) → β) (⇑e₁ : (a : α) → β) (⇑e₂ : (a : α) → β)
⊢ e₁ = e₂

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ β
h1 : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)
h2 : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 : α ≃ᵐ β }.symm =
    { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }

Tactic:
rfl

Premises used: MeasurableEquiv.symm, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: MeasurableEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Bijective (α := α ≃ᵐ β) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: MeasurableEquiv.symm_symm, Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_6
inst : MeasurableSpace α
⊢ Eq (α := α ≃ᵐ α) (symm (refl α)) (refl α)

Tactic:
rfl

Premises used: MeasurableEquiv.symm, MeasurableEquiv.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Eq.{u_1 + 1} (α := α → α) (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) id

Tactic:
funext e.left_inv

Premises used: MeasurableEquiv.toEquiv, funext, Equiv.left_inv
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Eq.{u_2 + 1} (α := β → β) (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) id

Tactic:
funext e.right_inv

Premises used: MeasurableEquiv.toEquiv, Equiv.right_inv, funext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
y : β
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) y : α) = y

Tactic:
e.right_inv y

Premises used: MeasurableEquiv.toEquiv, Equiv.right_inv
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
x : α
⊢ (e.symm : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
e.left_inv x

Premises used: MeasurableEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ e.symm.trans e = refl β

Tactic:
ext e.self_comp_symm

Premises used: MeasurableEquiv.self_comp_symm, MeasurableEquiv.ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ e.trans e.symm = refl α

Tactic:
ext e.symm_comp_self

Premises used: MeasurableEquiv.ext, MeasurableEquiv.symm_comp_self
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
e₁ : α ≃ᵐ β
e₂ : β ≃ᵐ γ
⊢ (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Tactic:
rfl

Premises used: Equiv.trans, MeasurableEquiv.symm, MeasurableEquiv.trans, Equiv.symm, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.surjective

Premises used: MeasurableEquiv.toEquiv, Equiv.surjective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Bijective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.bijective

Premises used: MeasurableEquiv.toEquiv, Equiv.bijective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.injective

Premises used: MeasurableEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ preimage.{u_2, u_1} (β := α) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
e.toEquiv.symm_preimage_preimage s

Premises used: MeasurableEquiv.toEquiv, Equiv.symm_preimage_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' s) ((⇑e.symm : (a : β) → α) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm s

Premises used: MeasurableEquiv.toEquiv, Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e.symm : (a : β) → α) ⁻¹' s) ((⇑e : (a : α) → β) '' s)

Tactic:
(image_eq_preimage_symm ..).symm

Premises used: MeasurableEquiv.image_eq_preimage_symm, Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e.symm : (a : β) → α) '' s) ((⇑e : (a : α) → β) ⁻¹' s)

Tactic:
image_symm_eq_preimage ..

Premises used: Equiv.image_symm_eq_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
rw : s = (⇑e.toEquiv : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t
rw₁ : (⇑e.symm : (a : β) → α) '' s = t ↔ (⇑e.symm : (a : β) → α) '' s = t
rw₂ rw₃ : (⇑e.symm : (a : β) → α) '' s = t ↔ (⇑e.symm : (a : β) → α) '' s = t
⊢ s = (⇑e : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t

Tactic:
rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]

Premises used: MeasurableEquiv.coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, MeasurableEquiv.coe_toEquiv_symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
rw : Set.image.{u_1, u_2} (α := α) (⇑e.toEquiv : (a : α) → β) ((⇑e.toEquiv : (a : α) → β) ⁻¹' s) = s
rw₁ rw₂ : s = s
⊢ Set.image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
rw [← coe_toEquiv, Equiv.image_preimage]

Premises used: MeasurableEquiv.coe_toEquiv, Equiv.image_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
rw : preimage.{u_1, u_2} (β := β) (⇑e.toEquiv : (a : α) → β) ((⇑e.toEquiv : (a : α) → β) '' s) = s
rw₁ rw₂ : s = s
⊢ preimage.{u_1, u_2} (β := β) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) '' s) = s

Tactic:
rw [← coe_toEquiv, Equiv.preimage_image]

Premises used: MeasurableEquiv.coe_toEquiv, Equiv.preimage_image
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
h : MeasurableSet.{u_1} (α := α) ((⇑e : (a : α) → β) ⁻¹' s)
⊢ MeasurableSet s

Tactic:
simpa only [symm_preimage_preimage] using e.symm.measurable h

Premises used: MeasurableEquiv.symm_preimage_preimage, MeasurableEquiv.symm, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
rw : MeasurableSet.{u_2} (α := β) ((⇑e.symm : (a : β) → α) ⁻¹' s) ↔ MeasurableSet s
rw₁ rw₂ : MeasurableSet s ↔ MeasurableSet s
⊢ MeasurableSet.{u_2} (α := β) ((⇑e : (a : α) → β) '' s) ↔ MeasurableSet s

Tactic:
rw [image_eq_preimage_symm, measurableSet_preimage]

Premises used: MeasurableEquiv.image_eq_preimage_symm, MeasurableEquiv.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSpace.map (⇑e : (a : α) → β) inst = inst_1

Tactic:
e.measurable.le_map.antisymm' fun _s ↦ e.measurableSet_preimage.1

Premises used: LE.le.antisymm', Measurable.le_map, Iff.mp, MeasurableEquiv.measurableSet_preimage, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable.{u_1, u_3} (α := α) (f ∘ (⇑e : (a : α) → β))
⊢ Measurable (α := β) (f ∘ (⇑(e.symm.trans e).toEquiv : (a : β) → β))

Tactic:
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable.{u_1, u_3} (α := α) (f ∘ (⇑e : (a : α) → β))
this : Measurable (α := β) (f ∘ (⇑(e.symm.trans e).toEquiv : (a : β) → β))
rwa : ∀ (this : Measurable (α := β) (f ∘ (⇑(e.symm.trans e) : (a : β) → β))), Measurable f
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Measurable (α := β) (f ∘ (⇑(refl β) : (a : β) → β))), Measurable f
⊢ Measurable f

Tactic:
rwa [coe_toEquiv, symm_trans_self] at this

Premises used: MeasurableEquiv.coe_toEquiv, MeasurableEquiv.symm_trans_self
-- 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 γ
⊢ Measurable (β := α × β × γ) fun (a : (α × β) × γ) ↦ (a.1.1, a.1.2, a.2)

Tactic:
measurability
-- 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 γ
⊢ Measurable (β := (α × β) × γ) fun (a : α × β × γ) ↦ ((a.1, a.2.1), a.2.2)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_1 t_1 u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable (β := { a : α // (fun (x : α) ↦ x ∈ s) a }) fun (a : (↑(s ×ˢ t) : Type (max u_1 u_2))) ↦
    Subtype.mk (p := fun (a : α) ↦ (fun (x : α) ↦ x ∈ s) a) (↑a : α × β).1 ⋯

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_1 t_1 u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable (β := { b : β // (fun (x : β) ↦ x ∈ t) b }) fun (a : (↑(s ×ˢ t) : Type (max u_1 u_2))) ↦
    Subtype.mk (p := fun (b : β) ↦ (fun (x : β) ↦ x ∈ t) b) (↑a : α × β).2 ⋯

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_1 t_1 u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
t : Set β
⊢ Measurable (β := α × β) fun (x : Prod.{u_1, u_2} (↑s : Type u_1) (↑t : Type u_2)) ↦ ((↑x.1 : α), (↑x.2 : β))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_1 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (α := (↑(range Sum.inl) : Type (max u_1 u_2)))
    ((⇑(Equiv.Set.rangeInl α β) : (a : (↑(range Sum.inl) : Type (max u_1 u_2))) → α) ⁻¹' s)

Tactic:
⟨_, hs.inl_image, Set.ext ?_⟩

Premises used: Set.ext, MeasurableSet, MeasurableSet.inl_image, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_1 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
hs : MeasurableSet s
refine :
  ∀ (x : { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) x }),
    Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) x })
        (Subtype.val (p := fun (x : α ⊕ β) ↦ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) x) ⁻¹' Sum.inl '' s) x ↔
      Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) x })
        ((⇑(Equiv.Set.rangeInl α β) : (a : (↑(range Sum.inl) : Type (max u_1 u_2))) → α) ⁻¹' s) x
⊢ MeasurableSet (α := (↑(range Sum.inl) : Type (max u_1 u_2)))
    ((⇑(Equiv.Set.rangeInl α β) : (a : (↑(range Sum.inl) : Type (max u_1 u_2))) → α) ⁻¹' s)

Tactic:
refine ⟨_, hs.inl_image, Set.ext ?_⟩