Theorem: LO.System.and_assoc! (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 𝓢
⊢ 𝓢 ⊢! (p ⋏ q) ⋏ r ⟷ p ⋏ q ⋏ r
Tactic:
apply iff_intro!
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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