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

State before:
⊢ Function.Involutive primeStarFunction
Tactic:
intros Γ
State after:
Γ : Pr
⊢ primeStarFunction (primeStarFunction Γ) = Γ

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

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

case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))

State before:
case a.a.h.mp
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) → f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
all_goals intros h₁
State after:
case a.a.h.mp
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
case a.a.h.mpr =>
  intros h₂
  have l₁ : ~~f ∈ Γ := Γ.val.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.dni⟩
  exact h₂ l₁
State after:
no goals

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ
Tactic:
case a.a.h.mp =>
  apply byContradiction
  intros h₂
  have l₂ : ¬(~~f ∈ Γ) := h₂ ∘ λel => Γ.val.property.mpr ⟨BProof.mp (BProof.ax el) BTheorem.dne⟩
  exact h₁ l₂
State after:
no goals

State before:
case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
intros h₁
State after:
case a.a.h.mpr
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
intros h₂
State after:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
⊢ False

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
⊢ False
Tactic:
have l₁ : ~~f ∈ Γ := Γ.val.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.dni⟩
State after:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
l₁ : ~~f ∈ Γ
⊢ False

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
l₁ : ~~f ∈ Γ
⊢ False
Tactic:
exact h₂ l₁
State after:
no goals

State before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ
Tactic:
apply byContradiction
State after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ ¬f ∈ ↑↑Γ → False

State before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ ¬f ∈ ↑↑Γ → False
Tactic:
intros h₂
State after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
⊢ False

State before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
⊢ False
Tactic:
have l₂ : ¬(~~f ∈ Γ) := h₂ ∘ λel => Γ.val.property.mpr ⟨BProof.mp (BProof.ax el) BTheorem.dne⟩
State after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
l₂ : ¬~~f ∈ Γ
⊢ False

State before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
l₂ : ¬~~f ∈ Γ
⊢ False
Tactic:
exact h₁ l₂
State after:
no goals