Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_multiGeachAxiom (Logic/Modal/Standard/Kripke/Geach/Completeness.lean)

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;
State after:
no goals

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]
State after:
no goals

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
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)

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
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)

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)
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)

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;
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
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)

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
State after:
no goals