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_1 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
s : Set α
hs : MeasurableSet s
⊢ ∀ (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

Tactic:
simp
-- 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.inr) : Type (max u_1 u_2)))
    ((⇑(Equiv.Set.rangeInr α β) : (a : (↑(range Sum.inr) : Type (max u_1 u_2))) → β) ⁻¹' s)

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

Premises used: Set.ext, MeasurableSet, And.intro, Exists.intro, MeasurableSet.inr_image
-- 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.inr) x }),
    Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x })
        (Subtype.val (p := fun (x : α ⊕ β) ↦ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x) ⁻¹' Sum.inr '' s) x ↔
      Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x })
        ((⇑(Equiv.Set.rangeInr α β) : (a : (↑(range Sum.inr) : Type (max u_1 u_2))) → β) ⁻¹' s) x
⊢ MeasurableSet (α := (↑(range Sum.inr) : Type (max u_1 u_2)))
    ((⇑(Equiv.Set.rangeInr α β) : (a : (↑(range Sum.inr) : Type (max u_1 u_2))) → β) ⁻¹' s)

Tactic:
refine ⟨_, hs.inr_image, Set.ext ?_⟩
-- 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
⊢ ∀ (x : { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x }),
    Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x })
        (Subtype.val (p := fun (x : α ⊕ β) ↦ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x) ⁻¹' Sum.inr '' s) x ↔
      Membership.mem (γ := Set { x : α ⊕ β // Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x })
        ((⇑(Equiv.Set.rangeInr α β) : (a : (↑(range Sum.inr) : Type (max u_1 u_2))) → β) ⁻¹' s) x

Tactic:
simp
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
c : γ
a : α
⊢ Membership.mem (γ := Set ((α ⊕ β) × γ)) univ (Sum.inl a, c) →
    (Sum.inl a, c) ∈
      SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ ∪
        SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ

Tactic:
simp [Set.prod_eq]

Premises used: Set.prod_eq
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
c : γ
b : β
⊢ Membership.mem (γ := Set ((α ⊕ β) × γ)) univ (Sum.inr b, c) →
    (Sum.inr b, c) ∈
      SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ ∪
        SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ

Tactic:
simp [Set.prod_eq]

Premises used: Set.prod_eq
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
refine_1 :
  Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)
refine_2 :
  Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)
⊢ Measurable (α := (α ⊕ β) × γ) (β := α × γ ⊕ β × γ) (⇑(Equiv.sumProdDistrib α β γ) : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ)

Tactic:
refine
      measurable_of_measurable_union_cover (range Sum.inl ×ˢ (univ : Set γ))
        (range Sum.inr ×ˢ (univ : Set γ)) (measurableSet_range_inl.prod MeasurableSet.univ)
        (measurableSet_range_inr.prod MeasurableSet.univ)
        (by rintro ⟨a | b, c⟩ <;> simp [Set.prod_eq]) ?_ ?_

Premises used: SProd.sprod, Set.univ, measurableSet_range_inl, MeasurableSet.prod, Sum.inl, measurableSet_range_inr, Sum.inr, measurable_of_measurable_union_cover, Set.range, MeasurableSet.univ
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)

Tactic:
(Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_

Premises used: Set.Mem, Set.univ, MeasurableEquiv.symm, Sum.inl, MeasurableEquiv.Set.prod, MeasurableEquiv.measurable_comp_iff, Iff.mp, Set.range
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
refine_1 :
  Measurable (α := (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inl) univ)) :
        (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
⊢ Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)

Tactic:
refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_

Premises used: Set.univ, MeasurableEquiv.symm, Sum.inl, MeasurableEquiv.Set.prod, MeasurableEquiv.measurable_comp_iff, Iff.mp, Set.range
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inl) univ)) :
        (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))

Tactic:
(prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_

Premises used: Set.Mem, MeasurableEquiv.prodCongr, MeasurableEquiv.symm, MeasurableEquiv.Set.rangeInl, MeasurableEquiv.Set.univ, MeasurableEquiv.measurable_comp_iff, Iff.mp
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
refine_1 :
  Measurable (α := α × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inl) univ)) :
          (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInl (Set.univ γ))) :
        (a : α × γ) → (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8)))
⊢ Measurable (α := (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inl) univ)) :
        (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))

Tactic:
refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_

Premises used: MeasurableEquiv.prodCongr, MeasurableEquiv.symm, MeasurableEquiv.Set.rangeInl, MeasurableEquiv.Set.univ, MeasurableEquiv.measurable_comp_iff, Iff.mp
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := α × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inl) univ)) :
          (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInl (Set.univ γ))) :
        (a : α × γ) → (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8)))

Tactic:
measurable_inl

Premises used: measurable_inl, Sum.map, Sum.elim
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := α × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inl) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inl) univ)) :
          (a : (↑(range Sum.inl) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inl ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInl (Set.univ γ))) :
        (a : α × γ) → (↑(range Sum.inl) : Type (max u_6 u_7)) × (↑univ : Type u_8)))

Tactic:
exact measurable_inl

Premises used: measurable_inl
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)

