internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T
Tactic:
have : Structure.Uprod A 𝓤 ⊧ₘ* T := ⟨by intro σ hσ; exact models_Uprod.mpr (h𝓤 $ Set.mem_image_of_mem (Semiformula.domain A) hσ)⟩
Proof state after:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
this : Structure.Uprod A 𝓤 ⊧ₘ* T
⊢ Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
this : Structure.Uprod A 𝓤 ⊧ₘ* T
⊢ Satisfiable T
Tactic:
exact satisfiable_intro (Structure.Uprod A 𝓤) this
Proof state after:
no goals
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
Tactic:
intro i
Proof state after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
i : FinSubtheory T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
i : FinSubtheory T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
Tactic:
exact satisfiable_iff.mp (h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → (Structure.UprodStruc A 𝓤).toStruc ⊧ f
Tactic:
intro σ hσ
Proof state after:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
σ : Sentence L
hσ : σ ∈ T
⊢ (Structure.UprodStruc A 𝓤).toStruc ⊧ σ
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
σ : Sentence L
hσ : σ ∈ T
⊢ (Structure.UprodStruc A 𝓤).toStruc ⊧ σ
Tactic:
exact models_Uprod.mpr (h𝓤 $ Set.mem_image_of_mem (Semiformula.domain A) hσ)
Proof state after:
no goals
Theorem: LO.FirstOrder.compact
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
Tactic:
rw[compactness_aux]
Proof state after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
Theorem: LO.FirstOrder.compact
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ne_and_of_isVType
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
p q r : Semiformula L μ n
h : p.isVType = true
⊢ p ≠ q ⋏ r
Tactic:
rintro rfl
Proof state after:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q r : Semiformula L μ n
h : (q ⋏ r).isVType = true
⊢ False
Theorem: LO.FirstOrder.Semiformula.ne_and_of_isVType
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q r : Semiformula L μ n
h : (q ⋏ r).isVType = true
⊢ False
Tactic:
simp[isVType] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ne_all_of_isVType
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
p : Semiformula L μ n
q : Semiformula L μ (n + 1)
h : p.isVType = true
⊢ p ≠ ∀' q
Tactic:
rintro rfl
Proof state after:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q : Semiformula L μ (n + 1)
h : (∀' q).isVType = true
⊢ False
Theorem: LO.FirstOrder.Semiformula.ne_all_of_isVType
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q : Semiformula L μ (n + 1)
h : (∀' q).isVType = true
⊢ False
Tactic:
simp[isVType] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.isVType_shift_iff
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
n : ℕ
p : SyntacticSemiformula L n
⊢ ((Rew.hom ⇑) p).isVType = isVType p
Tactic:
induction p using rec' <;> simp[Rew.rel, Rew.nrel, isVType]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.isVType_neg_true_of_eq_false
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
n : ℕ
p : SyntacticSemiformula L n
⊢ isVType p = false → (~p).isVType = true
Tactic:
induction p using rec' <;> simp[Rew.rel, Rew.nrel, isVType]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.Restricted.length_rewrite
Proof state before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → Semiterm L ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ₁ Δ₂ Γ : Sequent L
f : ℕ → SyntacticTerm L
d : ⊢ᶜ[C] Δ
⊢ length ↑(rewrite hC f d) = length ↑d
Tactic:
simp[rewrite]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.iff_cut
Proof state before:
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
⊢ Nonempty { d // CutFree d } → ⊢¹! Δ
Tactic:
rintro ⟨d⟩
Proof state after:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d : { d // CutFree d }
⊢  ⊢¹! Δ
Theorem: LO.FirstOrder.Derivation.iff_cut
Proof state before:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d : { d // CutFree d }
⊢  ⊢¹! Δ
Tactic:
exact ⟨d⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.iff_cut
Proof state before:
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
⊢  ⊢¹! Δ → Nonempty { d // CutFree d }
Tactic:
rintro ⟨d⟩
Proof state after:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d :  ⊢¹ Δ
⊢ Nonempty { d // CutFree d }
Theorem: LO.FirstOrder.Derivation.iff_cut
Proof state before:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d :  ⊢¹ Δ
⊢ Nonempty { d // CutFree d }
Tactic:
exact ⟨hauptsatz d⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.encode_encode_eq
Proof state before:
α : Type u_1
inst✝ : Primcodable α
a : α
⊢ goedelNumber (encode a) = goedelNumber a
Tactic:
simp [Semiterm.Operator.encode, goedelNumber_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'
Tactic:
case zero => rintro rfl rfl; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'
Tactic:
case one  => rintro rfl rfl; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'
Tactic:
case add  => rintro rfl rfl; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'
Tactic:
case mul  => rintro rfl rfl; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'
Tactic:
case proj => rintro rfl rfl; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
      (∀ (i : Fin n),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
            (∀ (i : Fin n),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
              z = z'
Tactic:
case comp m n c d ihc ihd =>
  simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
  intro w₁ hc₁ hd₁ w₂ hc₂ hd₂;
  have : w₁ = w₂ := funext fun i => ihd i (hd₁ i) (hd₂ i)
  rcases this with rfl
  exact ihc hc₁ hc₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
c : Code (n✝ + 1)
ih :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
v : Fin n✝ → M
z z' : M
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
          z = z'
Tactic:
case rfind c ih =>
  simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
  intro h₁ hm₁ h₂ hm₂
  by_contra hz
  wlog h : z < z' with Hz
  case inr =>
    have : z' < z := lt_of_le_of_ne (not_lt.mp h) (Ne.symm hz)
    exact Hz (k := k) c ih h₂ hm₂ h₁ hm₁ (Ne.symm hz) this
  have : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c) := hm₂ z h
  rcases this with ⟨x, xz, hx⟩
  exact xz (ih hx h₁)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
⊢ 0 = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
⊢ 1 = 1
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'
Tactic:
rintro rfl rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ + v j✝ = v i✝ + v j✝
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ + v j✝ = v i✝ + v j✝
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'
Tactic:
rintro rfl rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ * v j✝ = v i✝ * v j✝
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ * v j✝ = v i✝ * v j✝
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'
Tactic:
rintro rfl rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ = v i✝
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ = v i✝
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i = v j ∧ z = 1 ∨ ¬v i = v j ∧ z = 0 → v i = v j ∧ z' = 1 ∨ ¬v i = v j ∧ z' = 0 → z = z'
Tactic:
by_cases hv : v i = v j <;> simp[hv]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i = v j
⊢ z = 1 → z' = 1 → z = z'

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i = v j
⊢ z = 0 → z' = 0 → z = z'
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i = v j
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i = v j
⊢ 1 = 1
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i = v j
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i = v j
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i = v j
⊢ 0 = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i = v j
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i < v j ∧ z = 1 ∨ v j ≤ v i ∧ z = 0 → v i < v j ∧ z' = 1 ∨ v j ≤ v i ∧ z' = 0 → z = z'
Tactic:
by_cases hv : v i < v j <;> simp[hv, -not_lt, ←not_lt]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i < v j
⊢ z = 1 → z' = 1 → z = z'

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i < v j
⊢ z = 0 → z' = 0 → z = z'
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i < v j
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i < v j
⊢ 1 = 1
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i < v j
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i < v j
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i < v j
⊢ 0 = 0
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_uniq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i < v j
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals