Theorem: LO.System.iff_concact_disj! (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 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! (Γ ++ Δ).disj' ⟷ Γ.disj' ⋎ Δ.disj'
Tactic:
induction Γ using List.induction_with_singleton generalizing Δ <;> induction Δ using List.induction_with_singleton
State after:
case hnil.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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! ([] ++ []).disj' ⟷ [].disj' ⋎ [].disj'

case hnil.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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! ([] ++ [a✝]).disj' ⟷ [].disj' ⋎ [a✝].disj'

case hnil.hcons
F : 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'

case hsingle.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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! ([a✝] ++ []).disj' ⟷ [a✝].disj' ⋎ [].disj'

case hsingle.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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝¹ a✝ : F
⊢ 𝓢 ⊢! ([a✝¹] ++ [a✝]).disj' ⟷ [a✝¹].disj' ⋎ [a✝].disj'

case hsingle.hcons
F : 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'

case hcons.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
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'

case hcons.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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝³ : F
as✝ : List F
a✝² : as✝ ≠ []
a✝¹ : ∀ {Δ : List F}, 𝓢 ⊢! (as✝ ++ Δ).disj' ⟷ as✝.disj' ⋎ Δ.disj'
a✝ : F
⊢ 𝓢 ⊢! (a✝³ :: as✝ ++ [a✝]).disj' ⟷ (a✝³ :: as✝).disj' ⋎ [a✝].disj'

case hcons.hcons
F : 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✝² : F
as✝ : List F
a✝¹ : as✝ ≠ []
a✝ : 𝓢 ⊢! (a✝⁵ :: as✝¹ ++ as✝).disj' ⟷ (a✝⁵ :: as✝¹).disj' ⋎ as✝.disj'
⊢ 𝓢 ⊢! (a✝⁵ :: as✝¹ ++ a✝² :: as✝).disj' ⟷ (a✝⁵ :: as✝¹).disj' ⋎ (a✝² :: as✝).disj'

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!;
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
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!;
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
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!;
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
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!;
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
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!;
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
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!];
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
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!];
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
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!;
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
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!;
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
⊢ 𝓢 ⊢! ([] ++ []).disj' ⟷ [].disj' ⋎ [].disj'
Tactic:
simp only [List.append_nil, List.disj'_nil]
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 𝓢
⊢ 𝓢 ⊢! ⊥ ⟷ ⊥ ⋎ ⊥

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

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

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

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

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

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

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

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

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!;
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! a✝ ⟶ a✝ ⋎ ⊥
Tactic:
simp
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
a✝ : F
⊢ 𝓢 ⊢! a✝ ⋎ ⊥ ⟶ a✝
Tactic:
exact disj₃''! imp_id! efq!
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
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]
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' ⋎ ⊥

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

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

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

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

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

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

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

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

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

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

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