awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ_1
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst_5 : MeasurableSpace α
inst_6 : MeasurableSpace β
dsimp : Measurable (β := (γ → α) × (γ → β)) fun (f : (i : γ) → α × β) ↦ (fun (c : γ) ↦ (f c).1, fun (c : γ) ↦ (f c).2)
⊢ Measurable (α := γ → α × β) (β := (γ → α) × (γ → β))
    (⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) : (a : γ → α × β) → (γ → α) × (γ → β))

Tactic:
dsimp [Equiv.arrowProdEquivProdArrow]

Premises used: Equiv.arrowProdEquivProdArrow
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ_1
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst_5 : MeasurableSpace α
inst_6 : MeasurableSpace β
⊢ Measurable (β := (γ → α) × (γ → β)) fun (f : (i : γ) → α × β) ↦ (fun (c : γ) ↦ (f c).1, fun (c : γ) ↦ (f c).2)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ_1
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst_5 : MeasurableSpace α
inst_6 : MeasurableSpace β
dsimp : Measurable (β := γ → α × β) fun (p : ((i : γ) → α) × ((i : γ) → β)) (c : γ) ↦ (p.1 c, p.2 c)
⊢ Measurable (α := (γ → α) × (γ → β)) (β := γ → α × β)
    (⇑(Equiv.symm (Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β)) :
      (a : (γ → α) × (γ → β)) → γ → α × β)

Tactic:
dsimp [Equiv.arrowProdEquivProdArrow]

