chore(Algebra/Module): remove some backward.privateInPublic

Author: wwylele

Mathlib/Algebra/Module/GradedModule.lean

@@ -104,7 +104,6 @@ theorem of_smul_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
 open AddMonoidHom
 
 -- Almost identical to the proof of `direct_sum.one_mul`
-set_option backward.privateInPublic true in
 private theorem one_smul' [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
     (x : ⨁ i, M i) :
     (1 : ⨁ i, A i) • x = x := by
@@ -115,7 +114,6 @@ private theorem one_smul' [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodu
   exact DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)
 
 -- Almost identical to the proof of `direct_sum.mul_assoc`
-set_option backward.privateInPublic true in
 private theorem mul_smul' [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmodule A M]
     (a b : ⨁ i, A i)
     (c : ⨁ i, M i) : (a * b) • c = a • b • c := by
@@ -136,13 +134,11 @@ private theorem mul_smul' [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmo
     DirectSum.of_eq_of_gradedMonoid_eq
       (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The `Module` derived from `gmodule A M`. -/
 instance module [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmodule A M] :
     Module (⨁ i, A i) (⨁ i, M i) where
-  one_smul := one_smul' _ _
-  mul_smul := mul_smul' _ _
+  one_smul := by exact one_smul' _ _
+  mul_smul := by exact mul_smul' _ _
   smul_add r := (smulAddMonoidHom A M r).map_add
   smul_zero r := (smulAddMonoidHom A M r).map_zero
   add_smul r s x := by simp only [smul_def, map_add, AddMonoidHom.add_apply]

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -184,14 +184,6 @@ instance : InfSet (Submodule R M) :=
       add_mem' := by simp +contextual [add_mem]
       smul_mem' := by simp +contextual [smul_mem] }⟩
 
-set_option backward.privateInPublic true in
-private theorem sInf_le' {S : Set (Submodule R M)} {p} : p ∈ S → sInf S ≤ p :=
-  Set.biInter_subset_of_mem
-
-set_option backward.privateInPublic true in
-private theorem le_sInf' {S : Set (Submodule R M)} {p} : (∀ q ∈ S, p ≤ q) → p ≤ sInf S :=
-  Set.subset_iInter₂
-
 protected theorem isGLB_sInf {S : Set (Submodule R M)} : IsGLB S (sInf S) :=
   .of_image SetLike.coe_subset_coe isGLB_biInf
 
@@ -202,22 +194,18 @@ instance : Min (Submodule R M) :=
       add_mem' := by simp +contextual [add_mem]
       smul_mem' := by simp +contextual [smul_mem] }⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
-instance completeLattice : CompleteLattice (Submodule R M) :=
-  { (inferInstance : OrderTop (Submodule R M)),
-    (inferInstance : OrderBot (Submodule R M)) with
-    sup := fun a b ↦ sInf { x | a ≤ x ∧ b ≤ x }
-    le_sup_left := fun _ _ ↦ le_sInf' fun _ ⟨h, _⟩ ↦ h
-    le_sup_right := fun _ _ ↦ le_sInf' fun _ ⟨_, h⟩ ↦ h
-    sup_le := fun _ _ _ h₁ h₂ ↦ sInf_le' ⟨h₁, h₂⟩
-    inf := (· ⊓ ·)
-    le_inf := fun _ _ _ ↦ Set.subset_inter
-    inf_le_left := fun _ _ ↦ Set.inter_subset_left
-    inf_le_right := fun _ _ ↦ Set.inter_subset_right
-    sSup S := sInf {sm | ∀ s ∈ S, s ≤ sm}
-    isLUB_sSup _ := isGLB_upperBounds.mp Submodule.isGLB_sInf
-    isGLB_sInf _ := Submodule.isGLB_sInf }
+instance completeLattice : CompleteLattice (Submodule R M) where
+  sup a b := sInf { x | a ≤ x ∧ b ≤ x }
+  le_sup_left _ _ := Set.subset_iInter₂ fun _ ⟨h, _⟩ ↦ h
+  le_sup_right _ _ := Set.subset_iInter₂ fun _ ⟨_, h⟩ ↦ h
+  sup_le _ _ _ h₁ h₂ := Set.biInter_subset_of_mem ⟨h₁, h₂⟩
+  inf := (· ⊓ ·)
+  le_inf _ _ _ := Set.subset_inter
+  inf_le_left _ _ := Set.inter_subset_left
+  inf_le_right _ _ := Set.inter_subset_right
+  sSup S := sInf {sm | ∀ s ∈ S, s ≤ sm}
+  isLUB_sSup _ := isGLB_upperBounds.mp Submodule.isGLB_sInf
+  isGLB_sInf _ := Submodule.isGLB_sInf
 
 @[simp]
 theorem coe_inf : ↑(p ⊓ q) = (p ∩ q : Set M) :=