awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
rw : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
rw₁ : (∀ m_1 ∈ range m, MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
have rw₂ : (∀ (i : ι), MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
Tactic: rw [iInf, measurableSet_sInf, forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (n : ι), m n) (generateFrom {s : Set α | ∃ (n : ι), MeasurableSet s})
have h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Defs (goal)
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s
have h : GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s ↔ MeasurableSet s
Tactic: rw [measurableSet_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)
have rwa : MeasurableSet (g '' f '' s)
Tactic: rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (g '' f '' s)
⊢ MeasurableSet (g ∘ f '' s)
have rwa₁ : MeasurableSet (f '' s)
Tactic: rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)
have rw : MeasurableSet (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f '' f ⁻¹' s)
Tactic: rw [← image_preimage_eq_inter_range, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
rw : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f '' f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw₁ : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f ⁻¹' s)
Tactic: rw [← image_preimage_eq_inter_range, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
have rwa : MeasurableSet (rangeFactorization f '' s)
Tactic: rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (rangeFactorization f '' s)
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
have rwa₁ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) '' rangeFactorization f '' s)
Tactic: rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (rangeFactorization f '' s)
rwa₁ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) '' rangeFactorization f '' s)
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
have rwa₂ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) ∘ rangeFactorization f '' s)
Tactic: rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (rangeFactorization f '' s)
rwa₁ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) '' rangeFactorization f '' s)
rwa₂ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) ∘ rangeFactorization f '' s)
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
have rwa₃ : MeasurableSet (f '' s)
Tactic: rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')
have refine_1 : Measurable ((range f).restrict (π := fun (a : β) ↦ γ) (extend f g g'))
Tactic: refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
refine_1 : Measurable ((range f).restrict (π := fun (a : β) ↦ γ) (extend f g g'))
⊢ Measurable (extend f g g')
have refine_2 : Measurable ((range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g'))
Tactic: refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).restrict (π := fun (a : β) ↦ γ) (extend f g g'))
have refine_1 : Measurable.{u_2, u_3} (β := γ) fun (x : (↑(range f) : Type u_2)) ↦
  g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) sorry)
Tactic: rw [restrict_extend_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g'))
have refine_2 : Measurable (α := (↑(range f)ᶜ : Type u_2)) (g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ))
Tactic: rw [restrict_extend_compl_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f
have refine : ∀ (H : Measurable (g ∘ f)), Measurable f
Tactic: refine ⟨fun H => ?_, hg.measurable.comp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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)
⊢ Measurable f
have rwa : ∀ (this : Measurable (_root_.id ∘ f)), Measurable f
Tactic: rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 f
have suffices : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
Tactic: suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 s
have h₁ : s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s
Tactic: convert! (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 s
have h₁ : s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s ∪ i₃ '' i₃ ⁻¹' s
Tactic: convert!
    (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂) |>.union
      (hi₃.measurableSet_image' hs₃)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = (⇑e : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t
have rw : s = (⇑e.toEquiv : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t
Tactic: rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ s = (⇑e : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t
have rw₁ : (⇑e.symm : (a : β) → α) '' s = t ↔ (⇑e.symm : (a : β) → α) '' s = t
Tactic: rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ s = (⇑e : (a : α) → β) '' t ↔ (⇑e.symm : (a : β) → α) '' s = t
have rw₂ : (⇑e.symm : (a : β) → α) '' s = t ↔ (⇑e.symm : (a : β) → α) '' s = t
Tactic: rw [← coe_toEquiv, Equiv.eq_image_iff_symm_image_eq, coe_toEquiv_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ Set.image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s) = s
have rw : Set.image.{u_1, u_2} (α := α) (⇑e.toEquiv : (a : α) → β) ((⇑e.toEquiv : (a : α) → β) ⁻¹' s) = s
Tactic: rw [← coe_toEquiv, Equiv.image_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ Set.image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s) = s
have rw₁ : s = s
Tactic: rw [← coe_toEquiv, Equiv.image_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ preimage.{u_1, u_2} (β := β) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) '' s) = s
have rw : preimage.{u_1, u_2} (β := β) (⇑e.toEquiv : (a : α) → β) ((⇑e.toEquiv : (a : α) → β) '' s) = s
Tactic: rw [← coe_toEquiv, Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ preimage.{u_1, u_2} (β := β) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) '' s) = s
have rw₁ : s = s
Tactic: rw [← coe_toEquiv, Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet.{u_2} (α := β) ((⇑e : (a : α) → β) '' s) ↔ MeasurableSet s
have rw : MeasurableSet.{u_2} (α := β) ((⇑e.symm : (a : β) → α) ⁻¹' s) ↔ MeasurableSet s
Tactic: rw [image_eq_preimage_symm, measurableSet_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ MeasurableSet.{u_2} (α := β) ((⇑e : (a : α) → β) '' s) ↔ MeasurableSet s
have rw₁ : MeasurableSet s ↔ MeasurableSet s
Tactic: rw [image_eq_preimage_symm, measurableSet_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
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
have this : Measurable (α := β) (f ∘ (⇑(e.symm.trans e).toEquiv : (a : β) → β))
Tactic: have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 : β) → β))
⊢ Measurable f
have rwa : ∀ (this : Measurable (α := β) (f ∘ (⇑(e.symm.trans e) : (a : β) → β))), Measurable f
Tactic: rwa [coe_toEquiv, symm_trans_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ Measurable f
have rwa₁ : ∀ (this : Measurable (α := β) (f ∘ (⇑(refl β) : (a : β) → β))), Measurable f
Tactic: rwa [coe_toEquiv, symm_trans_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_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)
have 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
Tactic: refine ⟨_, hs.inl_image, Set.ext ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s_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)
have 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
Tactic: refine ⟨_, hs.inr_image, Set.ext ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 (α := (α ⊕ β) × γ) (β := α × γ ⊕ β × γ) (⇑(Equiv.sumProdDistrib α β γ) : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ)
have 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 : (α ⊕ β) × γ)
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]) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 : (α ⊕ β) × γ)
⊢ Measurable (α := (α ⊕ β) × γ) (β := α × γ ⊕ β × γ) (⇑(Equiv.sumProdDistrib α β γ) : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ)
have 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 : (α ⊕ β) × γ)
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]) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 : (α ⊕ β) × γ)
have 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))))
Tactic: refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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))))
have 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)))
Tactic: refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_