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

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐆𝐋 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
intro h
State after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯

State before:
α : 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]; apply imp_id!;
  | 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 hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐆𝐋)
h : 𝐆𝐋 ⊢! p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
rcases a with (hK | hVer)
State after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

State before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case 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 hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

State before:
case 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]; apply imp_id!;
State after:
no goals

State before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, _, e⟩ := hK
State after:
case 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 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 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 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 hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤

State before:
case 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 hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hVer
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
subst_vars
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! (Axioms.L w✝ⱽᴾ) ⋯

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! (Axioms.L w✝ⱽᴾ) ⋯
Tactic:
dsimp [Axioms.Ver, VerTranslation, toPropFormula]
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤
Tactic:
apply imp_id!
State after:
no goals

State before:
case 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 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 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 hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ⱽᴾ) ⋯
Tactic:
dsimp [toPropFormula]
State after:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤

State before:
case 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 hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula]
State after:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯

State before:
case 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 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 hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! ⊤
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case 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 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 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 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 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 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 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 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 hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply dne!
State after:
no goals