internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
case inl.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
exact ⟨q, by simp [hn], hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ q ∈ Δ
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
q : SyntacticFormula L
h : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
exact ⟨q, by simp [h], hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
q : SyntacticFormula L
h : q ∈ Δ
hq : (Evalfm M ε) q
⊢ q ∈ Δ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.sound
Proof state before:
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
⊢ s ⊧ σ
Tactic:
rcases s.nonempty with ⟨x⟩
Proof state after:
case intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
⊢ s ⊧ σ
Tactic:
rcases Derivation.sound b.derivation s.Dom (fun _ ↦ x) with ⟨p, hp, h⟩
Proof state after:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
hp : p ∈ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) b.antecedent ++ [σ])
h : (Evalfm s.Dom fun x_1 => x) p
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
hp : p ∈ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) b.antecedent ++ [σ])
h : (Evalfm s.Dom fun x_1 => x) p
⊢ s ⊧ σ
Tactic:
simp at hp
Proof state after:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
h : (Evalfm s.Dom fun x_1 => x) p
hp : (∃ a ∈ b.antecedent, ~Rew.emb.hom a = p) ∨ p = Rew.emb.hom σ
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
h : (Evalfm s.Dom fun x_1 => x) p
hp : (∃ a ∈ b.antecedent, ~Rew.emb.hom a = p) ∨ p = Rew.emb.hom σ
⊢ s ⊧ σ
Tactic:
rcases hp with (⟨π, hπ, rfl⟩ | rfl)
Proof state after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
⊢ s ⊧ σ

case intro.intro.intro.inr
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
h : (Evalfm s.Dom fun x_1 => x) (Rew.emb.hom σ)
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
⊢ s ⊧ σ
Tactic:
have : s ⊧ π := hT.RealizeSet (Gentzen.Disjconseq.subset b π hπ)
Proof state after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ s ⊧ σ
Tactic:
have : ¬s ⊧ π := by simpa using h
Proof state after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this✝ : s ⊧ π
this : ¬s ⊧ π
⊢ s ⊧ σ
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this✝ : s ⊧ π
this : ¬s ⊧ π
⊢ s ⊧ σ
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.sound
Proof state before:
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ ¬s ⊧ π
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.sound
Proof state before:
case intro.intro.intro.inr
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
h : (Evalfm s.Dom fun x_1 => x) (Rew.emb.hom σ)
⊢ s ⊧ σ
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.models_of_subtheory
Proof state before:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
⊢ inst✝¹.toStruc ⊧ p
Tactic:
have : T ⊢ p := System.Subtheory.prf (System.byAxm hp)
Proof state after:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
this : T ⊢ p
⊢ inst✝¹.toStruc ⊧ p
Theorem: LO.FirstOrder.models_of_subtheory
Proof state before:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
this : T ⊢ p
⊢ inst✝¹.toStruc ⊧ p
Tactic:
exact sound this hM
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lang_func
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
⊢ ⟨k, f⟩ ∈ (func f v).lang
Tactic:
simp[lang]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lang_func_ss
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
⊢ (v i).lang ⊆ (func f v).lang
Tactic:
intros x
Proof state after:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (func f v).lang
Theorem: LO.FirstOrder.Semiterm.lang_func_ss
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (func f v).lang
Tactic:
simp[lang]
Proof state after:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x = ⟨k, f⟩ ∨ ∃ a, x ∈ (v a).lang
Theorem: LO.FirstOrder.Semiterm.lang_func_ss
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x = ⟨k, f⟩ ∨ ∃ a, x ∈ (v a).lang
Tactic:
intros h
Proof state after:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ x = ⟨k, f⟩ ∨ ∃ a, x ∈ (v a).lang
Theorem: LO.FirstOrder.Semiterm.lang_func_ss
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ x = ⟨k, f⟩ ∨ ∃ a, x ∈ (v a).lang
Tactic:
exact Or.inr ⟨i, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_toSubLanguage'
Proof state before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n : ℕ
pf : (k : ℕ) → L.Func k → Prop
pr : (k : ℕ) → L.Rel k → Prop
t : Semiterm L μ n
h : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ t.lang → pf k f
⊢ lMap L.ofSubLanguage (toSubLanguage' pf pr t h) = t
Tactic:
induction t <;> simp[*, toSubLanguage', lMap_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.langFunc_rel_ss
Proof state before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
⊢ (v i).lang ⊆ (rel r v).langFunc
Tactic:
intros x
Proof state after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (rel r v).langFunc
Theorem: LO.FirstOrder.Semiformula.langFunc_rel_ss
Proof state before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (rel r v).langFunc
Tactic:
simp[langFunc]
Proof state after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → ∃ a, x ∈ (v a).lang
Theorem: LO.FirstOrder.Semiformula.langFunc_rel_ss
Proof state before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → ∃ a, x ∈ (v a).lang
Tactic:
intros h
Proof state after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ ∃ a, x ∈ (v a).lang
Theorem: LO.FirstOrder.Semiformula.langFunc_rel_ss
Proof state before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ ∃ a, x ∈ (v a).lang
Tactic:
exact ⟨i, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_toSubLanguage'
Proof state before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
pf : (k : ℕ) → L.Func k → Prop
pr : (k : ℕ) → L.Rel k → Prop
n : ℕ
p : Semiformula L μ n
hf : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ p.langFunc → pf k f
hr : ∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ p.langRel → pr k r
⊢ (lMap L.ofSubLanguage) (toSubLanguage' pf pr p hf hr) = p
Tactic:
induction p using rec' <;> simp[*, toSubLanguage', lMap_rel, lMap_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.func
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.func
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.func
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.func
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.func
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.extendStructure.rel
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.val_lMap
Proof state before:
μ : Type u_1
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
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
t : Semiterm L₁ μ n
⊢ Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ t) = Semiterm.val s₁ e ε t
Tactic:
induction t <;> simp[*, Semiterm.lMap_func, Semiterm.val_func]
Proof state after:
case func
μ : Type u_1
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
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
arity✝ : ℕ
a✝¹ : L₁.Func arity✝
a✝ : Fin arity✝ → Semiterm L₁ μ n
a_ih✝ :
  ∀ (a : Fin arity✝), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (a✝ a)) = Semiterm.val s₁ e ε (a✝ a)
⊢ (func (Φ.func a✝¹) fun i => Semiterm.val s₁ e ε (a✝ i)) = func a✝¹ fun i => Semiterm.val s₁ e ε (a✝ i)