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

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

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

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
intro y y'

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

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

Tactic:
intro s hs

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

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

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 γ
x✝ : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
x : α × β
⊢ x ∈ (fun y => (x✝, f y)) '' s ↔ x ∈ {x✝} ×ˢ (f '' s)

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

Tactic:
exact fun h ↦ hf.injective h

Result:
no goals

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

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

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