internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case mp.hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ᵀᴾ) ⋯
Tactic:
dsimp [Axioms.K, TrivTranslation, toPropFormula]
Proof state after:
case mp.hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ((w✝¹ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯) ⟶ (w✝¹ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ((w✝¹ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯) ⟶ (w✝¹ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Tactic:
apply imp_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hT
Proof state after:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝ : Formula α
e : Axioms.T w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝ : Formula α
e : Axioms.T w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (Axioms.T w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (Axioms.T w✝ᵀᴾ) ⋯
Tactic:
dsimp [Axioms.T, TrivTranslation, toPropFormula]
Proof state after:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Tactic:
apply imp_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hTc
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝ : Formula α
e : Axioms.Tc w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝ : Formula α
e : Axioms.Tc w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.Tc w✝
⊢ 𝐂𝐥 ⊢! (Axioms.Tc w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.Tc w✝
⊢ 𝐂𝐥 ⊢! (Axioms.Tc w✝ᵀᴾ) ⋯
Tactic:
dsimp [Axioms.Tc, TrivTranslation, toPropFormula]
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.Tc w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.Tc w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯
Tactic:
apply imp_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐓𝐫𝐢𝐯 ⊢ p✝ ⟶ q✝
h₂ : 𝐓𝐫𝐢𝐯 ⊢ p✝
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! ((p✝ ⟶ q✝)ᵀᴾ) ⋯
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
h : 𝐓𝐫𝐢𝐯 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ᵀᴾ) ⋯
Tactic:
dsimp [TrivTranslation, toPropFormula] at ih₁ ih₂
Proof state after:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐓𝐫𝐢𝐯 ⊢ p✝ ⟶ q✝
h₂ : 𝐓𝐫𝐢𝐯 ⊢ p✝
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
h : 𝐓𝐫𝐢𝐯 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐓𝐫𝐢𝐯 ⊢ p✝ ⟶ q✝
h₂ : 𝐓𝐫𝐢𝐯 ⊢ p✝
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
h : 𝐓𝐫𝐢𝐯 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ᵀᴾ) ⋯
Tactic:
exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩)
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐓𝐫𝐢𝐯 ⊢ p✝
ih : 𝐓𝐫𝐢𝐯 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
h : 𝐓𝐫𝐢𝐯 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ᵀᴾ) ⋯
Tactic:
exact ih $ axiomT'! h
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ᵀᴾ) ⋯
Tactic:
dsimp [TrivTranslation, toPropFormula]
Proof state after:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ᵀᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ᵀᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ᵀᴾ) ⋯
Tactic:
try first
| apply imp_id!;
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ᵀᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ᵀᴾ) ⋯
Tactic:
first
| apply imp_id!;
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ⊤
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⋏ (q✝ᵀᴾ) ⋯ ⟶ (p✝ᵀᴾ) ⋯
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⋏ (q✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯ ⟶ (p✝ᵀᴾ) ⋯ ⋏ (q✝ᵀᴾ) ⋯
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⟶ (p✝ᵀᴾ) ⋯ ⋎ (q✝ᵀᴾ) ⋯
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (q✝ᵀᴾ) ⋯ ⟶ (p✝ᵀᴾ) ⋯ ⋎ (q✝ᵀᴾ) ⋯
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ᵀᴾ) ⋯ ⟶ (r✝ᵀᴾ) ⋯) ⟶ ((q✝ᵀᴾ) ⋯ ⟶ (r✝ᵀᴾ) ⋯) ⟶ (p✝ᵀᴾ) ⋯ ⋎ (q✝ᵀᴾ) ⋯ ⟶ (r✝ᵀᴾ) ⋯
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯ ⟶ (p✝ᵀᴾ) ⋯
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯ ⟶ (r✝ᵀᴾ) ⋯) ⟶ ((p✝ᵀᴾ) ⋯ ⟶ (q✝ᵀᴾ) ⋯) ⟶ (p✝ᵀᴾ) ⋯ ⟶ (r✝ᵀᴾ) ⋯
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ᵀᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ᵀᴾ) ⋯
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯ → 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
have d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p := conj₂'! deducible_iff_trivTranslation
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
have d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ := by simpa only [TrivTranslation.back] using of_classical h;
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
exact d₁ ⨀ d₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
d₁ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ p
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ
Tactic:
simpa only [TrivTranslation.back] using of_classical h
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ↔ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Tactic:
. intro h;
  induction h.some using Deduction.inducition_with_nec with
  | hMaxm a =>
    rcases a with (hK | hVer)
    . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
    . obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; exact verum!;
  | hMdp h₁ h₂ ih₁ ih₂ =>
    dsimp [VerTranslation, toPropFormula] at ih₁ ih₂;
    exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
  | hNec => dsimp [toPropFormula]; exact verum!;
  | _ =>
    dsimp [VerTranslation, toPropFormula];
    try first
    | apply verum!;
    | apply imply₁!;
    | apply imply₂!;
    | apply conj₁!;
    | apply conj₂!;
    | apply conj₃!;
    | apply disj₁!;
    | apply disj₂!;
    | apply disj₃!;
    | apply dne!;
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Tactic:
. intro h;
  have d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p := conj₂'! deducible_iff_verTranslation;
  have d₂ : 𝐕𝐞𝐫 ⊢! pⱽ := by simpa using of_classical h;
  exact d₁ ⨀ d₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
