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

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
⊢ rel (Φ.rel r₁) v ↔ rel r₁ v
Tactic:
simp[extendStructure]
State after:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
⊢ (∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v) ↔ rel r₁ v

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
⊢ (∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v) ↔ rel r₁ v
Tactic:
refine ⟨by intros h; rcases h with ⟨r₁', e, h⟩; rcases injr e; exact h, by intros h; refine ⟨r₁, rfl, h⟩⟩
State after:
no goals

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
⊢ (∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v) → rel r₁ v
Tactic:
intros h
State after:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
h : ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v
⊢ rel r₁ v

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
h : ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v
⊢ rel r₁ v
Tactic:
rcases h with ⟨r₁', e, h⟩
State after:
case intro.intro
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
r₁' : L₁.Rel k
e : Φ.rel r₁' = Φ.rel r₁
h : rel r₁' v
⊢ rel r₁ v

State before:
case intro.intro
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
r₁' : L₁.Rel k
e : Φ.rel r₁' = Φ.rel r₁
h : rel r₁' v
⊢ rel r₁ v
Tactic:
rcases injr e
State after:
case intro.intro.refl
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
e : Φ.rel r₁ = Φ.rel r₁
h : rel r₁ v
⊢ rel r₁ v

State before:
case intro.intro.refl
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
e : Φ.rel r₁ = Φ.rel r₁
h : rel r₁ v
⊢ rel r₁ v
Tactic:
exact h
State after:
no goals

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
⊢ rel r₁ v → ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v
Tactic:
intros h
State after:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
h : rel r₁ v
⊢ ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v

State before:
μ : Sort ?u.98034
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 : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
h : rel r₁ v
⊢ ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v
Tactic:
refine ⟨r₁, rfl, h⟩
State after:
no goals