Theorem: LO.FirstOrder.Structure.extendStructure.func (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
μ : 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
⊢ func (Φ.func f₁) v = func f₁ v
Tactic:
simp[extendStructure]
State after:
μ : 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

State before:
μ : 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
Tactic:
have : ∃ y, ∃ f₁' : L₁.Func k, Φ.func f₁' = Φ.func f₁ ∧ y = s₁.func f₁' v := ⟨s₁.func f₁ v, f₁, rfl, rfl⟩
State after:
μ : 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

State before:
μ : 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
Tactic:
rcases Classical.epsilon_spec this with ⟨f', f'eq, h⟩
State after:
case intro.intro
μ : 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
f' : L₁.Func k
f'eq : Φ.func f' = Φ.func f₁
h : (Classical.epsilon fun y => ∃ f₁', Φ.func f₁' = Φ.func f₁ ∧ y = func f₁' v) = func f' v
⊢ (Classical.epsilon fun y => ∃ f₁_1, Φ.func f₁_1 = Φ.func f₁ ∧ y = func f₁_1 v) = func f₁ v

State before:
case intro.intro
μ : 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
f' : L₁.Func k
f'eq : Φ.func f' = Φ.func f₁
h : (Classical.epsilon fun y => ∃ f₁', Φ.func f₁' = Φ.func f₁ ∧ y = func f₁' v) = func f' v
⊢ (Classical.epsilon fun y => ∃ f₁_1, Φ.func f₁_1 = Φ.func f₁ ∧ y = func f₁_1 v) = func f₁ v
Tactic:
rcases injf f'eq with rfl
State after:
case intro.intro
μ : 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
v : Fin k → M
f' : L₁.Func k
this : ∃ y f₁', Φ.func f₁' = Φ.func f' ∧ y = func f₁' v
f'eq : Φ.func f' = Φ.func f'
h : (Classical.epsilon fun y => ∃ f₁', Φ.func f₁' = Φ.func f' ∧ y = func f₁' v) = func f' v
⊢ (Classical.epsilon fun y => ∃ f₁, Φ.func f₁ = Φ.func f' ∧ y = func f₁ v) = func f' v

State before:
case intro.intro
μ : 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
v : Fin k → M
f' : L₁.Func k
this : ∃ y f₁', Φ.func f₁' = Φ.func f' ∧ y = func f₁' v
f'eq : Φ.func f' = Φ.func f'
h : (Classical.epsilon fun y => ∃ f₁', Φ.func f₁' = Φ.func f' ∧ y = func f₁' v) = func f' v
⊢ (Classical.epsilon fun y => ∃ f₁, Φ.func f₁ = Φ.func f' ∧ y = func f₁ v) = func f' v
Tactic:
exact h
State after:
no goals