From 66bc3f9e8aaa622882c1193136be5ed8934e94e2 Mon Sep 17 00:00:00 2001
From: Metin Ersin Arican <metin.ersin.arican@gmail.com>
Date: Thu, 3 Oct 2024 22:48:50 +0300
Subject: [PATCH] resolve comments

---
 Mathlib/ModelTheory/Complexity.lean  | 16 ++++++++--------
 Mathlib/ModelTheory/Equivalence.lean |  9 +--------
 2 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/Mathlib/ModelTheory/Complexity.lean b/Mathlib/ModelTheory/Complexity.lean
index 162a25fe063f0..dfebf6bf99599 100644
--- a/Mathlib/ModelTheory/Complexity.lean
+++ b/Mathlib/ModelTheory/Complexity.lean
@@ -15,8 +15,8 @@ prenex normal forms.
 
 - `FirstOrder.Language.BoundedFormula.IsAtomic` defines atomic formulas - those which are
   constructed only from terms and relations.
-- `FirstOrder.Language.BoundedFormula.IsLiteral` defines literals - those which are `⊥`, `⊤`,
-  atomic formulas or negation of atomic formulas.
+- `FirstOrder.Language.BoundedFormula.IsLiteral`: Predicate for a formula to be a literal, namely of
+  the form `⊥`, `⊤`, atomic formulas or negation of atomic formulas.
 - `FirstOrder.Language.BoundedFormula.IsQF` defines quantifier-free formulas - those which are
   constructed only from atomic formulas and boolean operations.
 - `FirstOrder.Language.BoundedFormula.IsPrenex` defines when a formula is in prenex normal form -
@@ -47,10 +47,10 @@ prenex normal forms.
   normal form of a formula is semantically equivalent to the original formula.
 - `FirstOrder.Language.BoundedFormula.toCNF_semanticallyEquivalent` shows that the conjunctive
   normal form of a formula is semantically equivalent to the original formula.
-- `FirstOrder.Language.BoundedFormula.IsDNF.components` which gives the literals of a DNF as
-  a list of lists.
-- `FirstOrder.Language.BoundedFormula.IsCNF.components` which gives the literals of a CNF as
-  a list of lists.
+- `FirstOrder.Language.BoundedFormula.IsDNF.components` gives the literals of a DNF as a list of
+  lists.
+- `FirstOrder.Language.BoundedFormula.IsCNF.components` gives the literals of a CNF as a list of
+  lists.
 -/
 
 universe u v w u' v'
@@ -69,7 +69,7 @@ open FirstOrder Structure Fin
 
 namespace BoundedFormula
 
-/-- An auxilary operation which is semantically equivalent to
+/-- An auxiliary operation which is semantically equivalent to
   `FirstOrder.Language.BoundedFormula.not`. It takes a bounded formula `φ`, assuming any negation
   symbol inside `φ` occurs in front of an atomic formula or `⊥`, it applies negation to `φ`, pushes
   the negation inwards through `⊓`, `⊔`, `∀'`, `∃'`, and eliminates double negations. -/
@@ -112,7 +112,7 @@ theorem realize_simpleNot {n : ℕ} (φ : L.BoundedFormula α n) {v : α → M}
   · rfl
 
 theorem simpleNot_semanticallyEquivalent_not {T : L.Theory} {n : ℕ} (φ : L.BoundedFormula α n) :
-    (φ.simpleNot ⇔[T] φ.not) := by
+    φ.simpleNot ⇔[T] φ.not := by
   simp only [Theory.Iff, Theory.ModelsBoundedFormula, realize_iff,
     realize_simpleNot, realize_not, implies_true]
 
diff --git a/Mathlib/ModelTheory/Equivalence.lean b/Mathlib/ModelTheory/Equivalence.lean
index 3c6209d9d9be9..2d6e172ddb0b4 100644
--- a/Mathlib/ModelTheory/Equivalence.lean
+++ b/Mathlib/ModelTheory/Equivalence.lean
@@ -194,13 +194,6 @@ protected theorem imp {φ ψ φ' ψ' : L.BoundedFormula α n} (h : φ ⇔[T] ψ)
     BoundedFormula.realize_imp]
   exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff
 
-protected theorem sup {φ ψ φ' ψ' : L.BoundedFormula α n}
-    (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
-    (φ ⊔ φ') ⇔[T] (ψ ⊔ ψ') := by
-  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
-    BoundedFormula.realize_sup]
-  exact fun M v xs => or_congr h.realize_bd_iff h'.realize_bd_iff
-
 protected theorem inf {φ ψ φ' ψ' : L.BoundedFormula α n}
     (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
     (φ ⊓ φ') ⇔[T] (ψ ⊓ ψ') := by
@@ -230,7 +223,7 @@ theorem imp_iff_not_sup : (φ.imp ψ) ⇔[T] (φ.not ⊔ ψ) :=
 theorem sup_iff_not_inf_not : (φ ⊔ ψ) ⇔[T] (φ.not ⊓ ψ.not).not :=
   fun M v xs => by simp [imp_iff_not_or]
 
-theorem not_sup_semanticallyEquivalent_inf_not : (φ ⊔ ψ).not ⇔[T] (φ.not ⊓ ψ.not) :=
+theorem not_sup_iff_inf_not : (φ ⊔ ψ).not ⇔[T] φ.not ⊓ ψ.not :=
   fun M v xs => by simp [imp_iff_not_or]
 
 theorem inf_iff_not_sup_not : (φ ⊓ ψ) ⇔[T] (φ.not ⊔ ψ.not).not :=