internlm/Lean-Github huggingface dataset:
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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
Tactic:
. intro h; apply imp_swap'!; exact dhyp! h;
Proof state after:
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
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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
Tactic:
. intro h; exact imp_swap'! h ⨀ verum!;
Proof state after:
no goals
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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
Tactic:
intro h
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 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! p ⟶ ⊤ ⟶ q
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! p ⟶ ⊤ ⟶ q
Tactic:
apply imp_swap'!
Proof state after:
case nil.mp.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 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! ⊤ ⟶ p ⟶ q
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
case nil.mp.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 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! ⊤ ⟶ p ⟶ q
Tactic:
exact dhyp! h
Proof state after:
no goals
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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
Tactic:
intro h
Proof state after:
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 𝓢
h : 𝓢 ⊢! p ⟶ ⊤ ⟶ q
⊢ 𝓢 ⊢! p ⟶ q
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
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 𝓢
h : 𝓢 ⊢! p ⟶ ⊤ ⟶ q
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
exact imp_swap'! h ⨀ verum!
Proof state after:
no goals
Theorem: LO.System.implyLeft_cons_conj'!
Proof state before:
case cons
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 𝓢
q : F
ih : List F
tail_ih✝ : 𝓢 ⊢! (p :: ih).conj' ⟶ q✝ ↔ 𝓢 ⊢! p ⋏ ih.conj' ⟶ q✝
⊢ 𝓢 ⊢! (p :: q :: ih).conj' ⟶ q✝ ↔ 𝓢 ⊢! p ⋏ (q :: ih).conj' ⟶ q✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.imply_left_concat_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 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).conj' ⟶ Γ.conj' ⋏ Δ.conj'
Tactic:
apply FiniteContext.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 𝓢
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Theorem: LO.System.imply_left_concat_conj'!
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 𝓢
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Tactic:
have : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj' := id!
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Theorem: LO.System.imply_left_concat_conj'!
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Tactic:
have d := iff_provable_list_conj.mp this
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Theorem: LO.System.imply_left_concat_conj'!
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Tactic:
apply conj₃'!
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Γ.conj'

case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Δ.conj'
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Γ.conj'

case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Δ.conj'
Tactic:
. apply iff_provable_list_conj.mpr;
  intro p hp;
  exact d p (by simp; left; exact hp);
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Δ.conj'
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Δ.conj'
Tactic:
. apply iff_provable_list_conj.mpr;
  intro p hp;
  exact d p (by simp; right; exact hp);
Proof state after:
no goals
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Γ.conj'
Tactic:
apply iff_provable_list_conj.mpr
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ ∀ p ∈ Γ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ ∀ p ∈ Γ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Tactic:
intro p hp
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Tactic:
exact d p (by simp; left; exact hp)
Proof state after:
no goals
Theorem: LO.System.imply_left_concat_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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ++ Δ
Tactic:
simp
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ∨ p ∈ Δ
Theorem: LO.System.imply_left_concat_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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ∨ p ∈ Δ
Tactic:
left
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ
Theorem: LO.System.imply_left_concat_conj'!
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ
Tactic:
exact hp
Proof state after:
no goals
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! Δ.conj'
Tactic:
apply iff_provable_list_conj.mpr
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ ∀ p ∈ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
⊢ ∀ p ∈ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Tactic:
intro p hp
Proof state after:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Theorem: LO.System.imply_left_concat_conj'!
Proof state before:
case 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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! p
Tactic:
exact d p (by simp; right; exact hp)
Proof state after:
no goals
Theorem: LO.System.imply_left_concat_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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ++ Δ
Tactic:
simp
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ∨ p ∈ Δ
Theorem: LO.System.imply_left_concat_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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ∨ p ∈ Δ
Tactic:
right
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Δ
Theorem: LO.System.imply_left_concat_conj'!
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 𝓢
this : [(Γ ++ Δ).conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
d : ∀ p ∈ Γ ++ Δ, { ctx := [(Γ ++ Δ).conj'] } ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Δ
Tactic:
exact hp
Proof state after:
no goals
Theorem: LO.System.forthbackConjRemove
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.remove p Γ).conj' ⋏ p ⟶ Γ.conj'
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 𝓢
⊢ [(List.remove p Γ).conj' ⋏ p] ⊢[𝓢]! Γ.conj'
Theorem: LO.System.forthbackConjRemove
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 𝓢
⊢ [(List.remove p Γ).conj' ⋏ p] ⊢[𝓢]! Γ.conj'
Tactic:
apply iff_provable_list_conj.mpr
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_1 ∈ Γ, { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! p_1
Theorem: LO.System.forthbackConjRemove
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_1 ∈ Γ, { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! p_1
Tactic:
intro q hq
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 𝓢
q : F
hq : q ∈ Γ
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Theorem: LO.System.forthbackConjRemove
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 𝓢
q : F
hq : q ∈ Γ
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Tactic:
by_cases e : q = p
Proof state after:
case pos
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 𝓢
q : F
hq : q ∈ Γ
e : q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q

case neg
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Theorem: LO.System.forthbackConjRemove
Proof state before:
case pos
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 𝓢
q : F
hq : q ∈ Γ
e : q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q

case neg
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Tactic:
. subst e; exact conj₂'! id!;
Proof state after:
case neg
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Theorem: LO.System.forthbackConjRemove
Proof state before:
case neg
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Tactic:
. exact iff_provable_list_conj.mp (conj₁'! id!) q (by apply List.mem_remove_iff.mpr; simp_all);
Proof state after:
no goals
Theorem: LO.System.forthbackConjRemove
Proof state before:
case pos
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 𝓢
q : F
hq : q ∈ Γ
e : q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Tactic:
subst e
Proof state after:
case pos
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 𝓢
q : F
hq : q ∈ Γ
⊢ { ctx := [(List.remove q Γ).conj' ⋏ q] } ⊢! q
Theorem: LO.System.forthbackConjRemove
Proof state before:
case pos
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 𝓢
q : F
hq : q ∈ Γ
⊢ { ctx := [(List.remove q Γ).conj' ⋏ q] } ⊢! q
Tactic:
exact conj₂'! id!
Proof state after:
no goals
Theorem: LO.System.forthbackConjRemove
Proof state before:
case neg
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ { ctx := [(List.remove p Γ).conj' ⋏ p] } ⊢! q
Tactic:
exact iff_provable_list_conj.mp (conj₁'! id!) q (by apply List.mem_remove_iff.mpr; simp_all)
Proof state after:
no goals
Theorem: LO.System.forthbackConjRemove
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ q ∈ List.remove p Γ
Tactic:
apply List.mem_remove_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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ q ∈ Γ ∧ q ≠ p
Theorem: LO.System.forthbackConjRemove
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 𝓢
q : F
hq : q ∈ Γ
e : ¬q = p
⊢ q ∈ Γ ∧ q ≠ p
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.System.iff_concat_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 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).conj' ↔ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
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 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).conj' → 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'

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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'
Theorem: LO.System.iff_concat_conj'!
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 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).conj' → 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'

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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'
Tactic:
. intro h;
  replace h := iff_provable_list_conj.mp h;
  apply conj₃'!;
  . apply iff_provable_list_conj.mpr;
    intro p hp; exact h p (by simp only [List.mem_append]; left; simpa);
  . apply iff_provable_list_conj.mpr;
    intro p hp; exact h p (by simp only [List.mem_append]; right; simpa);
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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'