Theorem: LO.System.forthback_disj'_remove (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' ⟶ 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₂!));
State after:
no goals

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

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

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

State before:
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'
Tactic:
. subst_vars; simp;
State after:
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'

State before:
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'
Tactic:
. simp [(List.remove_singleton_of_ne h)];
State after:
no goals

State before:
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'
Tactic:
subst_vars
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 𝓢
q✝ r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
⊢ 𝓢 ⊢! q ⟶ q ⋎ (List.remove q [q]).disj'

State before:
case pos
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
q✝ r : F
Γ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
⊢ 𝓢 ⊢! q ⟶ q ⋎ (List.remove q [q]).disj'
Tactic:
simp
State after:
no goals

State before:
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'
Tactic:
simp [(List.remove_singleton_of_ne h)]
State after:
no goals

State before:
case 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
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
⊢ 𝓢 ⊢! (q :: Γ).disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
simp [(List.disj'_cons_nonempty h)]
State after:
case 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
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'

State before:
case 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
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
by_cases hpq : q = p
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ 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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'

State before:
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ 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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
. simp_all only [ne_eq, List.remove_cons_self]; exact disj₃''! disj₁! ih;
State after:
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'

State before:
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
. 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₂!));
State after:
no goals

State before:
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
simp_all only [ne_eq, List.remove_cons_self]
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : q = p
⊢ 𝓢 ⊢! p ⋎ Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : q = p
⊢ 𝓢 ⊢! p ⋎ Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
Tactic:
exact disj₃''! disj₁! ih
State after:
no goals

State before:
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
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
Tactic:
simp_all [(List.remove_cons_of_ne Γ hpq)]
State after:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
Tactic:
by_cases hqΓ : Γ.remove p = []
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
Tactic:
. simp_all;
  exact disj₃''! disj₂! (imp_trans! ih $ or_replace_right! efq!);
State after:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
Tactic:
. simp [(List.disj'_cons_nonempty hqΓ)];
  exact disj₃''! (imp_trans! disj₁! disj₂!) (imp_trans! ih (or_replace_right! disj₂!));
State after:
no goals

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
Tactic:
simp_all
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ ⊥
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ q

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ ⊥
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ q
Tactic:
exact disj₃''! disj₂! (imp_trans! ih $ or_replace_right! efq!)
State after:
no goals

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
Tactic:
simp [(List.disj'_cons_nonempty hqΓ)]
State after:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ q ⋎ (List.remove p Γ).disj'

State before:
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
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ q ⋎ (List.remove p Γ).disj'
Tactic:
exact disj₃''! (imp_trans! disj₁! disj₂!) (imp_trans! ih (or_replace_right! disj₂!))
State after:
no goals