fix for review

Logic/Modal/Normal/Deduction.lean

@@ -310,9 +310,8 @@ instance : IsEquiv (Formula α) (· ⟷[Λ, Γ] ·) where
   symm := by apply DeducibleEquivalent.symm
   trans := by apply DeducibleEquivalent.trans
 
-@[simp] lemma bot : (⊥ ⟷[Λ, Γ] ⊥) := by simp [DeducibleEquivalent]; apply iff_intro!; all_goals apply imp_id!
-
-@[simp] lemma top : (⊤ ⟷[Λ, Γ] ⊤) := by simp [DeducibleEquivalent]; apply iff_intro!; all_goals apply imp_id!
+@[simp]
+lemma tauto : p ⟷[Λ, Γ] p := by simp [DeducibleEquivalent]; apply iff_intro!; all_goals apply imp_id!
 
 lemma _root_.Set.subset_insert_insert {α} {s : Set α} {a b} : s ⊆ insert a (insert b s) := by
   have h₁ := Set.subset_insert a s;
@@ -403,10 +402,10 @@ lemma box (h : p ⟷[Λ, ∅] q) : ((□p) ⟷[Λ, Γ] (□q)) := by
   simp_all only [DeducibleEquivalent];
   apply iff_intro!;
   . have d₁ : Γ ⊢ᴹ[Λ]! □(p ⟶ q) := necessitation! (iff_mp'! h);
-    have d₂ : Γ ⊢ᴹ[Λ]! □(p ⟶ q) ⟶ (□p ⟶ □q) := Hilbert.AxiomK! Γ p q;
+    have d₂ : Γ ⊢ᴹ[Λ]! □(p ⟶ q) ⟶ (□p ⟶ □q) := Hilbert.axiomK! Γ p q;
     exact modus_ponens'! d₂ d₁;
   . have d₁ : Γ ⊢ᴹ[Λ]! □(q ⟶ p) := necessitation! (iff_mpr'! h);
-    have d₂ : Γ ⊢ᴹ[Λ]! □(q ⟶ p) ⟶ (□q ⟶ □p) := Hilbert.AxiomK! Γ q p;
+    have d₂ : Γ ⊢ᴹ[Λ]! □(q ⟶ p) ⟶ (□q ⟶ □p) := Hilbert.axiomK! Γ q p;
     exact modus_ponens'! d₂ d₁;
 
 end DeducibleEquivalent

Logic/Modal/Normal/Formula.lean

@@ -236,12 +236,6 @@ prefix:73 "□" => box
 def dia : Context α := Finset.dia Γ
 prefix:73 "◇" => dia
 
-@[deprecated]
-axiom insert_conj {Γ : Context α} {p : Formula α} : (insert p Γ).conj = Γ.conj ⋏ p
-
-@[deprecated]
-axiom insert_disj {Γ : Context α} {p : Formula α} : (insert p Γ).disj = Γ.disj ⋎ p
-
 end Context
 
 end LO.Modal.Normal

Logic/Modal/Normal/HilbertStyle.lean

@@ -66,9 +66,9 @@ variable [Classical Bew]
 
 open HasNecessitation
 
-def necessitation {Γ : Set F} {p} (d : Bew ∅ p) : Γ ⊢ □p := HasNecessitation.necessitation d
+def necessitation {Γ : Set F} {p} (d : (∅ : Set F) ⊢ p) : Γ ⊢ □p := HasNecessitation.necessitation d
 
-def necessitation! {Γ : Set F} {p} (d : Deducible Bew ∅ p) : Γ ⊢! □p := ⟨necessitation d.some⟩
+def necessitation! {Γ : Set F} {p} (d : (∅ : Set F) ⊢! p) : Γ ⊢! □p := ⟨necessitation d.some⟩
 
 open HasBoxedNecessitation
 
@@ -85,19 +85,19 @@ def preboxed_necessitation! {Γ : Set F} {p} (d : Γ.prebox ⊢! p) : Γ ⊢! 
 
 open HasAxiomK
 
-protected def AxiomK (Γ : Set F) (p q) :  Γ ⊢ (AxiomK p q) := HasAxiomK.K Γ p q
-def AxiomK' {Γ : Set F} {p q} (d₁ : Γ ⊢ (□(p ⟶ q))) (d₂ : Γ ⊢ □p) : Γ ⊢ □q := ((Hilbert.AxiomK Γ p q) ⨀ d₁) ⨀ d₂
+protected def axiomK (Γ : Set F) (p q) :  Γ ⊢ (AxiomK p q) := HasAxiomK.K Γ p q
+def axiomK' {Γ : Set F} {p q} (d₁ : Γ ⊢ (□(p ⟶ q))) (d₂ : Γ ⊢ □p) : Γ ⊢ □q := ((Hilbert.axiomK Γ p q) ⨀ d₁) ⨀ d₂
 
-lemma AxiomK! (Γ : Set F) (p q) : Γ ⊢! (AxiomK p q) := ⟨Hilbert.AxiomK Γ p q⟩
+lemma axiomK! (Γ : Set F) (p q) : Γ ⊢! (AxiomK p q) := ⟨Hilbert.axiomK Γ p q⟩
 
 def boxverum (Γ : Set F) : Γ ⊢ □⊤ := necessitation (verum _)
 lemma boxverum! (Γ : Set F) : Γ ⊢! □⊤ := ⟨boxverum Γ⟩
 
 def box_iff' {Γ : Set F} {p q : F} (d : ∅ ⊢ p ⟷ q) : Γ ⊢ (□p ⟷ □q) := by
-  have dp₁ : ∅ ⊢ (□(p ⟶ q) ⟶ (□p ⟶ □q)) := Hilbert.AxiomK ∅ p q;
+  have dp₁ : ∅ ⊢ (□(p ⟶ q) ⟶ (□p ⟶ □q)) := Hilbert.axiomK ∅ p q;
   have dp₂ : ∅ ⊢ (□(p ⟶ q)) := necessitation $ iff_mp' d;
 
-  have dq₁ : ∅ ⊢ (□(q ⟶ p) ⟶ (□q ⟶ □p)) := Hilbert.AxiomK ∅ q p;
+  have dq₁ : ∅ ⊢ (□(q ⟶ p) ⟶ (□q ⟶ □p)) := Hilbert.axiomK ∅ q p;
   have dq₂ : ∅ ⊢ (□(q ⟶ p)) := necessitation $ iff_mpr' d;
 
   exact iff_intro