internlm/Lean-Github huggingface dataset:
Theorem: appBoundingFormalApplication
Proof 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₃
Proof 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
Theorem: appBoundingFormalApplication
Proof 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, ?_⟩
Proof 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
Theorem: appBoundingFormalApplication
Proof 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
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₄⟩
Proof 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
Theorem: appBoundingFormalApplication
Proof 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⟩⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof 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
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑t ∩ Δ
Theorem: appBoundingFormalApplication
Proof 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₂
Proof 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
Theorem: appBoundingFormalApplication
Proof 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)
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₃
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof 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₂
Proof 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
Theorem: appBoundingFormalApplication
Proof 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
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₄
Proof 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
Theorem: appBoundingFormalApplication
Proof 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
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₉
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₉
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁₂
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁₃
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₂
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₂
Proof 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
Theorem: appBoundingFormalApplication
Proof 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)
Proof 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
Theorem: appBoundingFormalApplication
Proof 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)
Proof 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
Theorem: appBoundingFormalApplication
Proof 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
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₄
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁₀)⟩
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₅⟩⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof 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
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₄
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₄⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
⊢ ∀ (t u : Th) (p : Pr), formalApplicationFunction t u ≤ ↑p → ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
intros t u p h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof 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) }
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₁₅⟩
Proof 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
Theorem: appBoundingFormalApplication
Proof 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₃
Proof 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