internlm/Lean-Github huggingface dataset:
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r
Tactic:
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:
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ 𝓢 ⊢! q ⋎ r ⟶ (p ⋎ q) ⋎ r
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ [] ⊢[𝓢]! q ⋎ r ⟶ (p ⋎ q) ⋎ r
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ [] ⊢[𝓢]! q ⋎ r ⟶ (p ⋎ q) ⋎ r
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ [q ⋎ r] ⊢[𝓢]! (p ⋎ q) ⋎ r
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 𝓢
h : 𝓢 ⊢! p ⋎ q ⋎ r
⊢ [q ⋎ r] ⊢[𝓢]! (p ⋎ q) ⋎ r
Tactic:
exact disj₃'! (implyOrLeft'! $ implyOrRight'! imp_id!) (implyOrRight'! imp_id!) id!
Proof state after:
no goals
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
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
⊢ 𝓢 ⊢! 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 𝓢
h : 𝓢 ⊢! (p ⋎ q) ⋎ r
⊢ 𝓢 ⊢! p ⋎ q ⋎ r
Tactic:
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:
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 ⟶ p ⋎ q ⋎ r
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 𝓢
h : 𝓢 ⊢! (p ⋎ q) ⋎ r
⊢ [] ⊢[𝓢]! p ⋎ q ⟶ p ⋎ q ⋎ r
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 𝓢
h : 𝓢 ⊢! (p ⋎ q) ⋎ r
⊢ [] ⊢[𝓢]! p ⋎ q ⟶ p ⋎ q ⋎ r
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 𝓢
h : 𝓢 ⊢! (p ⋎ q) ⋎ r
⊢ [p ⋎ q] ⊢[𝓢]! p ⋎ q ⋎ r
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 𝓢
h : 𝓢 ⊢! (p ⋎ q) ⋎ r
⊢ [p ⋎ q] ⊢[𝓢]! p ⋎ q ⋎ r
Tactic:
exact disj₃'! (implyOrLeft'! imp_id!) (implyOrRight'! $ implyOrLeft'! imp_id!) id!
Proof state after:
no goals
Theorem: LO.System.and_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:
apply iff_intro!
Proof state after:
case h₁
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 h₂
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.and_assoc!
Proof state before:
case h₁
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 h₂
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:
. apply FiniteContext.deduct'!;
  have hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p := conj₁'! $ conj₁'! id!;
  have hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q := conj₂'! $ conj₁'! id!;
  have hr : [(p ⋏ q) ⋏ r] ⊢[𝓢]! r := conj₂'! id!;
  exact conj₃'! hp (conj₃'! hq hr);
Proof state after:
case h₂
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.and_assoc!
Proof state before:
case h₂
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:
. apply FiniteContext.deduct'!;
  have hp : [p ⋏ (q ⋏ r)] ⊢[𝓢]! p := conj₁'! id!;
  have hq : [p ⋏ (q ⋏ r)] ⊢[𝓢]! q := conj₁'! $ conj₂'! id!;
  have hr : [p ⋏ (q ⋏ r)] ⊢[𝓢]! r := conj₂'! $ conj₂'! id!;
  apply conj₃'!;
  . exact conj₃'! hp hq;
  . exact hr;
