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

State before:
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
⊢ 𝐂𝐥 ⊢! p → m𝓓 ⊢! pᴹ
Tactic:
intro h
State after:
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p
⊢ m𝓓 ⊢! pᴹ

State before:
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p
⊢ m𝓓 ⊢! pᴹ
Tactic:
induction h.some with
| eaxm ih =>
  simp_all;
  rcases ih with (efq | lem);
  . obtain ⟨q, e⟩ := efq; subst_vars; exact efq!;
  . obtain ⟨q, e⟩ := lem; subst_vars; exact lem!;
| mdp h₁ h₂ ih₁ ih₂ =>
  dsimp only [Superintuitionistic.Formula.toModalFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| _ =>
  dsimp [Superintuitionistic.Formula.toModalFormula];
  try first
  | apply verum!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply imply₁!;
  | apply imply₂!;
State after:
no goals

State before:
case eaxm
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
ih : p✝ ∈ Ax(𝐂𝐥)
h : 𝐂𝐥 ⊢! p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
simp_all
State after:
case eaxm
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
ih : (∃ p, Axioms.EFQ p = p✝) ∨ ∃ p, Axioms.LEM p = p✝
h : 𝐂𝐥 ⊢! p✝
⊢ m𝓓 ⊢! p✝ᴹ

State before:
case eaxm
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
ih : (∃ p, Axioms.EFQ p = p✝) ∨ ∃ p, Axioms.LEM p = p✝
h : 𝐂𝐥 ⊢! p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
rcases ih with (efq | lem)
State after:
case eaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
efq : ∃ p, Axioms.EFQ p = p✝
⊢ m𝓓 ⊢! p✝ᴹ

case eaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
lem : ∃ p, Axioms.LEM p = p✝
⊢ m𝓓 ⊢! p✝ᴹ

State before:
case eaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
efq : ∃ p, Axioms.EFQ p = p✝
⊢ m𝓓 ⊢! p✝ᴹ

case eaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
lem : ∃ p, Axioms.LEM p = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
. obtain ⟨q, e⟩ := efq; subst_vars; exact efq!;
State after:
case eaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
lem : ∃ p, Axioms.LEM p = p✝
⊢ m𝓓 ⊢! p✝ᴹ

State before:
case eaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
lem : ∃ p, Axioms.LEM p = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
. obtain ⟨q, e⟩ := lem; subst_vars; exact lem!;
State after:
no goals

State before:
case eaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
efq : ∃ p, Axioms.EFQ p = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
obtain ⟨q, e⟩ := efq
State after:
case eaxm.inl.intro
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
q : Superintuitionistic.Formula α
e : Axioms.EFQ q = p✝
⊢ m𝓓 ⊢! p✝ᴹ

State before:
case eaxm.inl.intro
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
q : Superintuitionistic.Formula α
e : Axioms.EFQ q = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
subst_vars
State after:
case eaxm.inl.intro
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p q : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! Axioms.EFQ q
⊢ m𝓓 ⊢! Axioms.EFQ qᴹ

State before:
case eaxm.inl.intro
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p q : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! Axioms.EFQ q
⊢ m𝓓 ⊢! Axioms.EFQ qᴹ
Tactic:
exact efq!
State after:
no goals

State before:
case eaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
lem : ∃ p, Axioms.LEM p = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
obtain ⟨q, e⟩ := lem
State after:
case eaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
q : Superintuitionistic.Formula α
e : Axioms.LEM q = p✝
⊢ m𝓓 ⊢! p✝ᴹ

State before:
case eaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝
q : Superintuitionistic.Formula α
e : Axioms.LEM q = p✝
⊢ m𝓓 ⊢! p✝ᴹ
Tactic:
subst_vars
State after:
case eaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p q : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! Axioms.LEM q
⊢ m𝓓 ⊢! Axioms.LEM qᴹ

State before:
case eaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p q : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! Axioms.LEM q
⊢ m𝓓 ⊢! Axioms.LEM qᴹ
Tactic:
exact lem!
State after:
no goals

State before:
case mdp
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h₁ : Superintuitionistic.Deduction 𝐂𝐥 (p✝ ⟶ q✝)
h₂ : Superintuitionistic.Deduction 𝐂𝐥 p✝
ih₁ : 𝐂𝐥 ⊢! p✝ ⟶ q✝ → m𝓓 ⊢! (p✝ ⟶ q✝)ᴹ
ih₂ : 𝐂𝐥 ⊢! p✝ → m𝓓 ⊢! p✝ᴹ
h : 𝐂𝐥 ⊢! q✝
⊢ m𝓓 ⊢! q✝ᴹ
Tactic:
dsimp only [Superintuitionistic.Formula.toModalFormula] at ih₁ ih₂
State after:
case mdp
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h₁ : Superintuitionistic.Deduction 𝐂𝐥 (p✝ ⟶ q✝)
h₂ : Superintuitionistic.Deduction 𝐂𝐥 p✝
ih₁ : 𝐂𝐥 ⊢! p✝ ⟶ q✝ → m𝓓 ⊢! p✝ᴹ ⟶ q✝ᴹ
ih₂ : 𝐂𝐥 ⊢! p✝ → m𝓓 ⊢! p✝ᴹ
h : 𝐂𝐥 ⊢! q✝
⊢ m𝓓 ⊢! q✝ᴹ

State before:
case mdp
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h₁ : Superintuitionistic.Deduction 𝐂𝐥 (p✝ ⟶ q✝)
h₂ : Superintuitionistic.Deduction 𝐂𝐥 p✝
ih₁ : 𝐂𝐥 ⊢! p✝ ⟶ q✝ → m𝓓 ⊢! p✝ᴹ ⟶ q✝ᴹ
ih₂ : 𝐂𝐥 ⊢! p✝ → m𝓓 ⊢! p✝ᴹ
h : 𝐂𝐥 ⊢! q✝
⊢ m𝓓 ⊢! q✝ᴹ
Tactic:
exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩)
State after:
no goals

