internlm/Lean-Github huggingface dataset:
Theorem: LO.System.iff_concat_conj'!
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 𝓢
⊢ 𝓢 ⊢! Γ.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₂;
Proof state after:
no goals
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'
Tactic:
intro h
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 𝓢
h : 𝓢 ⊢! (Γ ++ Δ).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 𝓢
h : 𝓢 ⊢! (Γ ++ Δ).conj'
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
Tactic:
replace h := iff_provable_list_conj.mp h
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
Tactic:
apply conj₃'!
Proof 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'
Theorem: LO.System.iff_concat_conj'!
Proof 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);
Proof 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'
Theorem: LO.System.iff_concat_conj'!
Proof 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);
Proof state after:
no goals
Theorem: LO.System.iff_concat_conj'!
Proof 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
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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)
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ++ Δ
Tactic:
simp only [List.mem_append]
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 ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ ∨ p ∈ Δ
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ
Theorem: LO.System.iff_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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Γ
⊢ p ∈ Γ
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.System.iff_concat_conj'!
Proof 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
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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)
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ++ Δ
Tactic:
simp only [List.mem_append]
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 ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Γ ∨ p ∈ Δ
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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! 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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Δ
Theorem: LO.System.iff_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 𝓢
h : ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
p : F
hp : p ∈ Δ
⊢ p ∈ Δ
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.System.iff_concat_conj'!
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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' → 𝓢 ⊢! (Γ ++ Δ).conj'
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ 𝓢 ⊢! (Γ ++ Δ).conj'
Theorem: LO.System.iff_concat_conj'!
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ 𝓢 ⊢! (Γ ++ Δ).conj'
Tactic:
apply iff_provable_list_conj.mpr
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
Theorem: LO.System.iff_concat_conj'!
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ p ∈ Γ ++ Δ, 𝓢 ⊢! p
Tactic:
simp only [List.mem_append]
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ (p : F), p ∈ Γ ∨ p ∈ Δ → 𝓢 ⊢! p
Theorem: LO.System.iff_concat_conj'!
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 : 𝓢 ⊢! Γ.conj' ⋏ Δ.conj'
⊢ ∀ (p : F), p ∈ Γ ∨ p ∈ Δ → 𝓢 ⊢! p
Tactic:
rintro p (hp₁ | hp₂)
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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₁;
Proof 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
Theorem: LO.System.iff_concat_conj'!
Proof 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₂;
Proof state after:
no goals
Theorem: LO.System.iff_concat_conj'!
Proof 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₁
Proof state after:
no goals
Theorem: LO.System.iff_concat_conj'!
Proof 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₂
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:
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 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).conj' ⟶ Γ.conj' ⋏ Δ.conj'

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

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:
. apply deduct'!; apply iff_concat_conj'!.mp; exact 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 𝓢
⊢ 𝓢 ⊢! Γ.conj' ⋏ Δ.conj' ⟶ (Γ ++ Δ).conj'
Theorem: LO.System.iff_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:
. apply deduct'!; apply iff_concat_conj'!.mpr; exact id!;
Proof state after:
no goals
Theorem: LO.System.iff_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:
apply 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 𝓢
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Theorem: LO.System.iff_concat_conj!
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 𝓢
⊢ [(Γ ++ Δ).conj'] ⊢[𝓢]! Γ.conj' ⋏ Δ.conj'
Tactic:
apply iff_concat_conj'!.mp
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 𝓢
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! (Γ ++ Δ).conj'
Theorem: LO.System.iff_concat_conj!
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 𝓢
⊢ { ctx := [(Γ ++ Δ).conj'] } ⊢! (Γ ++ Δ).conj'
Tactic:
exact id!
Proof state after:
no goals
Theorem: LO.System.iff_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:
apply 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 𝓢
⊢ [Γ.conj' ⋏ Δ.conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
Theorem: LO.System.iff_concat_conj!
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 𝓢
⊢ [Γ.conj' ⋏ Δ.conj'] ⊢[𝓢]! (Γ ++ Δ).conj'
Tactic:
apply iff_concat_conj'!.mpr
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 𝓢
⊢ { ctx := [Γ.conj' ⋏ Δ.conj'] } ⊢! Γ.conj' ⋏ Δ.conj'
Theorem: LO.System.iff_concat_conj!
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 𝓢
⊢ { ctx := [Γ.conj' ⋏ Δ.conj'] } ⊢! Γ.conj' ⋏ Δ.conj'
Tactic:
exact id!
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 𝓢
⊢ 𝓢 ⊢! 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.or_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:
. exact deduct'! $ or_assoc'!.mp 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 𝓢
⊢ 𝓢 ⊢! (p ⋎ q) ⋎ r ⟶ p ⋎ q ⋎ r
Theorem: LO.System.or_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:
. exact deduct'! $ or_assoc'!.mpr id!;
Proof state after:
no goals
Theorem: LO.System.or_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:
exact deduct'! $ or_assoc'!.mp id!
Proof state after:
no goals
Theorem: LO.System.or_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:
exact deduct'! $ or_assoc'!.mpr id!
Proof state after:
no goals
Theorem: LO.System.or_replace_right_iff!
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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟷ p ⋎ 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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ p ⋎ 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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ r ⟶ p ⋎ q
Theorem: LO.System.or_replace_right_iff!
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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ p ⋎ 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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ r ⟶ p ⋎ q
Tactic:
. apply or_replace_right!; exact conj₁'! d;
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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ r ⟶ p ⋎ q
Theorem: LO.System.or_replace_right_iff!
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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ r ⟶ p ⋎ q
Tactic:
. apply or_replace_right!; exact conj₂'! d;
Proof state after:
no goals
Theorem: LO.System.or_replace_right_iff!
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 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ p ⋎ r
Tactic:
apply or_replace_right!
Proof state after:
case h₁.hq
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
d : 𝓢 ⊢! q ⟷ r
⊢ 𝓢 ⊢! q ⟶ r