Theorem: LO.System.iff_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:
constructor
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'

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

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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'
Tactic:
. intro h;
  apply iff_provable_list_conj.mpr;
  simp only [List.mem_append];
  rintro p (hp₁ | hp₂);
  . exact (iff_provable_list_conj.mp $ conj₁'! h) p hp₁;
  . exact (iff_provable_list_conj.mp $ conj₂'! h) p hp₂;
State after:
no goals

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'
Tactic:
intro h
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 : 𝓢 ⊢! (Γ ++ Δ).conj'
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'

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 : 𝓢 ⊢! (Γ ++ Δ).conj'
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
Tactic:
replace h := iff_provable_list_conj.mp h
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 ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'

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 ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
Tactic:
apply conj₃'!
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj'

case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Δ.conj'

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj'

case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Δ.conj'
Tactic:
. apply iff_provable_list_conj.mpr;
  intro p hp; exact h p (by simp only [List.mem_append]; left; simpa);
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Δ.conj'

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Δ.conj'
Tactic:
. apply iff_provable_list_conj.mpr;
  intro p hp; exact h p (by simp only [List.mem_append]; right; simpa);
State after:
no goals

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj'
Tactic:
apply iff_provable_list_conj.mpr
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ ∀ p ∈ Γ, 𝓢 ⊢! p

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ ∀ p ∈ Γ, 𝓢 ⊢! p
Tactic:
intro p hp
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! p

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! p
Tactic:
exact h p (by simp only [List.mem_append]; left; simpa)
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ++ Δ
Tactic:
simp only [List.mem_append]
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 ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ
Tactic:
simpa
State after:
no goals

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Δ.conj'
Tactic:
apply iff_provable_list_conj.mpr
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ ∀ p ∈ Δ, 𝓢 ⊢! p

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ ∀ p ∈ Δ, 𝓢 ⊢! p
Tactic:
intro p hp
State after:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ 𝓢 ⊢! p

State before:
case mp.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ 𝓢 ⊢! p
Tactic:
exact h p (by simp only [List.mem_append]; right; simpa)
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ++ Δ
Tactic:
simp only [List.mem_append]
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 ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Δ
Tactic:
simpa
State after:
no goals

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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'
Tactic:
intro h
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ 𝓢 ⊢! (Γ ++ Δ).conj'

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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ 𝓢 ⊢! (Γ ++ Δ).conj'
Tactic:
apply iff_provable_list_conj.mpr
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p

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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
Tactic:
simp only [List.mem_append]
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ (p : F), p ∈ Γ ∨ p ∈ Δ → 𝓢 ⊢! p

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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ (p : F), p ∈ Γ ∨ p ∈ Δ → 𝓢 ⊢! p
Tactic:
rintro p (hp₁ | hp₂)
State after:
case mpr.inl
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₁ : p ∈ Γ
⊢ 𝓢 ⊢! p

case mpr.inr
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₂ : p ∈ Δ
⊢ 𝓢 ⊢! p

State before:
case mpr.inl
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₁ : p ∈ Γ
⊢ 𝓢 ⊢! p

case mpr.inr
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₂ : p ∈ Δ
⊢ 𝓢 ⊢! p
Tactic:
. exact (iff_provable_list_conj.mp $ conj₁'! h) p hp₁;
State after:
case mpr.inr
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₂ : p ∈ Δ
⊢ 𝓢 ⊢! p

State before:
case mpr.inr
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₂ : p ∈ Δ
⊢ 𝓢 ⊢! p
Tactic:
. exact (iff_provable_list_conj.mp $ conj₂'! h) p hp₂;
State after:
no goals

State before:
case mpr.inl
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₁ : p ∈ Γ
⊢ 𝓢 ⊢! p
Tactic:
exact (iff_provable_list_conj.mp $ conj₁'! h) p hp₁
State after:
no goals

State before:
case mpr.inr
F : Type u_1
inst✝⁴ : LogicalConnective 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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
p : F
hp₂ : p ∈ Δ
⊢ 𝓢 ⊢! p
Tactic:
exact (iff_provable_list_conj.mp $ conj₂'! h) p hp₂
State after:
no goals