Tactic:
(Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 ?_

Premises used: Set.Mem, Set.univ, MeasurableEquiv.symm, MeasurableEquiv.Set.prod, Sum.inr, MeasurableEquiv.measurable_comp_iff, Iff.mp, Set.range
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
refine_2 :
  Measurable (α := (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inr) univ)) :
        (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
⊢ Measurable (β := α × γ ⊕ β × γ)
    fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)

Tactic:
refine (Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 ?_

Premises used: Set.univ, MeasurableEquiv.symm, MeasurableEquiv.Set.prod, Sum.inr, MeasurableEquiv.measurable_comp_iff, Iff.mp, Set.range
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inr) univ)) :
        (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))

Tactic:
(prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_

Premises used: MeasurableEquiv.Set.rangeInr, Set.Mem, MeasurableEquiv.prodCongr, MeasurableEquiv.symm, MeasurableEquiv.Set.univ, MeasurableEquiv.measurable_comp_iff, Iff.mp
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
refine_2 :
  Measurable (α := β × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inr) univ)) :
          (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInr (Set.univ γ))) :
        (a : β × γ) → (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8)))
⊢ Measurable (α := (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) (β := α × γ ⊕ β × γ)
    ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
        (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
      (⇑(symm (Set.prod (range Sum.inr) univ)) :
        (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
          (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))

Tactic:
refine (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_

Premises used: MeasurableEquiv.Set.rangeInr, MeasurableEquiv.prodCongr, MeasurableEquiv.symm, MeasurableEquiv.Set.univ, MeasurableEquiv.measurable_comp_iff, Iff.mp
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := β × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inr) univ)) :
          (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInr (Set.univ γ))) :
        (a : β × γ) → (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8)))

Tactic:
measurable_inr

Premises used: Sum.map, measurable_inr, Sum.elim
-- 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
γ : Type u_8
inst_3 : MeasurableSpace α
inst_4 : MeasurableSpace β
inst_5 : MeasurableSpace γ
⊢ Measurable (α := β × γ) (β := α × γ ⊕ β × γ)
    (comp (β := (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8))
      ((fun (a : (↑(SProd.sprod (α := Set (α ⊕ β)) (β := Set γ) (range Sum.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
          (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)) ∘
        (⇑(symm (Set.prod (range Sum.inr) univ)) :
          (a : (↑(range Sum.inr) : Type (max u_7 u_6)) × (↑univ : Type u_8)) →
            (↑(range Sum.inr ×ˢ univ) : Type (max (max u_7 u_6) u_8))))
      (⇑(symm (prodCongr Set.rangeInr (Set.univ γ))) :
        (a : β × γ) → (↑(range Sum.inr) : Type (max u_6 u_7)) × (↑univ : Type u_8)))

Tactic:
exact measurable_inr

Premises used: measurable_inr
-- 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)
f : δ ≃ δ'
rw :
  ∀ (a : δ),
    Measurable (β := π ((f : (a : δ) → δ') a)) fun (x : (a : δ') → π a) ↦
      ((Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b)) x a
⊢ Measurable (α := (a : δ') → π a) (β := (b : δ) → π ((f : (a : δ) → δ') b))
    (⇑(Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b))

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- 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)
f : δ ≃ δ'
⊢ ∀ (a : δ),
    Measurable (β := π ((f : (a : δ) → δ') a)) fun (x : (a : δ') → π a) ↦
      ((Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b)) x a

Tactic:
fun i => measurable_pi_apply (f i)

Premises used: measurable_pi_apply, 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)
f : δ ≃ δ'
⊢ ∀ (a : δ),
    Measurable (β := π ((f : (a : δ) → δ') a)) fun (x : (a : δ') → π a) ↦
      ((Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b)) x a

Tactic:
exact fun i => measurable_pi_apply (f i)

Premises used: measurable_pi_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
δ : Type u_4
δ' : Type u_5
π : δ' → Type u_6
inst : (x : δ') → MeasurableSpace (π x)
f : δ ≃ δ'
⊢ Eq (α := (a : (b : δ) → π ((f : (a : δ) → δ') b)) → (a : δ') → π a)
    (⇑(piCongrLeft π f) : (a : (b : δ) → π ((f : (a : δ) → δ') b)) → (a : δ') → π a)
    (⇑(Equiv.piCongrLeft π f) : (a : (a : δ) → π ((f : (a : δ) → δ') a)) → (b : δ') → π b)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β ((e : (a : ι) → ι') i)
i : ι
rw :
  ({ toEquiv := Equiv.piCongrLeft (fun (i' : ι') ↦ β i') e, measurable_toFun := ⋯, measurable_invFun := ⋯ } :
        (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a)
      x ((e : (a : ι) → ι') i) =
    x i
rw₁ :
  (Equiv.piCongrLeft (fun (i' : ι') ↦ β i') e : (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a) x
      ((e : (a : ι) → ι') i) =
    x i
rw₂ rw₃ : x i = x i
⊢ (piCongrLeft (fun (i' : ι') ↦ β i') e : (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a) x
      ((e : (a : ι) → ι') i) =
    x i

Tactic:
rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]

Premises used: MeasurableEquiv.piCongrLeft, MeasurableEquiv.coe_mk, Equiv.piCongrLeft_apply_apply