internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
case a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ ◇^[t.i](□^[t.m]Γ.conj') ⟶ □^[t.j](◇^[t.n]Γ.conj') ∈ 𝗴𝗲(t)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
apply andImplyIffImplyImply'!.mpr
Proof state after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ ◇^[t.n]Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
exact imp_trans!
  (show L ⊢! □^[t.n](Δ.conj') ⟶ □^[t.n](~Γ.conj') by exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC)
  (show L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj') by exact contra₁'! $ conj₁'! $ multidiaDuality!)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ □^[t.n](~Γ.conj')
Tactic:
exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj')
Tactic:
exact contra₁'! $ conj₁'! $ multidiaDuality!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ L ⊬! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
simpa using Ω₃.consistent (Γ := [□^[t.n](Δ.conj'), ◇^[t.n](Γ.conj')]) (by simp_all)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ [□^[t.n]Δ.conj', ◇^[t.n]Γ.conj'], p ∈ Ω₃.theory
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[t.n]p ∈ Ω₃.theory → p ∈ Ω.theory
Tactic:
intros
Proof state after:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ Ω.theory
Tactic:
apply hΩ
Proof state after:
case right.a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom
Proof state before:
case right.a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
ts : List Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
hAx : 𝗚𝗲(ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Tactic:
induction ts with
| nil => simp [MultiGeachConfluent];
| cons t ts ih =>
  simp;
  constructor;
  . exact definability_canonicalFrame_GeachAxiom (includeK := ⟨(Set.Subset.trans AxiomSet.MultiGeach.subsetK hAx)⟩) (by aesop)
  . apply ih;
    simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case nil
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
hAx : 𝗚𝗲([]) ⊆ Ax(L)
⊢ MultiGeachConfluent [] (CanonicalFrame L)
Tactic:
simp [MultiGeachConfluent]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent (t :: ts) (CanonicalFrame L)
Tactic:
simp
Proof state after:
case cons
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L) ∧ MultiGeachConfluent ts (CanonicalFrame L)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L) ∧ MultiGeachConfluent ts (CanonicalFrame L)
Tactic:
constructor
Proof state after:
case cons.left
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L)

case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons.left
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L)

case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Tactic:
. exact definability_canonicalFrame_GeachAxiom (includeK := ⟨(Set.Subset.trans AxiomSet.MultiGeach.subsetK hAx)⟩) (by aesop)
Proof state after:
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Tactic:
. apply ih;
  simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons.left
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L)
Tactic:
exact definability_canonicalFrame_GeachAxiom (includeK := ⟨(Set.Subset.trans AxiomSet.MultiGeach.subsetK hAx)⟩) (by aesop)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
x✝ y✝ z✝ : (CanonicalFrame L).World
⊢ 𝗴𝗲(t) ⊆ Ax(L)
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
Tactic:
apply ih
Proof state after:
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ 𝗚𝗲(ts) ⊆ Ax(L)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom
Proof state before:
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ 𝗚𝗲(ts) ⊆ Ax(L)
Tactic:
simp_all
Proof state after:
no goals
Theorem: insert_sorted_size_eq
Proof state before:
α : Type u_1
inst✝ : Ord α
len i : Nat
⊢ ∀ (arr : Array α) (isLt : i < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i, isLt := isLt }) = len
Tactic:
induction i with
| zero =>
  intro arr isLt hLen
  simp [insertSorted, hLen]
| succ i' ih =>
  intro arr isLt hLen
  simp [insertSorted]
  split <;> try simp[*]
Proof state after:
no goals
Theorem: insert_sorted_size_eq
Proof state before:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
⊢ ∀ (arr : Array α) (isLt : Nat.zero < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.zero, isLt := isLt }) = len
Tactic:
intro arr isLt hLen
Proof state after:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted arr { val := Nat.zero, isLt := isLt }) = len
Theorem: insert_sorted_size_eq
Proof state before:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted arr { val := Nat.zero, isLt := isLt }) = len
Tactic:
simp [insertSorted, hLen]
Proof state after:
no goals
Theorem: insert_sorted_size_eq
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
⊢ ∀ (arr : Array α) (isLt : Nat.succ i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.succ i', isLt := isLt }) = len
Tactic:
intro arr isLt hLen
Proof state after:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted arr { val := Nat.succ i', isLt := isLt }) = len
Theorem: insert_sorted_size_eq
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted arr { val := Nat.succ i', isLt := isLt }) = len
Tactic:
simp [insertSorted]
Proof state after:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len
Theorem: insert_sorted_size_eq
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len
Tactic:
split <;> try simp[*]
Proof state after:
no goals
Theorem: insert_sorted_size_eq
Proof state before:
case succ.h_3
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
        { val := i',
          isLt :=
            (_ :
              i' <
                Array.size
                  (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                    { val := Nat.succ i', isLt := isLt })) }) =
    len
Tactic:
simp[*]
Proof state after:
no goals
Theorem: insert_sorted_size_eq'
Proof state before:
α : Type u_1
inst✝ : Ord α
len i : Nat
⊢ ∀ (arr : Array α) (isLt : i < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i, isLt := isLt }) = len
Tactic:
induction i with
| zero =>
  intro arr isLt hLen
  simp [insertSorted', *]
| succ i' ih =>
  intro arr isLt hLen
  simp [insertSorted', dbgTraceIfShared]
  split <;> simp [*]
Proof state after:
no goals
Theorem: insert_sorted_size_eq'
Proof state before:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
⊢ ∀ (arr : Array α) (isLt : Nat.zero < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := Nat.zero, isLt := isLt }) = len
Tactic:
intro arr isLt hLen
Proof state after:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted' arr { val := Nat.zero, isLt := isLt }) = len
Theorem: insert_sorted_size_eq'
Proof state before:
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted' arr { val := Nat.zero, isLt := isLt }) = len
Tactic:
simp [insertSorted', *]
Proof state after:
no goals
Theorem: insert_sorted_size_eq'
Proof state before:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i', isLt := isLt }) = len
⊢ ∀ (arr : Array α) (isLt : Nat.succ i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := Nat.succ i', isLt := isLt }) = len
Tactic:
intro arr isLt hLen
Proof state after:
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted' arr { val := Nat.succ i', isLt := isLt }) = len