internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
Tactic:
induction p using Formula.rec' with
| hbox p ih =>
  simp [TrivTranslation];
  apply iff_intro!;
  . exact imp_trans! axiomT! (conj₁'! ih)
  . exact imp_trans! (conj₂'! ih) axiomTc!
| himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂;
| hand _ _ ih₁ ih₂ => exact and_replace_iff! ih₁ ih₂;
| hor _ _ ih₁ ih₂ => exact or_replace_iff! ih₁ ih₂;
| _ => apply iff_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ (□p)ᵀ
Tactic:
simp [TrivTranslation]
Proof state after:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ pᵀ
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ pᵀ
Tactic:
apply iff_intro!
Proof state after:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
. exact imp_trans! axiomT! (conj₁'! ih)
Proof state after:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
. exact imp_trans! (conj₂'! ih) axiomTc!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ
Tactic:
exact imp_trans! axiomT! (conj₁'! ih)
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
exact imp_trans! (conj₂'! ih) axiomTc!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! (p✝ ⟶ q✝) ⟷ (p✝ ⟶ q✝)ᵀ
Tactic:
exact imp_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋏ q✝ ⟷ (p✝ ⋏ q✝)ᵀ
Tactic:
exact and_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋎ q✝ ⟷ (p✝ ⋎ q✝)ᵀ
Tactic:
exact or_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_trivTranslation
Proof state before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐓𝐫𝐢𝐯 ⊢! atom a✝ ⟷ atom a✝ᵀ
Tactic:
apply iff_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ⟷ pⱽ
Tactic:
induction p using Formula.rec' with
| hbox =>
  apply iff_intro!;
  . exact imply₁'! verum!
  . exact dhyp! (by simp)
| himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂;
| hand _ _ ih₁ ih₂ => exact and_replace_iff! ih₁ ih₂;
| hor _ _ ih₁ ih₂ => exact or_replace_iff! ih₁ ih₂;
| _ => apply iff_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟷ (□p✝)ⱽ
Tactic:
apply iff_intro!
Proof state after:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
. exact imply₁'! verum!
Proof state after:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
. exact dhyp! (by simp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ
Tactic:
exact imply₁'! verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
exact dhyp! (by simp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
ih₂ : 𝐕𝐞𝐫 ⊢! q✝ ⟷ q✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (p✝ ⟶ q✝) ⟷ (p✝ ⟶ q✝)ⱽ
Tactic:
exact imp_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
ih₂ : 𝐕𝐞𝐫 ⊢! q✝ ⟷ q✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! p✝ ⋏ q✝ ⟷ (p✝ ⋏ q✝)ⱽ
Tactic:
exact and_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
ih₂ : 𝐕𝐞𝐫 ⊢! q✝ ⟷ q✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! p✝ ⋎ q✝ ⟷ (p✝ ⋎ q✝)ⱽ
Tactic:
exact or_replace_iff! ih₁ ih₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.deducible_iff_verTranslation
Proof state before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐕𝐞𝐫 ⊢! atom a✝ ⟷ atom a✝ⱽ
Tactic:
apply iff_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
⊢ 𝐂𝐥 ⊢! p → m𝓓 ⊢! pᴹ
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p
⊢ m𝓓 ⊢! pᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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)
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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!;
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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
Proof 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ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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
Proof 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ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₂
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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₂⟩)
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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]
Proof 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✝ᴹ
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof state before:
case verum
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! ⊤
⊢ m𝓓 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.of_classical
Proof 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₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_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_Triv_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 | hT) | hTc;
    . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, TrivTranslation, toPropFormula]; apply imp_id!;
    . obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, TrivTranslation, toPropFormula]; apply imp_id!;
    . obtain ⟨_, e⟩ := hTc; subst_vars; dsimp [Axioms.Tc, TrivTranslation, toPropFormula]; apply imp_id!;
  | hMdp h₁ h₂ ih₁ ih₂ =>
    dsimp [TrivTranslation, toPropFormula] at ih₁ ih₂;
    exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
  | hNec _ ih => exact ih $ axiomT'! h;
  | _ =>
    dsimp [TrivTranslation, toPropFormula];
    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:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯ → 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.iff_Triv_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_trivTranslation;
  have d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ := by simpa only [TrivTranslation.back] using of_classical h;
  exact d₁ ⨀ d₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_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_Triv_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 | hT) | hTc;
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, TrivTranslation, toPropFormula]; apply imp_id!;
  . obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, TrivTranslation, toPropFormula]; apply imp_id!;
  . obtain ⟨_, e⟩ := hTc; subst_vars; dsimp [Axioms.Tc, TrivTranslation, toPropFormula]; apply imp_id!;
| hMdp h₁ h₂ ih₁ ih₂ =>
  dsimp [TrivTranslation, toPropFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| hNec _ ih => exact ih $ axiomT'! h;
| _ =>
  dsimp [TrivTranslation, toPropFormula];
  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.hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐓𝐫𝐢𝐯)
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
rcases a with (hK | hT) | hTc
Proof state after:
case mp.hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯

case mp.hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯

case mp.hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, TrivTranslation, toPropFormula]; apply imp_id!;
Proof state after:
case mp.hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
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✝ᵀᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
. obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, TrivTranslation, toPropFormula]; apply imp_id!;
Proof state after:
case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hTc : p✝ ∈ 𝗧𝗰
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
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; subst_vars; dsimp [Axioms.Tc, TrivTranslation, toPropFormula]; apply imp_id!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.iff_Triv_classical
Proof state before:
case mp.hMaxm.inl.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.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