induction h.some using Deduction.inducition_with_nec with
| hMaxm a =>
  rcases a with (hK | hVer)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
  . obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; exact verum!;
| hMdp h₁ h₂ ih₁ ih₂ =>
  dsimp [VerTranslation, toPropFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| hNec => dsimp [toPropFormula]; exact verum!;
| _ =>
  dsimp [VerTranslation, toPropFormula];
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐕𝐞𝐫)
h : 𝐕𝐞𝐫 ⊢! p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
rcases a with (hK | hVer)
Proof state after:
case mp.hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
Proof state after:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
. obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; exact verum!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ⱽᴾ) ⋯
Tactic:
dsimp only [Axioms.K, VerTranslation, toPropFormula]
Proof state after:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hVer
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
w✝ : Formula α
e : Axioms.Ver w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
w✝ : Formula α
e : Axioms.Ver w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! (Axioms.Ver w✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! (Axioms.Ver w✝ⱽᴾ) ⋯
Tactic:
dsimp [Axioms.Ver, VerTranslation, toPropFormula]
Proof state after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! ⊤
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
exact verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐕𝐞𝐫 ⊢ p✝ ⟶ q✝
h₂ : 𝐕𝐞𝐫 ⊢ p✝
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! ((p✝ ⟶ q✝)ⱽᴾ) ⋯
ih₂ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula] at ih₁ ih₂
Proof state after:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐕𝐞𝐫 ⊢ p✝ ⟶ q✝
h₂ : 𝐕𝐞𝐫 ⊢ p✝
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
ih₂ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐕𝐞𝐫 ⊢ p✝ ⟶ q✝
h₂ : 𝐕𝐞𝐫 ⊢ p✝
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
ih₂ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Tactic:
exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩)
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ⱽᴾ) ⋯
Tactic:
dsimp [toPropFormula]
Proof state after:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
exact verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula]
Proof state after:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! ⊤
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯) ⟶ (p✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ ((q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
⊢ 𝐕𝐞𝐫 ⊢! p
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
⊢ 𝐕𝐞𝐫 ⊢! p
Tactic:
have d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p := conj₂'! deducible_iff_verTranslation
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! p
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! p
Tactic:
have d₂ : 𝐕𝐞𝐫 ⊢! pⱽ := by simpa using of_classical h;
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
d₂ : 𝐕𝐞𝐫 ⊢! pⱽ
⊢ 𝐕𝐞𝐫 ⊢! p
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
d₂ : 𝐕𝐞𝐫 ⊢! pⱽ
⊢ 𝐕𝐞𝐫 ⊢! p
Tactic:
exact d₁ ⨀ d₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Ver_classical
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! pⱽ
Tactic:
simpa using of_classical h
Proof state after:
no goals