Theorem: LO.Modal.Standard.iff_Ver_classical (Logic/Modal/Standard/Maximal.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ↔ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p

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!;
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p

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₂;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

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!;
State after:
no goals

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)
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✝ⱽᴾ) ⋯

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₁!;
State after:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

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!;
State after:
no goals

State before:
case mp.hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, _, e⟩ := hK
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✝ⱽᴾ) ⋯

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
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✝ⱽᴾ) ⋯

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]
State after:
case mp.hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤

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₁!
State after:
no goals

State before:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hVer
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✝ⱽᴾ) ⋯

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
State after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! (Axioms.Ver w✝ⱽᴾ) ⋯

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]
State after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! ⊤

State before:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! Axioms.Ver w✝
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
exact verum!
State after:
no goals

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₂
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✝ⱽᴾ) ⋯

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₂⟩)
State after:
no goals

State before:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ⱽᴾ) ⋯
Tactic:
dsimp [toPropFormula]
State after:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤

State before:
case mp.hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐕𝐞𝐫 ⊢ p✝
a✝ : 𝐕𝐞𝐫 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐕𝐞𝐫 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
exact verum!
State after:
no goals

State before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula]
State after:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯

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!;
State after:
no goals

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!;
State after:
no goals

State before:
case mp.hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! ⊤
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case mp.hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply imply₁!
State after:
no goals

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₂!
State after:
no goals

State before:
case mp.hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply conj₁!
State after:
no goals

State before:
case mp.hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
Tactic:
apply conj₂!
State after:
no goals

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₃!
State after:
no goals

State before:
case mp.hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₁!
State after:
no goals

State before:
case mp.hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₂!
State after:
no goals

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₃!
State after:
no goals

State before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply dne!
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯ → 𝐕𝐞𝐫 ⊢! p
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
⊢ 𝐕𝐞𝐫 ⊢! p

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
⊢ 𝐕𝐞𝐫 ⊢! p
Tactic:
have d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p := conj₂'! deducible_iff_verTranslation
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! p

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;
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
d₂ : 𝐕𝐞𝐫 ⊢! pⱽ
⊢ 𝐕𝐞𝐫 ⊢! p

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
d₂ : 𝐕𝐞𝐫 ⊢! pⱽ
⊢ 𝐕𝐞𝐫 ⊢! p
Tactic:
exact d₁ ⨀ d₂
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
d₁ : 𝐕𝐞𝐫 ⊢! pⱽ ⟶ p
⊢ 𝐕𝐞𝐫 ⊢! pⱽ
Tactic:
simpa using of_classical h
State after:
no goals