internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Kripke.iff_definability_memAxiomSetFiniteFrameClass
Proof state before:
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
P : FiniteFrameProperty
definability : FiniteDefinability Ax P
⊢ ∀ {F : FiniteFrame' α}, F ∈ 𝔽ꟳ(Ax) ↔ P F
Tactic:
apply definability.defines
Proof state after:
no goals
Theorem: LO.System.efq_of_neg!
Proof state before:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
apply provable_iff_provable.mpr
Proof state after:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
⊢ [] ⊢[𝓢]! p ⟶ q
Theorem: LO.System.efq_of_neg!
Proof state before:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
⊢ [] ⊢[𝓢]! p ⟶ q
Tactic:
apply deduct_iff.mpr
Proof state after:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
⊢ [p] ⊢[𝓢]! q
Theorem: LO.System.efq_of_neg!
Proof state before:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
⊢ [p] ⊢[𝓢]! q
Tactic:
have dnp : [p] ⊢[𝓢]! p ⟶ ⊥ := of'! $ neg_equiv'!.mp h
Proof state after:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
dnp : [p] ⊢[𝓢]! p ⟶ ⊥
⊢ [p] ⊢[𝓢]! q
Theorem: LO.System.efq_of_neg!
Proof state before:
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! ~p
dnp : [p] ⊢[𝓢]! p ⟶ ⊥
⊢ [p] ⊢[𝓢]! q
Tactic:
exact efq'! (dnp ⨀ FiniteContext.id!)
Proof state after:
no goals
Theorem: LO.System.implyLeftReplaceIff'!
Proof state before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! p ⟶ r ↔ 𝓢 ⊢! q ⟶ r
Tactic:
constructor
Proof state after:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! p ⟶ r → 𝓢 ⊢! q ⟶ r

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Theorem: LO.System.implyLeftReplaceIff'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! p ⟶ r → 𝓢 ⊢! q ⟶ r

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Tactic:
. exact imp_trans! $ conj₂'! h;
Proof state after:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Theorem: LO.System.implyLeftReplaceIff'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Tactic:
. exact imp_trans! $ conj₁'! h;
Proof state after:
no goals
Theorem: LO.System.implyLeftReplaceIff'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! p ⟶ r → 𝓢 ⊢! q ⟶ r
Tactic:
exact imp_trans! $ conj₂'! h
Proof state after:
no goals
Theorem: LO.System.implyLeftReplaceIff'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! q ⟶ r → 𝓢 ⊢! p ⟶ r
Tactic:
exact imp_trans! $ conj₁'! h
Proof state after:
no goals
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ p ↔ 𝓢 ⊢! r ⟶ q
Tactic:
constructor
Proof state after:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ p → 𝓢 ⊢! r ⟶ q

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ q → 𝓢 ⊢! r ⟶ p
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ p → 𝓢 ⊢! r ⟶ q

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ q → 𝓢 ⊢! r ⟶ p
Tactic:
. intro hrp; exact imp_trans! hrp $ conj₁'! h;
Proof state after:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ q → 𝓢 ⊢! r ⟶ p
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ q → 𝓢 ⊢! r ⟶ p
Tactic:
. intro hrq; exact imp_trans! hrq $ conj₂'! h;
Proof state after:
no goals
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ p → 𝓢 ⊢! r ⟶ q
Tactic:
intro hrp
Proof state after:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
hrp : 𝓢 ⊢! r ⟶ p
⊢ 𝓢 ⊢! r ⟶ q
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
hrp : 𝓢 ⊢! r ⟶ p
⊢ 𝓢 ⊢! r ⟶ q
Tactic:
exact imp_trans! hrp $ conj₁'! h
Proof state after:
no goals
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
⊢ 𝓢 ⊢! r ⟶ q → 𝓢 ⊢! r ⟶ p
Tactic:
intro hrq
Proof state after:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
hrq : 𝓢 ⊢! r ⟶ q
⊢ 𝓢 ⊢! r ⟶ p
Theorem: LO.System.implyRightReplaceIff'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⟷ q
hrq : 𝓢 ⊢! r ⟶ q
⊢ 𝓢 ⊢! r ⟶ p
Tactic:
exact imp_trans! hrq $ conj₂'! h
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
Γ : List F
⊢ 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle => simp;
| hcons p Γ hΓ ih =>
  simp_all;
  constructor;
  . intro h;
    constructor;
    . exact conj₁'! h;
    . exact ih.mp (conj₂'! h);
  . rintro ⟨h₁, h₂⟩;
    exact conj₃'! h₁ (ih.mpr h₂);
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hnil
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! [].conj' ↔ ∀ p ∈ [], 𝓢 ⊢! p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
⊢ 𝓢 ⊢! [a✝].conj' ↔ ∀ p ∈ [a✝], 𝓢 ⊢! p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : Γ ≠ []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! (p :: Γ).conj' ↔ ∀ p_1 ∈ p :: Γ, 𝓢 ⊢! p_1
Tactic:
simp_all
Proof state after:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' ↔ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' ↔ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
constructor
Proof state after:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
. intro h;
  constructor;
  . exact conj₁'! h;
  . exact ih.mp (conj₂'! h);
Proof state after:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
. rintro ⟨h₁, h₂⟩;
  exact conj₃'! h₁ (ih.mpr h₂);
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
intro h
Proof state after:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
constructor
Proof state after:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p

case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p

case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
. exact conj₁'! h;
Proof state after:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
. exact ih.mp (conj₂'! h);
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p
Tactic:
exact conj₁'! h
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
exact ih.mp (conj₂'! h)
Proof state after:
no goals
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case hcons.mpr.intro
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h₁ : 𝓢 ⊢! p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! a
⊢ 𝓢 ⊢! p ⋏ Γ.conj'
Theorem: LO.System.iff_provable_list_conj
Proof state before:
case hcons.mpr.intro
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h₁ : 𝓢 ⊢! p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! a
⊢ 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
exact conj₃'! h₁ (ih.mpr h₂)
Proof state after:
no goals
Theorem: LO.System.conj'conj'_subset
Proof state before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : ∀ p ∈ Γ, p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! verum!;
| hsingle => simp_all; exact generalConj'! h;
| hcons p Γ hne ih => simp_all; exact implyRightAnd! (generalConj'! h.1) ih;
Proof state after:
no goals
Theorem: LO.System.conj'conj'_subset
Proof state before:
case hnil
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : ∀ p ∈ [], p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ [].conj'
Tactic:
simpa using dhyp! verum!
Proof state after:
no goals
Theorem: LO.System.conj'conj'_subset
Proof state before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : ∀ p ∈ [a✝], p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ [a✝].conj'
Tactic:
simp_all
Proof state after:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : a✝ ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ a✝
Theorem: LO.System.conj'conj'_subset
Proof state before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : a✝ ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ a✝
Tactic:
exact generalConj'! h
Proof state after:
no goals
Theorem: LO.System.conj'conj'_subset
Proof state before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : Γ ≠ []
ih : (∀ p ∈ Γ, p ∈ Δ) → 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : ∀ p_1 ∈ p :: Γ, p_1 ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ (p :: Γ).conj'
Tactic:
simp_all
Proof state after:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : ¬Γ = []
ih : 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : p ∈ Δ ∧ ∀ a ∈ Γ, a ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ p ⋏ Γ.conj'
Theorem: LO.System.conj'conj'_subset
Proof state before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : ¬Γ = []
ih : 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : p ∈ Δ ∧ ∀ a ∈ Γ, a ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ p ⋏ Γ.conj'
Tactic:
exact implyRightAnd! (generalConj'! h.1) ih
Proof state after:
no goals
Theorem: LO.System.or_assoc'!
Proof state before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! p ⋎ q ⋎ r ↔ 𝓢 ⊢! (p ⋎ q) ⋎ r
Tactic:
constructor
Proof state after:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! p ⋎ q ⋎ r → 𝓢 ⊢! (p ⋎ q) ⋎ r

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r → 𝓢 ⊢! p ⋎ q ⋎ r
Theorem: LO.System.or_assoc'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! p ⋎ q ⋎ r → 𝓢 ⊢! (p ⋎ q) ⋎ r

case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r → 𝓢 ⊢! p ⋎ q ⋎ r
Tactic:
. intro h;
  exact disj₃'!
    (implyOrLeft'! $ implyOrLeft'! imp_id!)
    (by
      apply provable_iff_provable.mpr;
      apply deduct_iff.mpr;
      exact disj₃'! (implyOrLeft'! $ implyOrRight'! imp_id!) (implyOrRight'! imp_id!) id!;
    )
    h;
Proof state after:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r → 𝓢 ⊢! p ⋎ q ⋎ r
Theorem: LO.System.or_assoc'!
Proof state before:
case mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r → 𝓢 ⊢! p ⋎ q ⋎ r
Tactic:
. intro h;
  exact disj₃'!
    (by
      apply provable_iff_provable.mpr;
      apply deduct_iff.mpr;
      exact disj₃'! (implyOrLeft'! imp_id!) (implyOrRight'! $ implyOrLeft'! imp_id!) id!;
    )
    (implyOrRight'! $ implyOrRight'! imp_id!)
    h;
Proof state after:
no goals
Theorem: LO.System.or_assoc'!
Proof state before:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! p ⋎ q ⋎ r → 𝓢 ⊢! (p ⋎ q) ⋎ r
Tactic:
intro h
Proof state after:
case mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r