Theorem: appBoundingFormalApplication (Fine/SystemB/CanonicalModel.lean)

State before:
⊢ ∀ (t u : Th) (p : Pr),
    formalApplicationFunction t u ≤ ↑p →
      ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
intros t u p h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
have ⟨q,h₂,h₃⟩ := lemma1 t u p h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
have ⟨r,h₄,h₅⟩ := lemma2 t u p h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
r : Pr
h₄ : u ≤ ↑r
h₅ : formalApplication ↑t ↑↑r ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
r : Pr
h₄ : u ≤ ↑r
h₅ : formalApplication ↑t ↑↑r ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
exact ⟨q,r,h₂,h₄,h₃,h₅⟩
State after:
no goals

State before:
⊢ ∀ (t u : Th) (p : Pr), formalApplicationFunction t u ≤ ↑p → ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
intros t u p h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
let Δ := {f : Form | ¬(formalApplication (▲{f}) u ⊆ p) }
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₂ : ↑t ∩ Δ = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros P h₂
  have l₃ : ▲{P} ⊆ ↑t := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
  have l₄ := formalAppMonotoneRight ↑u l₃
  exact h₂.right $ le_trans l₄ h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₃ : isDisjunctionClosed Δ := by
  intros P Q h₁ h₂
  have ⟨R,l₄⟩ := nonconstruction h₁.left
  have ⟨⟨S,l₆,⟨prf₁⟩⟩,l₈⟩ := nonconstruction l₄
  have ⟨T,l₉⟩ := nonconstruction h₁.right
  have ⟨⟨U,l₁₀,⟨prf₂⟩⟩,l₁₂⟩ := nonconstruction l₉
  clear h₁ l₄ l₉
  have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
  apply l₁₃
  apply h₂
  clear l₈ l₁₂ l₁₃ h₂
  have prf₃ : BProof {P} (S & U ⊃ R ¦ T) := BProof.mp 
    (BProof.mp prf₁ (BTheorem.hs BTheorem.taut BTheorem.orI₁))
    (BTheorem.hs BTheorem.andE₁ BTheorem.taut)
  have prf₄ : BProof {Q} (S & U ⊃ R ¦ T) := BProof.mp 
    (BProof.mp prf₂ (BTheorem.hs BTheorem.taut BTheorem.orI₂))
    (BTheorem.hs BTheorem.andE₂ BTheorem.taut)
  have prf₅ : BProof {P ¦ Q} (S & U ⊃ R ¦ T) := BTheorem.toProof $
    BTheorem.mp (BTheorem.adj prf₃.toTheorem prf₄.toTheorem) BTheorem.orE
  clear prf₁ prf₂ prf₃ prf₄
  have l₁₄ : S & U ∈ u := u.property.mpr ⟨BProof.adj (BProof.ax l₆) (BProof.ax l₁₀)⟩
  exact ⟨S & U, l₁₄, ⟨prf₅⟩⟩
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₄ : lindenbaumExtension t Δ ∩ Δ = ∅  := lindenbaumTheorem l₂ l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
clear l₂ l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
refine ⟨⟨⟨lindenbaumExtension t Δ, lindenbaumIsFormal⟩, lindenbaumIsPrime⟩, lindenbaumExtensionExtends, ?_⟩
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ formalApplication
      ↑↑{
            val :=
              { val := lindenbaumExtension t Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension t Δ → f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ) }
      ↑u ⊆
    ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ formalApplication
      ↑↑{
            val :=
              { val := lindenbaumExtension t Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension t Δ → f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ) }
      ↑u ⊆
    ↑↑p
