internlm/Lean-Github huggingface dataset:
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟷ ⊥ ⋎ (a✝² :: as✝).disj'
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟶ ⊥ ⋎ (a✝² :: as✝).disj'

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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ⊥ ⋎ (a✝² :: as✝).disj' ⟶ (a✝² :: as✝).disj'
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟶ ⊥ ⋎ (a✝² :: as✝).disj'

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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ⊥ ⋎ (a✝² :: as✝).disj' ⟶ (a✝² :: as✝).disj'
Tactic:
. simp;
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ⊥ ⋎ (a✝² :: as✝).disj' ⟶ (a✝² :: as✝).disj'
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ⊥ ⋎ (a✝² :: as✝).disj' ⟶ (a✝² :: as✝).disj'
Tactic:
. exact disj₃''! efq! imp_id!;
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟶ ⊥ ⋎ (a✝² :: as✝).disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ⊥ ⋎ (a✝² :: as✝).disj' ⟶ (a✝² :: as✝).disj'
Tactic:
exact disj₃''! efq! imp_id!
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝¹ a✝ : F
⊢ 𝓢 ⊢! ([a✝¹] ++ [a✝]).disj' ⟷ [a✝¹].disj' ⋎ [a✝].disj'
Tactic:
simp only [List.singleton_append, ne_eq, not_false_eq_true, List.disj'_cons_nonempty, List.disj'_singleton, iff_id!]
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝³ a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([a✝³] ++ as✝).disj' ⟷ [a✝³].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ([a✝³] ++ a✝² :: as✝).disj' ⟷ [a✝³].disj' ⋎ (a✝² :: as✝).disj'
Tactic:
simp only [List.singleton_append, ne_eq, not_false_eq_true, List.disj'_cons_nonempty, List.disj'_singleton, iff_id!]
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
hps : ps ≠ []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
q : F
⊢ 𝓢 ⊢! (p :: ps ++ [q]).disj' ⟷ (p :: ps).disj' ⋎ [q].disj'
Tactic:
simp_all
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ [q]).disj' ⟷ (p ⋎ ps.disj') ⋎ q
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ [q]).disj' ⟷ (p ⋎ ps.disj') ⋎ q
Tactic:
apply iff_trans! (by
  apply or_replace_right_iff!;
  simpa using @ihp [q];
) or_assoc!
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ [q]).disj' ⟷ p ⋎ ps.disj' ⋎ q
Tactic:
apply or_replace_right_iff!
Proof state after:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (ps ++ [q]).disj' ⟷ ps.disj' ⋎ q
Theorem: LO.System.iff_concact_disj!
Proof state before:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (ps ++ [q]).disj' ⟷ ps.disj' ⋎ q
Tactic:
simpa using @ihp [q]
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
hps : ps ≠ []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
q : F
qs : List F
hqs : qs ≠ []
ihq : 𝓢 ⊢! (p :: ps ++ qs).disj' ⟷ (p :: ps).disj' ⋎ qs.disj'
⊢ 𝓢 ⊢! (p :: ps ++ q :: qs).disj' ⟷ (p :: ps).disj' ⋎ (q :: qs).disj'
Tactic:
simp_all only [ne_eq, List.cons_append, List.append_eq_nil, and_self, not_false_eq_true, List.disj'_cons_nonempty]
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ q :: qs).disj' ⟷ (p ⋎ ps.disj') ⋎ q ⋎ qs.disj'
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ q :: qs).disj' ⟷ (p ⋎ ps.disj') ⋎ q ⋎ qs.disj'
Tactic:
apply iff_trans! (by
  apply or_replace_right_iff!;
  exact iff_trans! (@ihp (q :: qs)) (by
    apply or_replace_right_iff!;
    simp [List.disj'_cons_nonempty hqs];
  )
) or_assoc!
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! p ⋎ (ps ++ q :: qs).disj' ⟷ p ⋎ ps.disj' ⋎ q ⋎ qs.disj'
Tactic:
apply or_replace_right_iff!
Proof state after:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! (ps ++ q :: qs).disj' ⟷ ps.disj' ⋎ q ⋎ qs.disj'
Theorem: LO.System.iff_concact_disj!
Proof state before:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! (ps ++ q :: qs).disj' ⟷ ps.disj' ⋎ q ⋎ qs.disj'
Tactic:
exact iff_trans! (@ihp (q :: qs)) (by
  apply or_replace_right_iff!;
  simp [List.disj'_cons_nonempty hqs];
)
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj!
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! ps.disj' ⋎ (q :: qs).disj' ⟷ ps.disj' ⋎ q ⋎ qs.disj'
Tactic:
apply or_replace_right_iff!
Proof state after:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! (q :: qs).disj' ⟷ q ⋎ qs.disj'
Theorem: LO.System.iff_concact_disj!
Proof state before:
case 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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! (q :: qs).disj' ⟷ q ⋎ qs.disj'
Tactic:
simp [List.disj'_cons_nonempty hqs]
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' ↔ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' → 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'

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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj' → 𝓢 ⊢! (Γ ++ Δ).disj'
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' → 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'

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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj' → 𝓢 ⊢! (Γ ++ Δ).disj'
Tactic:
. intro h; exact (conj₁'! iff_concact_disj!) ⨀ 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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj' → 𝓢 ⊢! (Γ ++ Δ).disj'
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj' → 𝓢 ⊢! (Γ ++ Δ).disj'
Tactic:
. intro h; exact (conj₂'! iff_concact_disj!) ⨀ h;
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' → 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! (Γ ++ Δ).disj'
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! (Γ ++ Δ).disj'
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
Tactic:
exact (conj₁'! iff_concact_disj!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⋎ Δ.disj' → 𝓢 ⊢! (Γ ++ Δ).disj'
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (Γ ++ Δ).disj'
Theorem: LO.System.iff_concact_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! Γ.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (Γ ++ Δ).disj'
Tactic:
exact (conj₂'! iff_concact_disj!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ (q :: Γ).disj' ↔ 𝓢 ⊢! p ⟶ q ⋎ Γ.disj'
Tactic:
induction Γ with
| nil =>
  simp;
  constructor;
  . intro h; exact imp_trans! h disj₁!;
  . intro h; exact imp_trans! h $ disj₃''! imp_id! efq!;
| cons q ih => simp;
Proof state after:
no goals
Theorem: LO.System.implyRight_cons_disj'!
Proof state before:
case nil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ [q].disj' ↔ 𝓢 ⊢! p ⟶ q ⋎ [].disj'
Tactic:
simp
Proof state after:
case nil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ↔ 𝓢 ⊢! p ⟶ q ⋎ ⊥
Theorem: LO.System.implyRight_cons_disj'!
Proof state before:
case nil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ↔ 𝓢 ⊢! p ⟶ q ⋎ ⊥
Tactic:
constructor
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! 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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥ → 𝓢 ⊢! p ⟶ q
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! 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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥ → 𝓢 ⊢! p ⟶ q
Tactic:
. intro h; exact imp_trans! h disj₁!;
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥ → 𝓢 ⊢! p ⟶ q
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥ → 𝓢 ⊢! p ⟶ q
Tactic:
. intro h; exact imp_trans! h $ disj₃''! imp_id! efq!;
Proof state after:
no goals
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! 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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! p ⟶ q
⊢ 𝓢 ⊢! p ⟶ q ⋎ ⊥
Tactic:
exact imp_trans! h disj₁!
Proof state after:
no goals
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! 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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! p ⟶ q ⋎ ⊥
⊢ 𝓢 ⊢! p ⟶ q
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
h : 𝓢 ⊢! p ⟶ q ⋎ ⊥
⊢ 𝓢 ⊢! p ⟶ q
Tactic:
exact imp_trans! h $ disj₃''! imp_id! efq!
Proof state after:
no goals
Theorem: LO.System.implyRight_cons_disj'!
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 𝓢
inst✝ : HasEFQ 𝓢
q : F
ih : List F
tail_ih✝ : 𝓢 ⊢! p ⟶ (q✝ :: ih).disj' ↔ 𝓢 ⊢! p ⟶ q✝ ⋎ ih.disj'
⊢ 𝓢 ⊢! p ⟶ (q✝ :: q :: ih).disj' ↔ 𝓢 ⊢! p ⟶ q✝ ⋎ (q :: ih).disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.forthback_disj'_remove
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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle q =>
  simp;
  by_cases h: q = p;
  . subst_vars; simp;
  . simp [(List.remove_singleton_of_ne h)];
| hcons q Γ h ih =>
  simp [(List.disj'_cons_nonempty h)];
  by_cases hpq : q = p;
  . simp_all only [ne_eq, List.remove_cons_self]; exact disj₃''! disj₁! ih;
  . simp_all [(List.remove_cons_of_ne Γ hpq)];
    by_cases hqΓ : Γ.remove p = [];
    . simp_all;
      exact disj₃''! disj₂! (imp_trans! ih $ or_replace_right! efq!);
    . simp [(List.disj'_cons_nonempty hqΓ)];
      exact disj₃''! (imp_trans! disj₁! disj₂!) (imp_trans! ih (or_replace_right! disj₂!));
Proof state after:
no goals
Theorem: LO.System.forthback_disj'_remove
Proof state before:
case hnil
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! [].disj' ⟶ p ⋎ (List.remove p []).disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.forthback_disj'_remove
Proof state before:
case hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
⊢ 𝓢 ⊢! [q].disj' ⟶ p ⋎ (List.remove p [q]).disj'
Tactic:
simp
Proof state after:
case hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
⊢ 𝓢 ⊢! q ⟶ p ⋎ (List.remove p [q]).disj'
Theorem: LO.System.forthback_disj'_remove
Proof state before:
case hsingle
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
⊢ 𝓢 ⊢! q ⟶ p ⋎ (List.remove p [q]).disj'
Tactic:
by_cases h: 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 𝓢
inst✝ : HasEFQ 𝓢
q : F
h : q = p
⊢ 𝓢 ⊢! q ⟶ p ⋎ (List.remove p [q]).disj'

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 𝓢
inst✝ : HasEFQ 𝓢
q : F
h : ¬q = p
⊢ 𝓢 ⊢! q ⟶ p ⋎ (List.remove p [q]).disj'