-- Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
lemma MeasurableEmbedding.prod_mk_right {β γ : Type*} [MeasurableSingletonClass α]
    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
    {f : γ → β} (hf : MeasurableEmbedding f) (x : α) :
    MeasurableEmbedding (fun y ↦ (f y, x)) where
  injective

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
⊢ ∀ ⦃s : Set γ⦄, MeasurableSet s → MeasurableSet ((fun y => (f y, x)) '' s)

Tactic:
intro s hs

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet ((fun y => (f y, x)) '' s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet ((fun y => (f y, x)) '' s)

Tactic:
convert (hf.measurableSet_image.mpr hs).prod (MeasurableSet.singleton x)

Result:
case h.e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (fun y => (f y, x)) '' s = (f '' s) ×ˢ {x}

Proof state:
case h.e'_3.h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x✝ : α
s : Set γ
hs : MeasurableSet s
x : β × α
⊢ x ∈ (fun y => (f y, x✝)) '' s ↔ x ∈ (f '' s) ×ˢ {x✝}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
y y' : γ
⊢ (fun y => (f y, x)) y = (fun y => (f y, x)) y' → y = y'

Tactic:
simp only [Prod.mk.injEq, and_true]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
y y' : γ
⊢ f y = f y' → y = y'

Proof state:
case h.e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (fun y => (f y, x)) '' s = (f '' s) ×ˢ {x}

Tactic:
ext x

Result:
case h.e'_3.h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x✝ : α
s : Set γ
hs : MeasurableSet s
x : β × α
⊢ x ∈ (fun y => (f y, x✝)) '' s ↔ x ∈ (f '' s) ×ˢ {x✝}

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
⊢ Function.Injective fun y => (f y, x)

Tactic:
intro y y'

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
y y' : γ
⊢ (fun y => (f y, x)) y = (fun y => (f y, x)) y' → y = y'

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : γ → β
hf : MeasurableEmbedding f
x : α
y y' : γ
⊢ f y = f y' → y = y'

Tactic:
exact fun h ↦ hf.injective h

Result:
no goals