internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit.mp
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
⊢ (∃ e, isProofFn T σ e = true) →
    ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
intro h
Proof state after:
case unit.mp
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h : ∃ e, isProofFn T σ e = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit.mp
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h : ∃ e, isProofFn T σ e = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
rcases Nat.least_number _ h with ⟨e, he, hm⟩
Proof state after:
case unit.mp.intro.intro
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit.mp.intro.intro
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
exact ⟨e, ⟨he, fun h => by simpa using hm _ h⟩, he⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
h✝ : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
m✝ : ℕ
h : m✝ < e
⊢ isProofFn T σ m✝ = false
Tactic:
simpa using hm _ h
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit.mpr
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
⊢ (∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true) →
    ∃ e, isProofFn T σ e = true
Tactic:
rintro ⟨e, ⟨he, _⟩, _⟩
Proof state after:
case unit.mpr.intro.intro.intro
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
e : ℕ
right✝¹ he : isProofFn T σ e = true
right✝ : ∀ {m : ℕ}, m < e → isProofFn T σ m = false
⊢ ∃ e, isProofFn T σ e = true
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit.mpr.intro.intro.intro
μ : Type ?u.1286883
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
e : ℕ
right✝¹ he : isProofFn T σ e = true
right✝ : ∀ {m : ℕ}, m < e → isProofFn T σ m = false
⊢ ∃ e, isProofFn T σ e = true
Tactic:
exact ⟨e, he⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.isProofFn_computable
Proof state before:
μ : Type ?u.1302484
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ Primrec fun p => decide (List.map (⇑Rew.emb.hom) (p.1.1 :: List.map (fun x => ~x) p.2.2) ∈ p.2.1.sequents)
Tactic:
apply Primrec.list_mem.comp
  (Primrec.list_map
    (Primrec.list_cons.comp (Primrec.fst.comp .fst)
      (Primrec.list_map (Primrec.snd.comp .snd) $ Semiformula.neg_primrec.comp₂ .right))
      <| Semiformula.emb_primrec.comp₂ .right)
  (Primrec.list_map (Primrec.fst.comp .snd) <| Primrec.snd.comp₂ .right)
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_RePred
Proof state before:
μ : Type ?u.1325212
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ∀ (n : Sentence L), provableFn T n = Part.assert ((fun x => T ⊢! x) n) fun x => Part.some ()
Tactic:
intro σ
Proof state after:
μ : Type ?u.1325212
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
σ : Sentence L
⊢ provableFn T σ = Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Theorem: LO.FirstOrder.provable_RePred
Proof state before:
μ : Type ?u.1325212
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
σ : Sentence L
⊢ provableFn T σ = Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Tactic:
ext
Proof state after:
case H
μ : Type ?u.1325212
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
σ : Sentence L
a✝ : Unit
⊢ a✝ ∈ provableFn T σ ↔ a✝ ∈ Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Theorem: LO.FirstOrder.provable_RePred
Proof state before:
case H
μ : Type ?u.1325212
L : Language
inst✝⁸ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁷ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁴ : UniformlyPrimcodable L.Func
inst✝³ : UniformlyPrimcodable L.Rel
inst✝² : Primcodable μ
T : Theory L
inst✝¹ : DecidablePred T
inst✝ : T.Computable
σ : Sentence L
a✝ : Unit
⊢ a✝ ∈ provableFn T σ ↔ a✝ ∈ Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Tactic:
simp[←provable_iff_provableFn]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
w : M₁.World
⊢ w ⊧ p ↔ f w ⊧ p
Tactic:
induction p using Formula.rec' generalizing w with
| hatom p =>
  constructor;
  . apply hMor.atomic |>.mp;
  . apply hMor.atomic |>.mpr
| hbox p ih =>
  simp;
  constructor;
  . intro h w₂ hw₂;
    obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂;
    have := ih.mp $ h w₁ hww₁;
    subst e;
    assumption;
  . intro h w' hww';
    exact ih.mpr $ h (f w') $ hMor.forth hww';
| _ => simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hatom
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p ↔ f w ⊧ atom p
Tactic:
constructor
Proof state after:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p

case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p

case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
. apply hMor.atomic |>.mp;
Proof state after:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
. apply hMor.atomic |>.mpr
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p
Tactic:
apply hMor.atomic |>.mp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
apply hMor.atomic |>.mpr
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ w ⊧ □p ↔ f w ⊧ □p
Tactic:
simp
Proof state after:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) ↔ ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) ↔ ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
Tactic:
constructor
Proof state after:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p

case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p

case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
. intro h w₂ hw₂;
  obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂;
  have := ih.mp $ h w₁ hww₁;
  subst e;
  assumption;
Proof state after:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
. intro h w' hww';
  exact ih.mpr $ h (f w') $ hMor.forth hww';
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
Tactic:
intro h w₂ hw₂
Proof state after:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
⊢ Satisfies M₂ w₂ p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
⊢ Satisfies M₂ w₂ p
Tactic:
obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂
Proof state after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
⊢ Satisfies M₂ w₂ p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
⊢ Satisfies M₂ w₂ p
Tactic:
have := ih.mp $ h w₁ hww₁
Proof state after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
this : f w₁ ⊧ p
⊢ Satisfies M₂ w₂ p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
this : f w₁ ⊧ p
⊢ Satisfies M₂ w₂ p
Tactic:
subst e
Proof state after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
this : f w₁ ⊧ p
hw₂ : f w ≺ f w₁
⊢ Satisfies M₂ (f w₁) p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
this : f w₁ ⊧ p
hw₂ : f w ≺ f w₁
⊢ Satisfies M₂ (f w₁) p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
intro h w' hww'
Proof state after:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
w' : M₁.Frame.World
hww' : w ≺ w'
⊢ Satisfies M₁ w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
w' : M₁.Frame.World
hww' : w ≺ w'
⊢ Satisfies M₁ w' p
Tactic:
exact ih.mpr $ h (f w') $ hMor.forth hww'
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism
Proof state before:
case hor
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p✝ q✝ : Formula α
a✝¹ : ∀ {w : M₁.World}, w ⊧ p✝ ↔ f w ⊧ p✝
a✝ : ∀ {w : M₁.World}, w ⊧ q✝ ↔ f w ⊧ q✝
w : M₁.World
⊢ w ⊧ p✝ ⋎ q✝ ↔ f w ⊧ p✝ ⋎ q✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ F₁ ⊧ p → F₂ ⊧ p
Tactic:
contrapose
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ ¬F₂ ⊧ p → ¬F₁ ⊧ p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ ¬F₂ ⊧ p → ¬F₁ ⊧ p
Tactic:
intro h
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ¬F₂ ⊧ p
⊢ ¬F₁ ⊧ p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ¬F₂ ⊧ p
⊢ ¬F₁ ⊧ p
Tactic:
obtain ⟨V₂, w₂, h⟩ := by simpa [ValidOnFrame, ValidOnModel] using h;
Proof state after:
case intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ¬F₁ ⊧ p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
case intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ¬F₁ ⊧ p
Tactic:
simp [ValidOnFrame, ValidOnModel]
Proof state after:
case intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
case intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p
Tactic:
obtain ⟨w₁, e⟩ : ∃ w₁, f w₁ = w₂ := by apply hSur;
Proof state after:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p