things that'd been moved to Defs

Mathlib/GroupTheory/Congruence/Basic.lean

@@ -73,47 +73,6 @@ protected def congr {c d : Con M} (h : c = d) : c.Quotient ≃* d.Quotient :=
 theorem congr_mk {c d : Con M} (h : c = d) (a : M) :
     Con.congr h (a : c.Quotient) = (a : d.Quotient) := rfl
 
--- The complete lattice of congruence relations on a type
-/-- For congruence relations `c, d` on a type `M` with a multiplication, `c ≤ d` iff `∀ x y ∈ M`,
-    `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
-@[to_additive "For additive congruence relations `c, d` on a type `M` with an addition, `c ≤ d` iff
-`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`."]
-instance : LE (Con M) where
-  le c d := ∀ ⦃x y⦄, c x y → d x y
-
-/-- The infimum of a set of congruence relations on a given type with a multiplication. -/
-@[to_additive "The infimum of a set of additive congruence relations on a given type with
-an addition."]
-instance : InfSet (Con M) where
-  sInf S :=
-    { r := fun x y => ∀ c : Con M, c ∈ S → c x y
-      iseqv := ⟨fun x c _ => c.refl x, fun h c hc => c.symm <| h c hc,
-        fun h1 h2 c hc => c.trans (h1 c hc) <| h2 c hc⟩
-      mul' := fun h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc }
-
-@[to_additive]
-instance : PartialOrder (Con M) where
-  le_refl _ _ _ := id
-  le_trans _ _ _ h1 h2 _ _ h := h2 <| h1 h
-  le_antisymm _ _ hc hd := ext fun _ _ => ⟨fun h => hc h, fun h => hd h⟩
-
-/-- The complete lattice of congruence relations on a given type with a multiplication. -/
-@[to_additive "The complete lattice of additive congruence relations on a given type with
-an addition."]
-instance : CompleteLattice (Con M) where
-  __ := completeLatticeOfInf (Con M) fun s =>
-      ⟨fun r hr x y h => (h : ∀ r ∈ s, (r : Con M) x y) r hr, fun r hr x y h r' hr' =>
-        hr hr'
-          h⟩
-  inf c d := ⟨c.toSetoid ⊓ d.toSetoid, fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩⟩
-  inf_le_left _ _ := fun _ _ h => h.1
-  inf_le_right _ _ := fun _ _ h => h.2
-  le_inf  _ _ _ hb hc := fun _ _ h => ⟨hb h, hc h⟩
-  top := { Setoid.completeLattice.top with mul' := by tauto }
-  le_top _ := fun _ _ _ => trivial
-  bot := { Setoid.completeLattice.bot with mul' := fun h1 h2 => h1 ▸ h2 ▸ rfl }
-  bot_le c := fun x y h => h ▸ c.refl x
-
 @[to_additive]
 theorem comap_conGen_of_Bijective {M N : Type*} [Mul M] [Mul N] (f : M → N)
     (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :