internlm/Lean-Github huggingface dataset:
Theorem: LO.System.or_replace_right_iff!
Proof state before:
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
Tactic:
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 ⋎ r ⟶ p ⋎ q
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
⊢ 𝓢 ⊢! r ⟶ q
Theorem: LO.System.or_replace_right_iff!
Proof state before:
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
⊢ 𝓢 ⊢! r ⟶ q
Tactic:
exact conj₂'! d
Proof state after:
no goals
Theorem: LO.System.or_replace_left_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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟷ r ⋎ q
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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ r ⋎ q

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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⋎ q ⟶ p ⋎ q
Theorem: LO.System.or_replace_left_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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ r ⋎ q

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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⋎ q ⟶ p ⋎ q
Tactic:
. apply or_replace_left!; 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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⋎ q ⟶ p ⋎ q
Theorem: LO.System.or_replace_left_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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⋎ q ⟶ p ⋎ q
Tactic:
. apply or_replace_left!; exact conj₂'! d;
Proof state after:
no goals
Theorem: LO.System.or_replace_left_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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⋎ q ⟶ r ⋎ q
Tactic:
apply or_replace_left!
Proof state after:
case h₁.hp
F : 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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⟶ r
Theorem: LO.System.or_replace_left_iff!
Proof state before:
case h₁.hp
F : 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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! p ⟶ r
Tactic:
exact conj₁'! d
Proof state after:
no goals
Theorem: LO.System.or_replace_left_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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⋎ q ⟶ p ⋎ q
Tactic:
apply or_replace_left!
Proof state after:
case h₂.hp
F : 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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⟶ p
Theorem: LO.System.or_replace_left_iff!
Proof state before:
case h₂.hp
F : 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 : 𝓢 ⊢! p ⟷ r
⊢ 𝓢 ⊢! r ⟶ p
Tactic:
exact conj₂'! d
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 𝓢
⊢ 𝓢 ⊢! ([] ++ []).disj' ⟷ [].disj' ⋎ [].disj'
Tactic:
case hnil.hnil =>
  simp only [List.append_nil, List.disj'_nil];
  apply iff_intro!;
  . simp;
  . exact disj₃''! efq! efq!;
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✝ : F
⊢ 𝓢 ⊢! ([] ++ [a✝]).disj' ⟷ [].disj' ⋎ [a✝].disj'
Tactic:
case hnil.hsingle =>
  simp only [List.nil_append, List.disj'_singleton, List.disj'_nil];
  apply iff_intro!;
  . simp;
  . 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✝ : F
⊢ 𝓢 ⊢! ([a✝] ++ []).disj' ⟷ [a✝].disj' ⋎ [].disj'
Tactic:
case hsingle.hnil =>
  simp only [List.singleton_append, List.disj'_singleton, List.disj'_nil];
  apply iff_intro!;
  . simp;
  . exact disj₃''! imp_id! efq!;
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✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝ ++ []).disj' ⟷ (a✝² :: as✝).disj' ⋎ [].disj'
Tactic:
case hcons.hnil =>
  simp only [List.append_nil, List.disj'_nil];
  apply iff_intro!;
  . simp;
  . exact disj₃''! imp_id! efq!;
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✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ([] ++ a✝² :: as✝).disj' ⟷ [].disj' ⋎ (a✝² :: as✝).disj'
Tactic:
case hnil.hcons =>
  simp only [List.nil_append, List.disj'_nil];
  apply iff_intro!;
  . simp;
  . 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:
case hsingle.hsingle => 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:
case hsingle.hcons => 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:
case hcons.hsingle p ps hps ihp q =>
  simp_all;
  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
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:
case hcons.hcons p ps hps ihp q qs hqs ihq =>
  simp_all only [ne_eq, List.cons_append, List.append_eq_nil, and_self, not_false_eq_true, List.disj'_cons_nonempty];
  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 𝓢
⊢ 𝓢 ⊢! ([] ++ []).disj' ⟷ [].disj' ⋎ [].disj'
Tactic:
simp only [List.append_nil, List.disj'_nil]
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟷ ⊥ ⋎ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟷ ⊥ ⋎ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟶ ⊥ ⋎ ⊥

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 𝓢
⊢ 𝓢 ⊢! ⊥ ⋎ ⊥ ⟶ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟶ ⊥ ⋎ ⊥

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 𝓢
⊢ 𝓢 ⊢! ⊥ ⋎ ⊥ ⟶ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⋎ ⊥ ⟶ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⋎ ⊥ ⟶ ⊥
Tactic:
. exact disj₃''! efq! efq!;
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟶ ⊥ ⋎ ⊥
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⋎ ⊥ ⟶ ⊥
Tactic:
exact disj₃''! efq! efq!
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✝ : F
⊢ 𝓢 ⊢! ([] ++ [a✝]).disj' ⟷ [].disj' ⋎ [a✝].disj'
Tactic:
simp only [List.nil_append, List.disj'_singleton, List.disj'_nil]
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 𝓢
a✝ : F
⊢ 𝓢 ⊢! a✝ ⟷ ⊥ ⋎ a✝
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
⊢ 𝓢 ⊢! a✝ ⟷ ⊥ ⋎ a✝
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
⊢ 𝓢 ⊢! a✝ ⟶ ⊥ ⋎ a✝

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
⊢ 𝓢 ⊢! ⊥ ⋎ a✝ ⟶ a✝
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
⊢ 𝓢 ⊢! a✝ ⟶ ⊥ ⋎ a✝

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
⊢ 𝓢 ⊢! ⊥ ⋎ a✝ ⟶ a✝
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
⊢ 𝓢 ⊢! ⊥ ⋎ a✝ ⟶ a✝
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
⊢ 𝓢 ⊢! ⊥ ⋎ a✝ ⟶ a✝
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
⊢ 𝓢 ⊢! a✝ ⟶ ⊥ ⋎ a✝
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
⊢ 𝓢 ⊢! ⊥ ⋎ a✝ ⟶ a✝
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✝ : F
⊢ 𝓢 ⊢! ([a✝] ++ []).disj' ⟷ [a✝].disj' ⋎ [].disj'
Tactic:
simp only [List.singleton_append, List.disj'_singleton, List.disj'_nil]
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 𝓢
a✝ : F
⊢ 𝓢 ⊢! a✝ ⟷ a✝ ⋎ ⊥
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
⊢ 𝓢 ⊢! a✝ ⟷ a✝ ⋎ ⊥
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
⊢ 𝓢 ⊢! a✝ ⟶ a✝ ⋎ ⊥

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
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
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
⊢ 𝓢 ⊢! a✝ ⟶ a✝ ⋎ ⊥

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
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
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
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
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
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
Tactic:
. exact disj₃''! imp_id! efq!;
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
⊢ 𝓢 ⊢! a✝ ⟶ a✝ ⋎ ⊥
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
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
Tactic:
exact disj₃''! imp_id! efq!
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✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝ ++ []).disj' ⟷ (a✝² :: as✝).disj' ⋎ [].disj'
Tactic:
simp only [List.append_nil, List.disj'_nil]
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 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟷ (a✝² :: as✝).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 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⋎ ⊥ ⟶ (a✝² :: as✝).disj'
Tactic:
. exact disj₃''! imp_id! efq!;
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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.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✝ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⋎ ⊥ ⟶ (a✝² :: as✝).disj'
Tactic:
exact disj₃''! imp_id! efq!
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✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! ([] ++ a✝² :: as✝).disj' ⟷ [].disj' ⋎ (a✝² :: as✝).disj'
Tactic:
simp only [List.nil_append, List.disj'_nil]
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 𝓢
a✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! ([] ++ as✝).disj' ⟷ [].disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝² :: as✝).disj' ⟷ ⊥ ⋎ (a✝² :: as✝).disj'