Theorem: LO.Modal.Standard.iff_Triv_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 | 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!;
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_trivTranslation;
  have d₂ : 𝐓𝐫𝐢𝐯 ⊢! pᵀ := by simpa only [TrivTranslation.back] 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 | 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!;
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 | hT) | hTc
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✝ᵀᴾ) ⋯

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!;
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✝ᵀᴾ) ⋯

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

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

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

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

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

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

State before:
case mp.hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hT
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✝ᵀᴾ) ⋯

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
State after:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (Axioms.T w✝ᵀᴾ) ⋯

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]
State after:
case mp.hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.T w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯

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

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

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

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]
State after:
case mp.hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! Axioms.Tc w✝
⊢ 𝐂𝐥 ⊢! (w✝ᵀᴾ) ⋯ ⟶ (w✝ᵀᴾ) ⋯

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!
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 [TrivTranslation, 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✝
ih : 𝐓𝐫𝐢𝐯 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ᵀᴾ) ⋯
h : 𝐓𝐫𝐢𝐯 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ᵀᴾ) ⋯
Tactic:
exact ih $ axiomT'! h
State after:
no goals

State before:
case mp.hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ᵀᴾ) ⋯
Tactic:
dsimp [TrivTranslation, 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 imp_id!;
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| 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 imp_id!;
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| 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.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.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.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_trivTranslation
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 only [TrivTranslation.back] 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 only [TrivTranslation.back] using of_classical h
State after:
no goals