Theorem: formalAppIdentLeft (Fine/SystemB/Theories.lean)

State before:
⊢ ∀ (Γ : Th), formalApplicationFunction BTh Γ = Γ
Tactic:
intros Γ
State after:
Γ : Th
⊢ formalApplicationFunction BTh Γ = Γ

State before:
Γ : Th
⊢ formalApplicationFunction BTh Γ = Γ
Tactic:
ext f
State after:
case a.h
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) ↔ f ∈ ↑Γ

State before:
case a.h
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) ↔ f ∈ ↑Γ
Tactic:
apply Iff.intro
State after:
case a.h.mp
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ

case a.h.mpr
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)

State before:
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ
Tactic:
case a.h.mp =>
  intros h₁
  have ⟨g,h₂,⟨h₃⟩⟩ := h₁
  exact Γ.property.mpr ⟨BProof.mp (BProof.ax h₂) h₃⟩
State after:
no goals

State before:
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
case a.h.mpr =>
  intros h₁
  exact ⟨f, h₁, ⟨BTheorem.taut⟩⟩
State after:
no goals

State before:
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ
Tactic:
intros h₁
State after:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
⊢ f ∈ ↑Γ

State before:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
⊢ f ∈ ↑Γ
Tactic:
have ⟨g,h₂,⟨h₃⟩⟩ := h₁
State after:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
g : Form
h₂ : g ∈ ↑Γ
h₃ : BTheorem (g⊃f)
⊢ f ∈ ↑Γ

State before:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
g : Form
h₂ : g ∈ ↑Γ
h₃ : BTheorem (g⊃f)
⊢ f ∈ ↑Γ
Tactic:
exact Γ.property.mpr ⟨BProof.mp (BProof.ax h₂) h₃⟩
State after:
no goals

State before:
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
intros h₁
State after:
Γ : Th
f : Form
h₁ : f ∈ ↑Γ
⊢ f ∈ ↑(formalApplicationFunction BTh Γ)

State before:
Γ : Th
f : Form
h₁ : f ∈ ↑Γ
⊢ f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
exact ⟨f, h₁, ⟨BTheorem.taut⟩⟩
State after:
no goals