internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
use M.Valuation, w
Proof state after:
no goals
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
⊢ i𝓓 ⊢! p ⋎ q → i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
intro hpq
Proof state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
have : m𝓓 ⊢! □pᵍ ⋎ □qᵍ := disj₃'! (implyOrLeft'! axiomTc_GTranslate!) (implyOrRight'! axiomTc_GTranslate!) (by simpa using ModalCompanion.companion.mp hpq)
Proof state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
cases ModalDisjunctive.modal_disjunctive this with
| inl h => left; exact ModalCompanion.companion.mpr h;
| inr h => right; exact ModalCompanion.companion.mpr h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ
Tactic:
simpa using ModalCompanion.companion.mp hpq
Proof state after:
no goals
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
case inl.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! pᵍ
⊢ i𝓓 ⊢! p
Tactic:
exact ModalCompanion.companion.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
Tactic:
right
Proof state after:
case inr.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! q
Theorem: LO.Modal.Standard.dp_of_mdp
Proof state before:
case inr.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! q
Tactic:
exact ModalCompanion.companion.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.T_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 0, j := 0, m := 1, n := 0 }) = 𝗧
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.B_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 0, j := 1, m := 0, n := 1 }) = 𝗕
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.D_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 0, j := 0, m := 1, n := 1 }) = 𝗗
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.Four_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 0, j := 2, m := 1, n := 0 }) = 𝟰
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.Five_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 1, j := 1, m := 0, n := 1 }) = 𝟱
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.Dot2_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 1, j := 1, m := 1, n := 1 }) = .𝟮
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.C4_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 0, j := 1, m := 2, n := 0 }) = 𝗖𝟰
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Geach.CD_def
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗴𝗲({ i := 1, j := 1, m := 0, n := 0 }) = 𝗖𝗗
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.def_nil
Proof state before:
α : Type u_1
Ax : AxiomSet α
⊢ 𝗚𝗲([]) = 𝗞
Tactic:
simp [MultiGeach]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.iff_cons
Proof state before:
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
l : List Axioms.Geach.Taple
⊢ 𝗚𝗲(x :: l) = 𝗴𝗲(x) ∪ 𝗚𝗲(l)
Tactic:
simp only [MultiGeach]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK
Proof state before:
α : Type u_1
Ax : AxiomSet α
l : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗚𝗲(l)
Tactic:
induction l with
| nil => simp;
| cons => simp; apply Set.subset_union_of_subset_right (by assumption);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK
Proof state before:
case nil
α : Type u_1
Ax : AxiomSet α
⊢ 𝗞 ⊆ 𝗚𝗲([])
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK
Proof state before:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
simp
Proof state after:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK
Proof state before:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)
Tactic:
apply Set.subset_union_of_subset_right (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗚𝗲(tail✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
l : List Axioms.Geach.Taple
h : x ∈ l
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(l)
Tactic:
induction l with
| nil => contradiction;
| cons a as ih =>
  simp_all;
  cases h;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ ih (by assumption);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case nil
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
h : x ∈ []
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲([])
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x ∈ a :: as
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(a :: as)
Tactic:
simp_all
Proof state after:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x = a ∨ x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x = a ∨ x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
cases h
Proof state after:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
. subst_vars; tauto;
Proof state after:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
. apply Set.subset_union_of_subset_right $ ih (by assumption);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
subst_vars
Proof state after:
case cons.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : a ∈ as → 𝗴𝗲(a) ⊆ 𝗚𝗲(as)
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : a ∈ as → 𝗴𝗲(a) ⊆ 𝗚𝗲(as)
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
apply Set.subset_union_of_subset_right $ ih (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.mem
Proof state before:
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ x ∈ as
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
l₁ l₂ : List Axioms.Geach.Taple
h : l₁ ⊆ l₂
⊢ 𝗚𝗲(l₁) ⊆ 𝗚𝗲(l₂)
Tactic:
induction l₁ generalizing l₂ <;> induction l₂
Proof state after:
case nil.nil
α : Type u_1
Ax : AxiomSet α
h : [] ⊆ []
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲([])

case nil.cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)

case cons.nil
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])

case cons.cons
α : Type u_1
Ax : AxiomSet α
head✝¹ : Axioms.Geach.Taple
tail✝¹ : List Axioms.Geach.Taple
tail_ih✝¹ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝¹ ⊆ l₂ → 𝗚𝗲(tail✝¹) ⊆ 𝗚𝗲(l₂)
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : head✝¹ :: tail✝¹ ⊆ tail✝ → 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(tail✝)
h : head✝¹ :: tail✝¹ ⊆ head✝ :: tail✝
⊢ 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(head✝ :: tail✝)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])
Tactic:
case nil.nil | cons.nil => simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
case nil.cons => simp_all; apply Set.subset_union_of_subset_right (by simp);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a :: as ⊆ bs → 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(bs)
h : a :: as ⊆ b :: bs
⊢ 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(b :: bs)
Tactic:
case cons.cons a as iha b bs ihb =>
  simp_all;
  constructor;
  . cases h.1;
    . subst_vars; tauto;
    . apply Set.subset_union_of_subset_right $ mem (by assumption);
  . simpa using (iha h.2);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
simp_all
Proof state after:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)
Tactic:
apply Set.subset_union_of_subset_right (by simp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗚𝗲(tail✝)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a :: as ⊆ bs → 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(bs)
h : a :: as ⊆ b :: bs
⊢ 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(b :: bs)
Tactic:
simp_all
Proof state after:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs) ∧ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs) ∧ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
constructor
Proof state after:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. cases h.1;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ mem (by assumption);
Proof state after:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. simpa using (iha h.2);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
cases h.1
Proof state after:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. subst_vars; tauto;
Proof state after:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. apply Set.subset_union_of_subset_right $ mem (by assumption);
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
subst_vars
Proof state after:
case left.inl
α : Type u_1
Ax : AxiomSet α
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : b ∈ bs → as ⊆ bs → 𝗴𝗲(b) ⊆ 𝗚𝗲(bs)
h : (b = b ∨ b ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(b) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left.inl
α : Type u_1
Ax : AxiomSet α
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : b ∈ bs → as ⊆ bs → 𝗴𝗲(b) ⊆ 𝗚𝗲(bs)
h : (b = b ∨ b ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(b) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
tauto
Proof state after:
no goals