awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.inr) univ) : Type (max (max u_6 u_7) u_8))) ↦
    (Equiv.sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (↑a : (α ⊕ β) × γ)
have 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))))
Tactic: refine (Set.prod (range Sum.inr) 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.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))))
have 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)))
Tactic: refine (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_
-- 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 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 : δ ≃ δ'
⊢ Measurable (α := (a : δ') → π a) (β := (b : δ) → π ((f : (a : δ) → δ') b))
    (⇑(Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b))
have rw : ∀ (a : δ),
  Measurable (β := π ((f : (a : δ) → δ') a)) fun (x : (a : δ') → π a) ↦
    ((Equiv.piCongrLeft π f).symm : (a : (a : δ') → π a) → (b : δ) → π ((f : (a : δ) → δ') b)) x a
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
Goal:
ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β ((e : (a : ι) → ι') i)
i : ι
⊢ (piCongrLeft (fun (i' : ι') ↦ β i') e : (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a) x
      ((e : (a : ι) → ι') i) =
    x i
have rw : ({ toEquiv := Equiv.piCongrLeft (fun (i' : ι') ↦ β i') e, measurable_toFun := sorry, measurable_invFun := sorry } :
      (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a)
    x ((e : (a : ι) → ι') i) =
  x i
Tactic: rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ (piCongrLeft (fun (i' : ι') ↦ β i') e : (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a) x
      ((e : (a : ι) → ι') i) =
    x i
have rw₁ : (Equiv.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
⊢ (piCongrLeft (fun (i' : ι') ↦ β i') e : (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a) x
      ((e : (a : ι) → ι') i) =
    x i
have rw₂ : x i = x i
Tactic: rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]
-- 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
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 (α := γ → α × β) (β := (γ → α) × (γ → β))
    (⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) : (a : γ → α × β) → (γ → α) × (γ → β))
have dsimp : Measurable (β := (γ → α) × (γ → β)) fun (f : (i : γ) → α × β) ↦ (fun (c : γ) ↦ (f c).1, fun (c : γ) ↦ (f c).2)
Tactic: dsimp [Equiv.arrowProdEquivProdArrow]
-- 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
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 (α := (γ → α) × (γ → β)) (β := γ → α × β)
    (⇑(Equiv.symm (Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β)) :
      (a : (γ → α) × (γ → β)) → γ → α × β)
have dsimp : Measurable (β := γ → α × β) fun (p : ((i : γ) → α) × ((i : γ) → β)) (c : γ) ↦ (p.1 c, p.2 c)
Tactic: dsimp [Equiv.arrowProdEquivProdArrow]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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) ↦
    (Equiv.sumPiEquivProdPi fun (a : δ ⊕ δ') ↦ α a :
        (a : (i : δ ⊕ δ') → α i) → ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i')))
      fun (i : δ ⊕ δ') ↦ a i
have 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'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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'))) (β := (i : δ ⊕ δ') → α i)
    (⇑(Equiv.sumPiEquivProdPi α).symm :
      (a : ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))) → (i : δ ⊕ δ') → α i)
have 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
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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
have rw : Measurable f
Tactic: rw [← hf.2.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (goal)
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 α⦄, MeasurableSet s → MeasurableSet (f '' s)
have rw : ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
Tactic: rw [← hf.2.1]
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding f
⊢ (↑(f '' univ) : Type u_2) = (↑(range f) : Type u_2)
have rw : (↑(range f) : Type u_2) = (↑(range f) : Type u_2)
Tactic: rw [image_univ]
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding 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))
have 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))
Tactic: rw [image_univ]
-- 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 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
⊢ α ≃ᵐ β
have rcases : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
Tactic: rcases this with ⟨A, Ameas, Afp⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
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
⊢ α ≃ᵐ β
have Bmeas : MeasurableSet B
Tactic: have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ α ≃ᵐ β
have refine : MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
Tactic: refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
have apply : MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
Tactic: apply MeasurableEquiv.sumCongr (hf.equivImage _)
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ Aᶜ = g '' Bᶜ
have a : Aᶜᶜ = (g '' Bᶜ)ᶜ
Tactic: apply compl_injective
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ Aᶜᶜ = (g '' Bᶜ)ᶜ
have a : (F A)ᶜᶜ = (g '' Bᶜ)ᶜ
Tactic: rw [← Afp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Embedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
have this : Aᶜ = g '' Bᶜ
Tactic: have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
-- 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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
have rw : MeasurableEquiv.{u_1, u_2} (↑(g '' Bᶜ) : Type u_1) (↑Bᶜ : Type u_2)
Tactic: rw [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 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
⊢ α ≃ᵐ β
have rcases : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
rcases rcases₁ : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
⊢ α ≃ᵐ β
have rcases₂ : (A : Set α) →
  (Ameas : MeasurableSet A) →
    (Afp : F A = A) →
      let B := f '' A;
      (Bmeas : MeasurableSet B) → α ≃ᵐ β
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
rcases rcases₁ : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
rcases₂ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → α ≃ᵐ β
⊢ α ≃ᵐ β
have rcases₃ : (A : Set α) →
  (Ameas : MeasurableSet A) →
    (Afp : F A = A) →
      let B := f '' A;
      (Bmeas : MeasurableSet B) →
        MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
rcases rcases₁ : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
rcases₂ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → α ≃ᵐ β
rcases₃ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) →
          MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
⊢ α ≃ᵐ β
have rcases₄ : (A : Set α) →
  (Ameas : MeasurableSet A) →
    (Afp : F A = A) →
      let B := f '' A;
      (Bmeas : MeasurableSet B) → MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
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 t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
rcases rcases₁ : (A : Set α) → (Ameas : MeasurableSet A) → (Afp : F A = A) → α ≃ᵐ β
rcases₂ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → α ≃ᵐ β
rcases₃ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) →
          MeasurableEquiv.{u_1, u_2} ((↑A : Type u_1) ⊕ (↑Aᶜ : Type u_1)) ((↑B : Type u_2) ⊕ (↑Bᶜ : Type u_2))
rcases₄ :
  (A : Set α) →
    (Ameas : MeasurableSet A) →
      (Afp : F A = A) →
        let B := f '' A;
        (Bmeas : MeasurableSet B) → MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
⊢ α ≃ᵐ β
have rcases₅ : (A : Set α) →
  (Ameas : MeasurableSet A) →
    (Afp : F A = A) →
      let B := f '' A;
      (Bmeas : MeasurableSet B) → (this : Aᶜ = g '' Bᶜ) → MeasurableEquiv.{u_1, u_2} (↑Aᶜ : Type u_1) (↑Bᶜ : Type u_2)
Tactic: classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm
Cleared hypotheses: this