Theorem: LO.Modal.Standard.axiomTc_GTranslate! (Logic/Modal/Standard/Kripke/ModalCompanion.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! pᵍ ⟶ □pᵍ
Tactic:
induction p using Superintuitionistic.Formula.rec' with
| hatom => simp only [GoedelTranslation.atom_def, axiomFour!];
| himp => simp only [GoedelTranslation.imp_def, axiomFour!];
| hfalsum => simp only [GoedelTranslation.falsum_def, efq!];
| hverum => exact dhyp! (nec! verum!);
| hand p q ihp ihq =>
  simp only [GoedelTranslation.and_def];
  exact imp_trans! (andReplace! ihp ihq) collect_box_and!
| hor p q ihp ihq =>
  simp only [GoedelTranslation.or_def];
  exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
State after:
no goals

State before:
case hatom
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
a✝ : α
⊢ m𝓓 ⊢! Superintuitionistic.Formula.atom a✝ᵍ ⟶ □Superintuitionistic.Formula.atom a✝ᵍ
Tactic:
simp only [GoedelTranslation.atom_def, axiomFour!]
State after:
no goals

State before:
case himp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p✝ q✝ : Superintuitionistic.Formula α
a✝¹ : m𝓓 ⊢! p✝ᵍ ⟶ □p✝ᵍ
a✝ : m𝓓 ⊢! q✝ᵍ ⟶ □q✝ᵍ
⊢ m𝓓 ⊢! (p✝ ⟶ q✝)ᵍ ⟶ □(p✝ ⟶ q✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, axiomFour!]
State after:
no goals

State before:
case hfalsum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! ⊥ᵍ ⟶ □⊥ᵍ
Tactic:
simp only [GoedelTranslation.falsum_def, efq!]
State after:
no goals

State before:
case hverum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! ⊤ᵍ ⟶ □⊤ᵍ
Tactic:
exact dhyp! (nec! verum!)
State after:
no goals

State before:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! (p ⋏ q)ᵍ ⟶ □(p ⋏ q)ᵍ
Tactic:
simp only [GoedelTranslation.and_def]
State after:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋏ qᵍ ⟶ □(pᵍ ⋏ qᵍ)

State before:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋏ qᵍ ⟶ □(pᵍ ⋏ qᵍ)
Tactic:
exact imp_trans! (andReplace! ihp ihq) collect_box_and!
State after:
no goals

State before:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! (p ⋎ q)ᵍ ⟶ □(p ⋎ q)ᵍ
Tactic:
simp only [GoedelTranslation.or_def]
State after:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ ⟶ □(pᵍ ⋎ qᵍ)

State before:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ ⟶ □(pᵍ ⋎ qᵍ)
Tactic:
exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
State after:
no goals