Proof state after:
no goals
Theorem: LO.System.and_assoc!
Proof state before:
case h₁
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:
apply FiniteContext.deduct'!
Proof state after:
case h₁.h
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.and_assoc!
Proof state before:
case h₁.h
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:
have hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p := conj₁'! $ conj₁'! id!
Proof state after:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Tactic:
have hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q := conj₂'! $ conj₁'! id!
Proof state after:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Tactic:
have hr : [(p ⋏ q) ⋏ r] ⊢[𝓢]! r := conj₂'! id!
Proof state after:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q
hr : [(p ⋏ q) ⋏ r] ⊢[𝓢]! r
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₁.h
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 𝓢
hp : [(p ⋏ q) ⋏ r] ⊢[𝓢]! p
hq : [(p ⋏ q) ⋏ r] ⊢[𝓢]! q
hr : [(p ⋏ q) ⋏ r] ⊢[𝓢]! r
⊢ [(p ⋏ q) ⋏ r] ⊢[𝓢]! p ⋏ q ⋏ r
Tactic:
exact conj₃'! hp (conj₃'! hq hr)
Proof state after:
no goals
Theorem: LO.System.and_assoc!
Proof state before:
case h₂
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:
apply FiniteContext.deduct'!
Proof state after:
case h₂.h
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.and_assoc!
Proof state before:
case h₂.h
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:
have hp : [p ⋏ (q ⋏ r)] ⊢[𝓢]! p := conj₁'! id!
Proof state after:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Tactic:
have hq : [p ⋏ (q ⋏ r)] ⊢[𝓢]! q := conj₁'! $ conj₂'! id!
Proof state after:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Tactic:
have hr : [p ⋏ (q ⋏ r)] ⊢[𝓢]! r := conj₂'! $ conj₂'! id!
Proof state after:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ [p ⋏ q ⋏ r] ⊢[𝓢]! (p ⋏ q) ⋏ r
Tactic:
apply conj₃'!
Proof state after:
case h₂.h.d₁
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! p ⋏ q

case h₂.h.d₂
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! r
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h.d₁
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! p ⋏ q

