internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof state before:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ Sum.inl () ≺ Sum.inr (Sum.inr wq)
Tactic:
apply Fq.Rel_refl
Proof state after:
no goals
Theorem: Collection.mem_set_iff
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x : β
a : α
⊢ x ∈ set a ↔ x ∈ a
Tactic:
simp [set]
Proof state after:
no goals
Theorem: Collection.subset_iff_set_subset_set
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a b : α
⊢ a ⊆ b ↔ set a ⊆ set b
Tactic:
simp [subset_iff, set]
Proof state after:
no goals
Theorem: Collection.empty_subset
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
⊢ ∅ ⊆ a
Tactic:
simp [subset_iff]
Proof state after:
no goals
Theorem: Collection.mem_cons
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ x ∈ cons x a
Tactic:
simp [mem_cons_iff]
Proof state after:
no goals
Theorem: Collection.subset_cons
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ a ⊆ cons x a
Tactic:
simp [subset_iff, mem_cons_iff]
Proof state after:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ ∀ x_1 ∈ a, x_1 = x ∨ x_1 ∈ a
Theorem: Collection.subset_cons
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ ∀ x_1 ∈ a, x_1 = x ∨ x_1 ∈ a
Tactic:
tauto
Proof state after:
no goals
Theorem: Collection.set_empty
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
⊢ set ∅ = ∅
Tactic:
ext
Proof state after:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x✝ : β
⊢ x✝ ∈ set ∅ ↔ x✝ ∈ ∅
Theorem: Collection.set_empty
Proof state before:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x✝ : β
⊢ x✝ ∈ set ∅ ↔ x✝ ∈ ∅
Tactic:
simp [set]
Proof state after:
no goals
Theorem: Collection.set_cons
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
⊢ set (cons z a) = insert z (set a)
Tactic:
ext
Proof state after:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
x✝ : β
⊢ x✝ ∈ set (cons z a) ↔ x✝ ∈ insert z (set a)
Theorem: Collection.set_cons
Proof state before:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
x✝ : β
⊢ x✝ ∈ set (cons z a) ↔ x✝ ∈ insert z (set a)
Tactic:
simp [set]
Proof state after:
no goals
Theorem: Collection.empty_finite
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
⊢ Finite ∅
Tactic:
simp [Finite]
Proof state after:
no goals
Theorem: Collection.cons_finite_iff
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
h : Finite (cons z a)
⊢ a ⊆ cons z a
Tactic:
simp
Proof state after:
no goals
Theorem: Collection.cons_finite_iff
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
⊢ Finite a → Finite (cons z a)
Tactic:
simpa [Finite] using Set.Finite.insert z
Proof state after:
no goals
Theorem: Collection.mem_list_toCollection
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x : β
l : List β
⊢ x ∈ l.toCollection ↔ x ∈ l
Tactic:
induction l <;> simp [List.toCollection, *]
Proof state after:
no goals
Theorem: Collection.mem_finset_toCollection
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x : β
s : Finset β
⊢ x ∈ s.toCollection ↔ x ∈ s
Tactic:
simp [Finset.toCollection]
Proof state after:
no goals
Theorem: Collection.list_toCollection_finite
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
l : List β
⊢ Finite l.toCollection
Tactic:
simp [Finite, set]
Proof state after:
no goals
Theorem: Collection.finset_toCollection_finite
Proof state before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
s : Finset β
⊢ Finite s.toCollection
Tactic:
simp [Finite, set]
Proof state after:
no goals
Theorem: Set.collection_finite_iff
Proof state before:
α : Type u_1
s : Set α
⊢ Collection.Finite s ↔ s.Finite
Tactic:
simp [Collection.Finite]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.val_lMap_add₁
Proof state before:
L₁ : Language
L₂ : Language
M : Type u_1
str₁ : Structure L₁ M
str₂ : Structure L₂ M
μ : Type u_2
n : ℕ
t : Semiterm L₁ μ n
e : Fin n → M
ε : μ → M
⊢ Semiterm.val (add L₁ L₂ M) e ε (Semiterm.lMap (Language.Hom.add₁ L₁ L₂) t) = Semiterm.val str₁ e ε t
Tactic:
induction t <;> simp [Semiterm.val, Language.Hom.func_add₁, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.val_lMap_add₂
Proof state before:
L₁ : Language
L₂ : Language
M : Type u_1
str₁ : Structure L₁ M
str₂ : Structure L₂ M
μ : Type u_2
n : ℕ
t : Semiterm L₂ μ n
e : Fin n → M
ε : μ → M
⊢ Semiterm.val (add L₁ L₂ M) e ε (Semiterm.lMap (Language.Hom.add₂ L₁ L₂) t) = Semiterm.val str₂ e ε t
Tactic:
induction t <;> simp [Semiterm.val, Language.Hom.func_add₂, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_lMap_add₁
Proof state before:
L₁ : Language
L₂ : Language
M : Type u_1
str₁ : Structure L₁ M
str₂ : Structure L₂ M
μ : Type u_2
n : ℕ
p : Semiformula L₁ μ n
e : Fin n → M
ε : μ → M
⊢ (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₁ L₁ L₂)) p) ↔ (Semiformula.Eval str₁ e ε) p
Tactic:
induction p using Semiformula.rec' <;>
  simp [*, Language.Hom.rel_add₁, Semiformula.eval_rel,
    Semiformula.lMap_rel, Semiformula.eval_nrel, Semiformula.lMap_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_lMap_add₂
Proof state before:
L₁ : Language
L₂ : Language
M : Type u_1
str₁ : Structure L₁ M
str₂ : Structure L₂ M
μ : Type u_2
n : ℕ
p : Semiformula L₂ μ n
e : Fin n → M
ε : μ → M
⊢ (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₂ L₁ L₂)) p) ↔ (Semiformula.Eval str₂ e ε) p
Tactic:
induction p using Semiformula.rec' <;>
  simp [*, Language.Hom.rel_add₂, Semiformula.eval_rel,
    Semiformula.lMap_rel, Semiformula.eval_nrel, Semiformula.lMap_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.val_lMap_sigma
Proof state before:
ι : Type u_4
L : ι → Language
M : Type u_1
str : (i : ι) → Structure (L i) M
i : ι
μ : Type u_2
n : ℕ
t : Semiterm (L i) μ n
e : Fin n → M
ε : μ → M
⊢ Semiterm.val (sigma L M) e ε (Semiterm.lMap (Language.Hom.sigma L i) t) = Semiterm.val (str i) e ε t
Tactic:
induction t <;> simp [Semiterm.val, Language.Hom.func_sigma, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_lMap_sigma
Proof state before:
ι : Type u_4
L : ι → Language
M : Type u_1
str : (i : ι) → Structure (L i) M
i : ι
μ : Type u_2
n : ℕ
p : Semiformula (L i) μ n
e : Fin n → M
ε : μ → M
⊢ (Semiformula.Eval (sigma L M) e ε) ((Semiformula.lMap (Language.Hom.sigma L i)) p) ↔ (Semiformula.Eval (str i) e ε) p
Tactic:
induction p using Semiformula.rec' <;>
  simp [*, Language.Hom.rel_sigma, Semiformula.eval_rel,
    Semiformula.lMap_rel, Semiformula.eval_nrel, Semiformula.lMap_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.valm_uLift
Proof state before:
L : Language
M : Type v
inst✝ : Structure L M
n : ℕ
ξ : Type u_1
e : Fin n → ULift.{v', v} M
ε : ξ → ULift.{v', v} M
t : Semiterm L ξ n
⊢ valm (ULift.{v', v} M) e ε t = { down := valm M (fun i => (e i).down) (fun i => (ε i).down) t }
Tactic:
induction t <;> simp [*, Semiterm.val_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.evalm_uLift
Proof state before:
L : Language
M : Type v
inst✝ : Structure L M
n : ℕ
ξ : Type u_1
e : Fin n → ULift.{v', v} M
ε : ξ → ULift.{v', v} M
p : Semiformula L ξ n
⊢ (Evalm (ULift.{v', v} M) e ε) p ↔ (Evalm M (fun i => (e i).down) fun i => (ε i).down) p
Tactic:
induction p using Semiformula.rec' <;>
  simp [*, Semiformula.eval_rel, Semiformula.eval_nrel, Semiterm.valm_uLift, Matrix.comp_vecCons']
Proof state after:
no goals
Theorem: LO.FirstOrder.uLift_elementaryEquiv
Proof state before:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
⊢ ULift.{v', v} M ≡ₑ[L] M
Tactic:
intro σ
Proof state after:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
σ : Sentence L
⊢ ULift.{v', v} M ⊧ₘ σ ↔ M ⊧ₘ σ
Theorem: LO.FirstOrder.uLift_elementaryEquiv
Proof state before:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
σ : Sentence L
⊢ ULift.{v', v} M ⊧ₘ σ ↔ M ⊧ₘ σ
Tactic:
simp [models_iff, Semiformula.evalm_uLift, Matrix.empty_eq, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs_varSumInL
Proof state before:
L : Language
μ : Type u_1
inst✝ : Semiformula.Operator.Eq L
k n : ℕ
w₁ w₂ : Fin k → Semiterm L μ n
i : Fin k
⊢ (Rew.substs (Matrix.vecAppend ⋯ w₁ w₂)) (varSumInL i) = w₁ i
Tactic:
simp [varSumInL, Matrix.vecAppend_eq_ite]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs_varSumInR
Proof state before:
L : Language
μ : Type u_1
inst✝ : Semiformula.Operator.Eq L
k n : ℕ
w₁ w₂ : Fin k → Semiterm L μ n
i : Fin k
⊢ (Rew.substs (Matrix.vecAppend ⋯ w₁ w₂)) (varSumInR i) = w₂ i
Tactic:
simp [varSumInR, Matrix.vecAppend_eq_ite]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.emb_varSumInL
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
k : ℕ
o : Type u_2
inst✝ : IsEmpty o
i : Fin k
⊢ Rew.emb (varSumInL i) = varSumInL i
Tactic:
simp [varSumInL]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.emb_varSumInR
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
k : ℕ
o : Type u_2
inst✝ : IsEmpty o
i : Fin k
⊢ Rew.emb (varSumInR i) = varSumInR i
Tactic:
simp [varSumInR]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
⊢ ∀ ⦃f : Sentence L⦄, f ∈ 𝐄𝐐 → inst✝¹.toStruc ⊧ f
Tactic:
intro σ h
Proof state after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
σ : Sentence L
h : σ ∈ 𝐄𝐐
⊢ inst✝¹.toStruc ⊧ σ
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
σ : Sentence L
h : σ ∈ 𝐄𝐐
⊢ inst✝¹.toStruc ⊧ σ
Tactic:
cases h <;> simp [models_def, Semiformula.vecEq, Semiterm.val_func]
Proof state after:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
        func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

case relExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r✝ : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r✝ Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r✝ Semiterm.varSumInR)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInR)
Tactic:
case relExt r =>
  simp [Semiformula.eval_rel]; intro e h; simp [congr_arg (rel r) (funext h)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
        func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
intro e h
Proof state after:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
    func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
    func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
congr
Proof state after:
case funcExt.e_a
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) = fun i =>
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
case funcExt.e_a
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) = fun i =>
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
funext i
Proof state after:
case funcExt.e_a.h
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
i : Fin k✝
⊢ Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
case funcExt.e_a.h
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
i : Fin k✝
⊢ Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
exact h i
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInR)
Tactic:
simp [Semiformula.eval_rel]
Proof state after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
        rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
        rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
intro e h
Proof state after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
    rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom
Proof state before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
    rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
simp [congr_arg (rel r) (funext h)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_refl
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
⊢ eqv L a a
Tactic:
have : M ⊧ₘ “∀ x, x = x” := H.realize (Theory.eqAxiom.refl (L := L))
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : M ⊧ₘ (“∀' #0 = #0”)
⊢ eqv L a a
Theorem: LO.FirstOrder.Structure.Eq.eqv_refl
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : M ⊧ₘ (“∀' #0 = #0”)
⊢ eqv L a a
Tactic:
simp [models_def] at this
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : ∀ (x : M), op(=).val ![x, x]
⊢ eqv L a a
Theorem: LO.FirstOrder.Structure.Eq.eqv_refl
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : ∀ (x : M), op(=).val ![x, x]
⊢ eqv L a a
Tactic:
exact this a
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_symm
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ eqv L a b → eqv L b a
Tactic:
have : M ⊧ₘ “∀ x y, x = y → y = x” := H.realize (Theory.eqAxiom.symm (L := L))
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : M ⊧ₘ (“∀' ∀' (#1 = #0 → #0 = #1)”)
⊢ eqv L a b → eqv L b a
Theorem: LO.FirstOrder.Structure.Eq.eqv_symm
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : M ⊧ₘ (“∀' ∀' (#1 = #0 → #0 = #1)”)
⊢ eqv L a b → eqv L b a
Tactic:
simp [models_def] at this
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : ∀ (x x_1 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x]
⊢ eqv L a b → eqv L b a
Theorem: LO.FirstOrder.Structure.Eq.eqv_symm
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : ∀ (x x_1 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x]
⊢ eqv L a b → eqv L b a
Tactic:
exact this a b
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_trans
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
⊢ eqv L a b → eqv L b c → eqv L a c
Tactic:
have : M ⊧ₘ “∀ x y z, x = y → y = z → x = z” := H.realize (Theory.eqAxiom.trans (L := L))
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
this : M ⊧ₘ (“∀' ∀' ∀' (#2 = #1 → (#1 = #0 → #2 = #0))”)
⊢ eqv L a b → eqv L b c → eqv L a c
Theorem: LO.FirstOrder.Structure.Eq.eqv_trans
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
this : M ⊧ₘ (“∀' ∀' ∀' (#2 = #1 → (#1 = #0 → #2 = #0))”)
⊢ eqv L a b → eqv L b c → eqv L a c
Tactic:
simp [models_def] at this
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
this : ∀ (x x_1 x_2 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x_2] → op(=).val ![x, x_2]
⊢ eqv L a b → eqv L b c → eqv L a c
Theorem: LO.FirstOrder.Structure.Eq.eqv_trans
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b c : M
this : ∀ (x x_1 x_2 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x_2] → op(=).val ![x, x_2]
⊢ eqv L a b → eqv L b c → eqv L a c
Tactic:
exact this a b c
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_funcExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ eqv L (func f v) (func f w)
Tactic:
have : M ⊧ₘ ∀* (Semiformula.vecEq varSumInL varSumInR ⟶ op(=).operator ![Semiterm.func f varSumInL, Semiterm.func f varSumInR]) :=
  H.realize (eqAxiom.funcExt f (L := L))
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (“(!(vecEq varSumInL varSumInR) → !!(Semiterm.func f varSumInL) = !!(Semiterm.func f varSumInR))”)
⊢ eqv L (func f v) (func f w)