Theorem: LO.System.imply_left_concat_conj'! (Logic/Logic/HilbertStyle/Supplemental.lean)

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'!
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'

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!
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'

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

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₃'!
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'

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

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

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

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

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

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
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 ∈ Δ

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
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 ∈ Γ

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

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

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

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

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
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 ∈ Δ

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
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 ∈ Δ

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