Tactic:
change formalApplication (lindenbaumExtension t Δ) ↑u ⊆ p
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ formalApplication (lindenbaumExtension t Δ) ↑u ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ formalApplication (lindenbaumExtension t Δ) ↑u ⊆ ↑↑p
Tactic:
intros P h₁
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
⊢ P ∈ ↑↑p
Tactic:
have ⟨Q,h₂,h₃⟩ := h₁
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
⊢ P ∈ ↑↑p
Tactic:
have l₄ : formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p := by
  apply byContradiction
  intros h₄
  exact (Set.eq_empty_iff_forall_not_mem.mp l₄) (Q⊃P) ⟨h₃,h₄⟩
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄✝ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
l₄ : formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄✝ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
l₄ : formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p
⊢ P ∈ ↑↑p
Tactic:
exact l₄ ⟨Q,h₂,⟨BProof.ax rfl⟩⟩
State after:
no goals

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ↑t ∩ Δ = ∅
Tactic:
apply Set.eq_empty_iff_forall_not_mem.mpr
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑t ∩ Δ

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑t ∩ Δ
Tactic:
intros P h₂
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
⊢ False
Tactic:
have l₃ : ▲{P} ⊆ ↑t := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
⊢ False
Tactic:
have l₄ := formalAppMonotoneRight ↑u l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
l₄ : flip formalApplication (↑u) (▲{P}) ≤ flip formalApplication ↑u ↑t
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
l₄ : flip formalApplication (↑u) (▲{P}) ≤ flip formalApplication ↑u ↑t
⊢ False
Tactic:
exact h₂.right $ le_trans l₄ h₁
State after:
no goals

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
⊢ isDisjunctionClosed Δ
Tactic:
intros P Q h₁ h₂
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
⊢ False
Tactic:
have ⟨R,l₄⟩ := nonconstruction h₁.left
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨S,l₆,⟨prf₁⟩⟩,l₈⟩ := nonconstruction l₄
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
⊢ False
Tactic:
have ⟨T,l₉⟩ := nonconstruction h₁.right
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (▲{Q}) ↑u → T ∈ ↑↑p)
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (▲{Q}) ↑u → T ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨U,l₁₀,⟨prf₂⟩⟩,l₁₂⟩ := nonconstruction l₉
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (▲{Q}) ↑u → T ∈ ↑↑p)
U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (▲{Q}) ↑u → T ∈ ↑↑p)
U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
clear h₁ l₄ l₉
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False
Tactic:
apply l₁₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p
Tactic:
apply h₂
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
clear l₈ l₁₂ l₁₃ h₂
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
have prf₃ : BProof {P} (S & U ⊃ R ¦ T) := BProof.mp 
  (BProof.mp prf₁ (BTheorem.hs BTheorem.taut BTheorem.orI₁))
  (BTheorem.hs BTheorem.andE₁ BTheorem.taut)
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
have prf₄ : BProof {Q} (S & U ⊃ R ¦ T) := BProof.mp 
  (BProof.mp prf₂ (BTheorem.hs BTheorem.taut BTheorem.orI₂))
  (BTheorem.hs BTheorem.andE₂ BTheorem.taut)
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
prf₄ : BProof {Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
prf₄ : BProof {Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
have prf₅ : BProof {P ¦ Q} (S & U ⊃ R ¦ T) := BTheorem.toProof $
  BTheorem.mp (BTheorem.adj prf₃.toTheorem prf₄.toTheorem) BTheorem.orE
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
prf₄ : BProof {Q} (S&U⊃R¦T)
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
prf₃ : BProof {P} (S&U⊃R¦T)
prf₄ : BProof {Q} (S&U⊃R¦T)
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
clear prf₁ prf₂ prf₃ prf₄
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
T U : Form
l₁₀ : U ∈ ↑u
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
T U : Form
l₁₀ : U ∈ ↑u
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
have l₁₄ : S & U ∈ u := u.property.mpr ⟨BProof.adj (BProof.ax l₆) (BProof.ax l₁₀)⟩
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
T U : Form
l₁₀ : U ∈ ↑u
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
l₁₄ : S&U ∈ u
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q R S : Form
l₆ : S ∈ ↑u
T U : Form
l₁₀ : U ∈ ↑u
prf₅ : BProof {P¦Q} (S&U⊃R¦T)
l₁₄ : S&U ∈ u
⊢ R¦T ∈ formalApplication (▲{P¦Q}) ↑u
Tactic:
exact ⟨S & U, l₁₄, ⟨prf₅⟩⟩
State after:
no goals

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
⊢ formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p
Tactic:
apply byContradiction
State after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
⊢ ¬formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p → False

State before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
⊢ ¬formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p → False
Tactic:
intros h₄
State after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
h₄ : ¬formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p
⊢ False

State before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (lindenbaumExtension t Δ) ↑u
Q : Form
h₂ : Q ∈ ↑u
h₃ : Q⊃P ∈ lindenbaumExtension t Δ
h₄ : ¬formalApplication (▲{Q⊃P}) ↑u ⊆ ↑↑p
⊢ False
Tactic:
exact (Set.eq_empty_iff_forall_not_mem.mp l₄) (Q⊃P) ⟨h₃,h₄⟩
State after:
no goals

State before:
⊢ ∀ (t u : Th) (p : Pr), formalApplicationFunction t u ≤ ↑p → ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
intros t u p h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
let Δ := {f : Form | ¬(formalApplication t (▲{f}) ⊆ p) }
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
have l₂ : ↑u ∩ Δ = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros P h₂
  have l₃ : ▲{P} ⊆ ↑u := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
  have l₄ := formalAppMonotoneLeft ↑t l₃
  exact h₂.right $ le_trans l₄ h₁
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
have l₃ : isDisjunctionClosed Δ := by
  intros P Q h₁ h₂
  have ⟨R,l₄⟩ := nonconstruction h₁.left
  have ⟨⟨S,⟨prf₁⟩,l₆⟩,l₈⟩ := nonconstruction l₄
  have ⟨T,l₉⟩ := nonconstruction h₁.right
  have ⟨⟨U,⟨prf₂⟩,l₁₀⟩,l₁₂⟩ := nonconstruction l₉
  clear h₁ l₄ l₉
  have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
  apply l₁₃
  apply h₂
  clear l₈ l₁₂ l₁₃ h₂
  have l₁₄ : S¦U ∈ ▲{P¦Q} := ⟨(BTheorem.orFunctor prf₁.toTheorem prf₂.toTheorem).toProof⟩
  have l₁₅ : (S¦U ⊃ R¦T) ∈ t := t.property.mpr ⟨BProof.mp (BProof.adj 
    (BProof.mp (BProof.ax l₆) (BTheorem.hs BTheorem.taut BTheorem.orI₁))
    (BProof.mp (BProof.ax l₁₀) (BTheorem.hs BTheorem.taut BTheorem.orI₂)))
    BTheorem.orE⟩
  exact ⟨S ¦ U, l₁₄, l₁₅⟩
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
have l₄ : lindenbaumExtension u Δ ∩ Δ = ∅  := lindenbaumTheorem l₂ l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
clear l₂ l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
refine ⟨⟨⟨lindenbaumExtension u Δ, lindenbaumIsFormal⟩, lindenbaumIsPrime⟩, lindenbaumExtensionExtends, ?_⟩
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication ↑t
      ↑↑{
            val :=
              { val := lindenbaumExtension u Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension u Δ ↔ lindenbaumExtension u Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension u Δ → f ∈ lindenbaumExtension u Δ ∨ g ∈ lindenbaumExtension u Δ) } ⊆
    ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication ↑t
      ↑↑{
            val :=
              { val := lindenbaumExtension u Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension u Δ ↔ lindenbaumExtension u Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension u Δ → f ∈ lindenbaumExtension u Δ ∨ g ∈ lindenbaumExtension u Δ) } ⊆
    ↑↑p
Tactic:
change formalApplication ↑t (lindenbaumExtension u Δ) ⊆ p
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication (↑t) (lindenbaumExtension u Δ) ⊆ ↑↑p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication (↑t) (lindenbaumExtension u Δ) ⊆ ↑↑p
Tactic:
intros P h₁
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
⊢ P ∈ ↑↑p
Tactic:
have ⟨Q,h₂,h₃⟩ := h₁
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ P ∈ ↑↑p
Tactic:
have l₄ : formalApplication ↑t (▲{Q}) ⊆ ↑↑p := by
  apply byContradiction
  intros h₄
  exact (Set.eq_empty_iff_forall_not_mem.mp l₄) Q ⟨h₂,h₄⟩
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄✝ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
l₄ : formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ P ∈ ↑↑p

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄✝ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
l₄ : formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ P ∈ ↑↑p
Tactic:
exact l₄ ⟨Q,⟨BProof.ax rfl⟩,h₃⟩
State after:
no goals

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ↑u ∩ Δ = ∅
Tactic:
apply Set.eq_empty_iff_forall_not_mem.mpr
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑u ∩ Δ

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑u ∩ Δ
Tactic:
intros P h₂
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
⊢ False
Tactic:
have l₃ : ▲{P} ⊆ ↑u := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
⊢ False
Tactic:
have l₄ := formalAppMonotoneLeft ↑t l₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
l₄ : formalApplication (↑t) (▲{P}) ≤ formalApplication ↑t ↑u
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
l₄ : formalApplication (↑t) (▲{P}) ≤ formalApplication ↑t ↑u
⊢ False
Tactic:
exact h₂.right $ le_trans l₄ h₁
State after:
no goals

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
⊢ isDisjunctionClosed Δ
Tactic:
intros P Q h₁ h₂
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
⊢ False
Tactic:
have ⟨R,l₄⟩ := nonconstruction h₁.left
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨S,⟨prf₁⟩,l₆⟩,l₈⟩ := nonconstruction l₄
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
⊢ False
Tactic:
have ⟨T,l₉⟩ := nonconstruction h₁.right
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨U,⟨prf₂⟩,l₁₀⟩,l₁₂⟩ := nonconstruction l₉
State after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
clear h₁ l₄ l₉
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False
Tactic:
apply l₁₃
State after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p

State before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p
Tactic:
apply h₂
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
clear l₈ l₁₂ l₁₃ h₂
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
have l₁₄ : S¦U ∈ ▲{P¦Q} := ⟨(BTheorem.orFunctor prf₁.toTheorem prf₂.toTheorem).toProof⟩
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
have l₁₅ : (S¦U ⊃ R¦T) ∈ t := t.property.mpr ⟨BProof.mp (BProof.adj 
  (BProof.mp (BProof.ax l₆) (BTheorem.hs BTheorem.taut BTheorem.orI₁))
  (BProof.mp (BProof.ax l₁₀) (BTheorem.hs BTheorem.taut BTheorem.orI₂)))
  BTheorem.orE⟩
State after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
l₁₅ : S¦U⊃R¦T ∈ t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})

State before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
l₁₅ : S¦U⊃R¦T ∈ t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
exact ⟨S ¦ U, l₁₄, l₁₅⟩
State after:
no goals

State before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
Tactic:
apply byContradiction
State after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p → False

State before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p → False
Tactic:
intros h₄
State after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
h₄ : ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ False

State before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
h₄ : ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ False
Tactic:
exact (Set.eq_empty_iff_forall_not_mem.mp l₄) Q ⟨h₂,h₄⟩
State after:
no goals