State before:
case disj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ m𝓓 ⊢! ((p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝)ᴹ
Tactic:
dsimp [Superintuitionistic.Formula.toModalFormula]
State after:
case disj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ m𝓓 ⊢! (p✝ᴹ ⟶ r✝ᴹ) ⟶ (q✝ᴹ ⟶ r✝ᴹ) ⟶ p✝ᴹ ⋎ q✝ᴹ ⟶ r✝ᴹ

State before:
case disj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ m𝓓 ⊢! (p✝ᴹ ⟶ r✝ᴹ) ⟶ (q✝ᴹ ⟶ r✝ᴹ) ⟶ p✝ᴹ ⋎ q✝ᴹ ⟶ r✝ᴹ
Tactic:
try first
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
State after:
no goals

State before:
case disj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ m𝓓 ⊢! (p✝ᴹ ⟶ r✝ᴹ) ⟶ (q✝ᴹ ⟶ r✝ᴹ) ⟶ p✝ᴹ ⋎ q✝ᴹ ⟶ r✝ᴹ
Tactic:
first
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
State after:
no goals

State before:
case verum
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! ⊤
⊢ m𝓓 ⊢! ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case conj₁
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ m𝓓 ⊢! p✝ᴹ ⋏ q✝ᴹ ⟶ p✝ᴹ
Tactic:
apply conj₁!
State after:
no goals

State before:
case conj₂
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ m𝓓 ⊢! p✝ᴹ ⋏ q✝ᴹ ⟶ q✝ᴹ
Tactic:
apply conj₂!
State after:
no goals

State before:
case conj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ m𝓓 ⊢! p✝ᴹ ⟶ q✝ᴹ ⟶ p✝ᴹ ⋏ q✝ᴹ
Tactic:
apply conj₃!
State after:
no goals

State before:
case disj₁
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ m𝓓 ⊢! p✝ᴹ ⟶ p✝ᴹ ⋎ q✝ᴹ
Tactic:
apply disj₁!
State after:
no goals

State before:
case disj₂
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ m𝓓 ⊢! q✝ᴹ ⟶ p✝ᴹ ⋎ q✝ᴹ
Tactic:
apply disj₂!
State after:
no goals

State before:
case disj₃
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ m𝓓 ⊢! (p✝ᴹ ⟶ r✝ᴹ) ⟶ (q✝ᴹ ⟶ r✝ᴹ) ⟶ p✝ᴹ ⋎ q✝ᴹ ⟶ r✝ᴹ
Tactic:
apply disj₃!
State after:
no goals

State before:
case imply₁
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ m𝓓 ⊢! p✝ᴹ ⟶ q✝ᴹ ⟶ p✝ᴹ
Tactic:
apply imply₁!
State after:
no goals

State before:
case imply₂
α : Type u_1
inst✝ : DecidableEq α
p✝¹ : Formula α
m𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ m𝓓 ⊢! (p✝ᴹ ⟶ q✝ᴹ ⟶ r✝ᴹ) ⟶ (p✝ᴹ ⟶ q✝ᴹ) ⟶ p✝ᴹ ⟶ r✝ᴹ
Tactic:
apply imply₂!
State after:
no goals