have : ∃ y, ∃ f₁' : L₁.Func k, Φ.func f₁' = Φ.func f₁ ∧ y = s₁.func f₁' v := ⟨s₁.func f₁ v, f₁, rfl, rfl⟩
μ : Sort ?u.89513
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
k : ℕ
injf : Function.Injective Φ.func
f₁ : L₁.Func k
v : Fin k → M
⊢ (Classical.epsilon fun y => ∃ f₁_1, Φ.func f₁_1 = Φ.func f₁ ∧ y = func f₁_1 v) = func f₁ v
μ : Sort ?u.89513
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
k : ℕ
injf : Function.Injective Φ.func
f₁ : L₁.Func k
v : Fin k → M
this : ∃ y f₁', Φ.func f₁' = Φ.func f₁ ∧ y = func f₁' v
⊢ (Classical.epsilon fun y => ∃ f₁_1, Φ.func f₁_1 = Φ.func f₁ ∧ y = func f₁_1 v) = func f₁ v