case h₂.h.d₂
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! r
Tactic:
. exact conj₃'! hp hq;
Proof state after:
case h₂.h.d₂
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! r
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h.d₂
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! r
Tactic:
. exact hr;
Proof state after:
no goals
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h.d₁
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! p ⋏ q
Tactic:
exact conj₃'! hp hq
Proof state after:
no goals
Theorem: LO.System.and_assoc!
Proof state before:
case h₂.h.d₂
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 𝓢
hp : [p ⋏ q ⋏ r] ⊢[𝓢]! p
hq : [p ⋏ q ⋏ r] ⊢[𝓢]! q
hr : [p ⋏ q ⋏ r] ⊢[𝓢]! r
⊢ { ctx := [p ⋏ q ⋏ r] } ⊢! r
Tactic:
exact hr
Proof state after:
no goals
Theorem: LO.System.cut!
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₁ c q₁ p₂ q₂ : F
d₁ : 𝓢 ⊢! p₁ ⋏ c ⟶ q₁
d₂ : 𝓢 ⊢! p₂ ⟶ c ⋎ q₂
⊢ 𝓢 ⊢! p₁ ⋏ p₂ ⟶ q₁ ⋎ q₂
Tactic:
apply deduct'!
Proof state after:
case h
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₁ c q₁ p₂ q₂ : F
d₁ : 𝓢 ⊢! p₁ ⋏ c ⟶ q₁
d₂ : 𝓢 ⊢! p₂ ⟶ c ⋎ q₂
⊢ [p₁ ⋏ p₂] ⊢[𝓢]! q₁ ⋎ q₂
Theorem: LO.System.cut!
Proof state before:
case h
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₁ c q₁ p₂ q₂ : F
d₁ : 𝓢 ⊢! p₁ ⋏ c ⟶ q₁
d₂ : 𝓢 ⊢! p₂ ⟶ c ⋎ q₂
⊢ [p₁ ⋏ p₂] ⊢[𝓢]! q₁ ⋎ q₂
Tactic:
exact disj₃'! (implyOrLeft'! $ of'! (andImplyIffImplyImply'!.mp d₁) ⨀ (conj₁'! id!)) disj₂! (of'! d₂ ⨀ conj₂'! id!)
Proof state after:
no goals
Theorem: LO.System.id_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 𝓢
he : ∀ g ∈ Γ, g = p
⊢ 𝓢 ⊢! p ⟶ Γ.conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simp_all only [List.conj'_nil, IsEmpty.forall_iff, forall_const]; exact dhyp! $ verum!;
| hsingle => simp_all only [List.mem_singleton, forall_eq, List.conj'_singleton, imp_id!];
| hcons r Γ h ih =>
  simp [List.conj'_cons_nonempty h];
  simp at he;
  have ⟨he₁, he₂⟩ := he;
  subst he₁;
  exact implyRightAnd! imp_id! (ih he₂);
Proof state after:
no goals
Theorem: LO.System.id_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 𝓢
he : ∀ g ∈ [], g = p
⊢ 𝓢 ⊢! p ⟶ [].conj'
Tactic:
simp_all only [List.conj'_nil, IsEmpty.forall_iff, forall_const]
Proof state after:
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 𝓢
he : ∀ g ∈ [], g = p
⊢ 𝓢 ⊢! p ⟶ ⊤
Theorem: LO.System.id_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 𝓢
he : ∀ g ∈ [], g = p
⊢ 𝓢 ⊢! p ⟶ ⊤
Tactic:
exact dhyp! $ verum!
Proof state after:
no goals
Theorem: LO.System.id_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
he : ∀ g ∈ [a✝], g = p
⊢ 𝓢 ⊢! p ⟶ [a✝].conj'
Tactic:
simp_all only [List.mem_singleton, forall_eq, List.conj'_singleton, imp_id!]
Proof state after:
no goals
Theorem: LO.System.id_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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : ∀ g ∈ r :: Γ, g = p
⊢ 𝓢 ⊢! p ⟶ (r :: Γ).conj'
Tactic:
simp [List.conj'_cons_nonempty h]
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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : ∀ g ∈ r :: Γ, g = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Theorem: LO.System.id_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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : ∀ g ∈ r :: Γ, g = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Tactic:
simp at he
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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : r = p ∧ ∀ a ∈ Γ, a = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Theorem: LO.System.id_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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : r = p ∧ ∀ a ∈ Γ, a = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Tactic:
have ⟨he₁, he₂⟩ := he
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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : r = p ∧ ∀ a ∈ Γ, a = p
he₁ : r = p
he₂ : ∀ a ∈ Γ, a = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Theorem: LO.System.id_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 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = p) → 𝓢 ⊢! p ⟶ Γ.conj'
he : r = p ∧ ∀ a ∈ Γ, a = p
he₁ : r = p
he₂ : ∀ a ∈ Γ, a = p
⊢ 𝓢 ⊢! p ⟶ r ⋏ Γ.conj'
Tactic:
subst he₁
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 𝓢
q r✝ : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = r) → 𝓢 ⊢! r ⟶ Γ.conj'
he : r = r ∧ ∀ a ∈ Γ, a = r
he₂ : ∀ a ∈ Γ, a = r
⊢ 𝓢 ⊢! r ⟶ r ⋏ Γ.conj'
Theorem: LO.System.id_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 𝓢
q r✝ : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
r : F
Γ : List F
h : Γ ≠ []
ih : (∀ g ∈ Γ, g = r) → 𝓢 ⊢! r ⟶ Γ.conj'
he : r = r ∧ ∀ a ∈ Γ, a = r
he₂ : ∀ a ∈ Γ, a = r
⊢ 𝓢 ⊢! r ⟶ r ⋏ Γ.conj'
Tactic:
exact implyRightAnd! imp_id! (ih he₂)
Proof state after:
no goals
Theorem: LO.System.implyLeft_cons_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 𝓢
⊢ 𝓢 ⊢! (p :: Γ).conj' ⟶ q ↔ 𝓢 ⊢! p ⋏ Γ.conj' ⟶ q
Tactic:
induction Γ with
| nil =>
  simp [andImplyIffImplyImply'!];
  constructor;
  . intro h; apply imp_swap'!; exact dhyp! h;
  . intro h; exact imp_swap'! h ⨀ verum!;
| cons q ih => simp;
Proof state after:
no goals
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
case nil
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].conj' ⟶ q ↔ 𝓢 ⊢! p ⋏ [].conj' ⟶ q
Tactic:
simp [andImplyIffImplyImply'!]
Proof state after:
case nil
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 ↔ 𝓢 ⊢! p ⟶ ⊤ ⟶ q
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
case nil
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 ↔ 𝓢 ⊢! p ⟶ ⊤ ⟶ q
Tactic:
constructor
Proof state after:
case nil.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 → 𝓢 ⊢! p ⟶ ⊤ ⟶ q

case nil.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 → 𝓢 ⊢! p ⟶ q