Premises used: Equiv.arrowProdEquivProdArrow
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ_1
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst_5 : MeasurableSpace α
inst_6 : MeasurableSpace β
⊢ Measurable (β := γ → α × β) fun (p : ((i : γ) → α) × ((i : γ) → β)) (c : γ) ↦ (p.1 c, p.2 c)

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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst_5 : MeasurableSpace β₁
inst_6 : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x : Set (α₂ → β₂)
h : MeasurableSet x
⊢ MeasurableSet (α := α₁ → β₁) ((⇑(hα.arrowCongr' (↑hβ : β₁ ≃ β₂)) : (a : α₁ → β₁) → α₂ → β₂) ⁻¹' x)

Tactic:
MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.measurable.comp (measurable_pi_apply _)

Premises used: Iff.mpr, MeasurableSet.preimage, measurable_pi_iff, Measurable.comp, measurable_pi_apply, MeasurableEquiv.measurable, Equiv.symm, DFunLike.coe
-- 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 γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst_5 : MeasurableSpace β₁
inst_6 : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x : Set (α₂ → β₂)
h : MeasurableSet x
⊢ MeasurableSet (α := α₁ → β₁) ((⇑(hα.arrowCongr' (↑hβ : β₁ ≃ β₂)) : (a : α₁ → β₁) → α₂ → β₂) ⁻¹' x)

Tactic:
exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.measurable.comp (measurable_pi_apply _)

Premises used: Iff.mpr, MeasurableSet.preimage, measurable_pi_iff, Measurable.comp, MeasurableEquiv.measurable
-- 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 γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst_5 : MeasurableSpace β₁
inst_6 : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x : Set (α₁ → β₁)
h : MeasurableSet x
⊢ MeasurableSet (α := α₂ → β₂) ((⇑(hα.arrowCongr' (↑hβ : β₁ ≃ β₂)).symm : (a : α₂ → β₂) → α₁ → β₁) ⁻¹' x)

Tactic:
MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.symm.measurable.comp (measurable_pi_apply _)

Premises used: Iff.mpr, MeasurableSet.preimage, measurable_pi_iff, Measurable.comp, MeasurableEquiv.symm, measurable_pi_apply, MeasurableEquiv.measurable, DFunLike.coe
-- 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 γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst_5 : MeasurableSpace β₁
inst_6 : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x : Set (α₁ → β₁)
h : MeasurableSet x
⊢ MeasurableSet (α := α₂ → β₂) ((⇑(hα.arrowCongr' (↑hβ : β₁ ≃ β₂)).symm : (a : α₂ → β₂) → α₁ → β₁) ⁻¹' x)

Tactic:
exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.symm.measurable.comp (measurable_pi_apply _)

Premises used: Iff.mpr, MeasurableSet.preimage, measurable_pi_iff, Measurable.comp, MeasurableEquiv.symm, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
n : ℕ
α : Fin (n + 1) → Type u_8
inst_5 : (i : Fin (n + 1)) → MeasurableSpace (α i)
i : Fin (n + 1)
⊢ Measurable (β := α i) fun (x : α i × ((j : Fin n) → α (i.succAbove j))) ↦
    ((Fin.insertNthEquiv α i).symm.symm : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) x i

Tactic:
simp [measurable_fst]

Premises used: measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
n : ℕ
α : Fin (n + 1) → Type u_8
inst_5 : (i : Fin (n + 1)) → MeasurableSpace (α i)
i : Fin (n + 1)
j : Fin n
⊢ Measurable (β := α (i.succAbove j)) fun (x : α i × ((j : Fin n) → α (i.succAbove j))) ↦
    ((Fin.insertNthEquiv α i).symm.symm : (a : α i × ((j : Fin n) → α (i.succAbove j))) → (j : Fin (n + 1)) → α j) x
      (i.succAbove j)

Tactic:
simpa using (measurable_pi_apply _).comp measurable_snd

Premises used: Measurable.comp, measurable_pi_apply, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
eta_expand :
  Measurable (β := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) fun (a : (i : δ ⊕ δ') → α i) ↦
    (Equiv.sumPiEquivProdPi fun (a : δ ⊕ δ') ↦ α a :
        (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
      fun (i : δ ⊕ δ') ↦ a i
⊢ Measurable (α := (i : δ ⊕ δ') → α i) (β := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
    (⇑(Equiv.sumPiEquivProdPi α) : (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))

Tactic:
eta_expand
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
dsimp :
  Measurable (β := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) fun (a : (i : δ ⊕ δ') → α i) ↦
    (fun (i : δ) ↦ a (Sum.inl i), fun (i' : δ') ↦ a (Sum.inr i'))
⊢ Measurable (β := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) fun (a : (i : δ ⊕ δ') → α i) ↦
    (Equiv.sumPiEquivProdPi fun (a : δ ⊕ δ') ↦ α a :
        (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
      fun (i : δ ⊕ δ') ↦ a i

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable (β := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) fun (a : (i : δ ⊕ δ') → α i) ↦
    (fun (i : δ) ↦ a (Sum.inl i), fun (i' : δ') ↦ a (Sum.inr i'))

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
rw :
  ∀ (a : δ ⊕ δ'),
    Measurable (β := α a) fun (x : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) ↦
      ((Equiv.sumPiEquivProdPi α).symm :
          (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
        x a
⊢ Measurable (α := ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) (β := (i : δ ⊕ δ') → α i)
    (⇑(Equiv.sumPiEquivProdPi α).symm :
      (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
i : δ
⊢ Measurable (β := α (Sum.inl i)) fun (x : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) ↦
    ((Equiv.sumPiEquivProdPi α).symm :
        (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
      x (Sum.inl i)

Tactic:
measurable_pi_iff.1 measurable_fst _

Premises used: measurable_pi_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
i : δ
⊢ Measurable (β := α (Sum.inl i)) fun (x : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) ↦
    ((Equiv.sumPiEquivProdPi α).symm :
        (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
      x (Sum.inl i)

Tactic:
exact measurable_pi_iff.1 measurable_fst _

Premises used: measurable_pi_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
i : δ'
⊢ Measurable (β := α (Sum.inr i)) fun (x : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) ↦
    ((Equiv.sumPiEquivProdPi α).symm :
        (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
      x (Sum.inr i)

Tactic:
measurable_pi_iff.1 measurable_snd _

Premises used: measurable_pi_iff, measurable_snd, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α_1
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst_3 : (x : δ') → MeasurableSpace (π x)
inst_4 : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst_5 : (i : δ ⊕ δ') → MeasurableSpace (α i)
i : δ'
⊢ Measurable (β := α (Sum.inr i)) fun (x : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) ↦
    ((Equiv.sumPiEquivProdPi α).symm :
        (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
      x (Sum.inr i)

Tactic:
exact measurable_pi_iff.1 measurable_snd _

Premises used: measurable_pi_iff, measurable_snd, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Eq (α := (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
    (⇑(sumPiEquivProdPi α) : (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
    (⇑(Equiv.sumPiEquivProdPi α) : (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Eq (α := (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
    (⇑(symm (sumPiEquivProdPi α)) : (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
    (⇑(Equiv.sumPiEquivProdPi α).symm :
      (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
hf : Involutive f
hf' : Measurable f
a : α
⊢ (ofInvolutive f hf hf' : (a : α) → α) a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
hf : Involutive f
hf' : Measurable f
⊢ (ofInvolutive f hf hf').symm = ofInvolutive f hf hf'

Tactic:
rfl

Premises used: MeasurableEquiv.ofInvolutive, MeasurableEquiv.symm, Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_8
⊢ Eq.{u_8 + 1} (α := (a : α → Prop) → Set α) (⇑MeasurableEquiv.setOf : (a : α → Prop) → Set α) setOf

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSpace.comap f inst_1 = inst

Tactic:
hf.measurable.comap_le.antisymm fun _s h ↦
    ⟨_, hf.measurableSet_image' h, hf.injective.preimage_image _⟩

Premises used: Measurable.comap_le, MeasurableEmbedding.measurableSet_image', LE.le.antisymm, MeasurableEmbedding.injective, Function.Injective.preimage_image, And.intro, Exists.intro, Set.image, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (range f)
rw : Measurable f
⊢ Measurable f

Tactic:
rw [← hf.2.1]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (range f)
⊢ Measurable f

Tactic:
comap_measurable f

Premises used: comap_measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (range f)
⊢ Measurable f

Tactic:
exact comap_measurable f

Premises used: comap_measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (range f)
rw : ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
rw [← hf.2.1]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst_1 = inst ∧ MeasurableSet (range f)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f '' f ⁻¹' s)

Tactic:
simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2

Premises used: Set.image_preimage_eq_inter_range, And.right, MeasurableSet.inter
-- 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_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α → β
g : β → α
s : Set α
hf : MeasurableEmbedding f
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet.{u_2} (α := (↑(f '' s) : Type u_2))
    (preimage (β := (↑s : Type u_1)) (⇑(Equiv.Set.image f s ⋯).symm : (a : (↑(f '' s) : Type u_2)) → (↑s : Type u_1))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u))

Tactic:
simpa [preimage_preimage, Set.image_symm_preimage hf.injective]
      using measurable_subtype_coe (hf.measurableSet_image' hu)

Premises used: measurable_subtype_coe, Set.preimage_preimage, MeasurableEmbedding.measurableSet_image', Equiv.Set.image_symm_preimage, 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 : α → β
g : β → α
hf : MeasurableEmbedding f
rw rw₁ : (↑(range f) : Type u_2) = (↑(range f) : Type u_2)
⊢ (↑(f '' univ) : Type u_2) = (↑(range f) : Type u_2)

Tactic:
rw [image_univ]

Premises used: Set.image_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 : α → β
g : β → α
hf : MeasurableEmbedding f
rw rw₁ :
  HEq.{u_2 + 1} (α := MeasurableSpace (↑(range f) : Type u_2))
    (Subtype.instMeasurableSpace (p := fun (x : β) ↦ x ∈ range f)) (β := MeasurableSpace (↑(range f) : Type u_2))
    (Subtype.instMeasurableSpace (p := fun (x : β) ↦ x ∈ range f))
⊢ HEq.{u_2 + 1} (α := MeasurableSpace (↑(f '' univ) : Type u_2))
    (Subtype.instMeasurableSpace (p := fun (x : β) ↦ x ∈ f '' univ)) (β := MeasurableSpace (↑(range f) : Type u_2))
    (Subtype.instMeasurableSpace (p := fun (x : β) ↦ x ∈ range f))

Tactic:
rw [image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
g : (↑(range f) : Type u_2) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : MeasurableEquiv.{u_1, u_2} α (↑(range f) : Type u_2) :=
  { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯,
    measurable_invFun := hg }
⊢ MeasurableEmbedding f

Tactic:
(MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.comp, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
g : (↑(range f) : Type u_2) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : MeasurableEquiv.{u_1, u_2} α (↑(range f) : Type u_2) :=
  { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯,
    measurable_invFun := hg }
⊢ MeasurableEmbedding f

Tactic:
exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.comp, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
g : β → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g f
⊢ MeasurableEmbedding f

Tactic:
of_measurable_inverse_on_range hf₁ hf₂ (hg.comp measurable_subtype_coe) H

Premises used: measurable_subtype_coe, Measurable.comp, MeasurableEmbedding.of_measurable_inverse_on_range
-- 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 : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
⊢ α ≃ᵐ β

Tactic:
rcases this with ⟨A, Ameas, 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
⊢ MeasurableSet B

Tactic:
have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas