chore: fix reducibility setting for lattice copy (#37895)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/CategoryTheory/Sites/Grothendieck.lean

@@ -306,7 +306,7 @@ theorem isGLB_sInf (s : Set (GrothendieckTopology C)) : IsGLB s (sInf s) := by
 definitionally equal to the bottom and top respectively.
 -/
 instance : CompleteLattice (GrothendieckTopology C) :=
-  CompleteLattice.copy (completeLatticeOfInf _ isGLB_sInf) _ rfl (discrete C)
+  fast_instance% CompleteLattice.copy (completeLatticeOfInf _ isGLB_sInf) _ rfl (discrete C)
     (by
       apply le_antisymm
       · exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)

Mathlib/Order/Copy.lean

@@ -24,39 +24,35 @@ universe u
 
 variable {α : Type u}
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a top order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def OrderTop.copy {h : LE α} {h' : LE α} (c : @OrderTop α h')
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderTop α h :=
   @OrderTop.mk α h { top := top } fun _ ↦ by simp [eq_top, le_eq]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bottom order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def OrderBot.copy {h : LE α} {h' : LE α} (c : @OrderBot α h')
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderBot α h :=
   @OrderBot.mk α h { bot := bot } fun _ ↦ by simp [eq_bot, le_eq]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bounded order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def BoundedOrder.copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h')
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h :=
   @BoundedOrder.mk α h (@OrderTop.mk α h { top := top } (fun _ ↦ by simp [eq_top, le_eq]))
     (@OrderBot.mk α h { bot := bot } (fun _ ↦ by simp [eq_bot, le_eq]))
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def Lattice.copy (c : Lattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
@@ -75,23 +71,19 @@ def Lattice.copy (c : Lattice α)
   inf_le_right := by intros; simp [eq_le, eq_inf]
   le_inf := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_inf, hac, hbc]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a distributive lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def DistribLattice.copy (c : DistribLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
     (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) : DistribLattice α where
   toLattice := Lattice.copy (@DistribLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
   le_sup_inf := by intros; simp +instances [eq_le, eq_sup, eq_inf, le_sup_inf]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a generalised heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -105,11 +97,9 @@ def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
   himp := himp
   le_himp_iff _ _ _ := by simp +instances [eq_le, eq_himp, eq_inf]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a generalised co-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -123,11 +113,9 @@ def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
   sdiff := sdiff
   sdiff_le_iff := by simp +instances [eq_le, eq_sdiff, eq_sup]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def HeytingAlgebra.copy (c : HeytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -145,11 +133,9 @@ def HeytingAlgebra.copy (c : HeytingAlgebra α)
   compl := compl
   himp_bot := by simp +instances [eq_le, eq_himp, eq_bot, eq_compl]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a co-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -167,10 +153,9 @@ def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
   hnot := hnot
   top_sdiff := by simp +instances [eq_le, eq_sdiff, eq_top, eq_hnot]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bi-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -187,11 +172,9 @@ def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
   __ := CoheytingAlgebra.copy (@BiheytingAlgebra.toCoheytingAlgebra α c) le eq_le top eq_top bot
     eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a complete lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CompleteLattice.copy (c : CompleteLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -211,10 +194,9 @@ def CompleteLattice.copy (c : CompleteLattice α)
   le_top := by intros; simp +instances [eq_le, eq_top]
   bot_le := by intros; simp +instances [eq_le, eq_bot]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a frame with possibly different definitional
 equalities. -/
+@[implicit_reducible]
 def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -229,10 +211,9 @@ def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_
   __ := HeytingAlgebra.copy (@Frame.toHeytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a coframe with possibly different definitional
 equalities. -/
+@[implicit_reducible]
 def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -247,10 +228,9 @@ def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by in
   __ := CoheytingAlgebra.copy (@Coframe.toCoheytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a complete distributive lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CompleteDistribLattice.copy (c : CompleteDistribLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -269,10 +249,9 @@ def CompleteDistribLattice.copy (c : CompleteDistribLattice α)
   __ := Coframe.copy (@CompleteDistribLattice.toCoframe α c) le eq_le top eq_top bot eq_bot sup
     eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot sSup eq_sSup sInf eq_sInf
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a conditionally complete lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def ConditionallyCompleteLattice.copy (c : ConditionallyCompleteLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)

Mathlib/Topology/Sets/Closeds.lean

@@ -45,7 +45,7 @@ instance : SetLike (Closeds α) α where
   coe := Closeds.carrier
   coe_injective' s t h := by cases s; cases t; congr
 
-instance : PartialOrder (Closeds α) := .ofSetLike (Closeds α) α
+instance : PartialOrder (Closeds α) := fast_instance% .ofSetLike (Closeds α) α
 
 instance : CanLift (Set α) (Closeds α) (↑) IsClosed where
   prf s hs := ⟨⟨s, hs⟩, rfl⟩
@@ -96,7 +96,7 @@ def gi : GaloisInsertion (@Closeds.closure α _) (↑) where
   choice_eq _s hs := SetLike.coe_injective <| subset_closure.antisymm hs
 
 instance instCompleteLattice : CompleteLattice (Closeds α) :=
-  CompleteLattice.copy
+  fast_instance% CompleteLattice.copy
     (GaloisInsertion.liftCompleteLattice gi)
     -- le
     _ rfl
@@ -188,7 +188,7 @@ def coframeMinimalAxioms : Coframe.MinimalAxioms (Closeds α) where
   iInf_sup_le_sup_sInf a s :=
     (SetLike.coe_injective <| by simp only [coe_sup, coe_iInf, coe_sInf, Set.union_iInter₂]).le
 
-instance instCoframe : Coframe (Closeds α) := .ofMinimalAxioms coframeMinimalAxioms
+instance instCoframe : Coframe (Closeds α) := fast_instance% .ofMinimalAxioms coframeMinimalAxioms
 
 @[simps]
 instance [T1Space α] : Singleton α (Closeds α) where
@@ -282,26 +282,22 @@ def Opens.complOrderIso : Opens α ≃o (Closeds α)ᵒᵈ where
 
 variable {α}
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Closeds.coe_eq_singleton_of_isAtom [T0Space α] {s : Closeds α} (hs : IsAtom s) :
     ∃ a, (s : Set α) = {a} := by
   refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_
   lift t to Closeds α using ht'
   exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast] lemma Closeds.isAtom_coe [T1Space α] {s : Closeds α} :
     IsAtom (s : Set α) ↔ IsAtom s :=
   Closeds.gi.isAtom_iff' rfl
     (fun t ht ↦ by obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht; exact closure_singleton) s
 
-set_option backward.isDefEq.respectTransparency false in
 /-- in a `T1Space`, atoms of `TopologicalSpace.Closeds α` are precisely the singletons. -/
 theorem Closeds.isAtom_iff [T1Space α] {s : Closeds α} :
     IsAtom s ↔ ∃ x, s = {x} := by
   simp [← Closeds.isAtom_coe, Set.isAtom_iff, SetLike.ext_iff, Set.ext_iff]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- in a `T1Space`, coatoms of `TopologicalSpace.Opens α` are precisely complements of singletons:
 `({x} : Closeds α).compl`. -/
 theorem Opens.isCoatom_iff [T1Space α] {s : Opens α} :
@@ -326,7 +322,7 @@ instance : SetLike (Clopens α) α where
   coe s := s.carrier
   coe_injective' s t h := by cases s; cases t; congr
 
-instance : PartialOrder (Clopens α) := .ofSetLike (Clopens α) α
+instance : PartialOrder (Clopens α) := fast_instance% .ofSetLike (Clopens α) α
 
 theorem isClopen (s : Clopens α) : IsClopen (s : Set α) :=
   s.isClopen'
@@ -372,7 +368,7 @@ instance : Compl (Clopens α) := ⟨fun s => ⟨sᶜ, s.isClopen.compl⟩⟩
 @[simp, norm_cast] lemma coe_himp (s t : Clopens α) : ↑(s ⇨ t) = (s ⇨ t : Set α) := rfl
 @[simp, norm_cast] lemma coe_compl (s : Clopens α) : (↑sᶜ : Set α) = (↑s)ᶜ := rfl
 
-instance : BooleanAlgebra (Clopens α) :=
+instance : BooleanAlgebra (Clopens α) := fast_instance%
   SetLike.coe_injective.booleanAlgebra _ .rfl .rfl coe_sup coe_inf coe_top coe_bot coe_compl
     coe_sdiff coe_himp
 
@@ -414,7 +410,7 @@ instance : SetLike (IrreducibleCloseds α) α where
   coe := IrreducibleCloseds.carrier
   coe_injective' s t h := by cases s; cases t; congr
 
-instance : PartialOrder (IrreducibleCloseds α) := .ofSetLike (IrreducibleCloseds α) α
+instance : PartialOrder (IrreducibleCloseds α) := fast_instance% .ofSetLike (IrreducibleCloseds α) α
 
 instance : CanLift (Set α) (IrreducibleCloseds α) (↑) (fun s ↦ IsIrreducible s ∧ IsClosed s) where
   prf s hs := ⟨⟨s, hs.1, hs.2⟩, rfl⟩

Mathlib/Topology/Sets/Opens.lean

@@ -72,7 +72,7 @@ instance : SetLike (Opens α) α where
   coe := Opens.carrier
   coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ _ => by congr
 
-instance : PartialOrder (Opens α) := .ofSetLike (Opens α) α
+instance : PartialOrder (Opens α) := fast_instance% .ofSetLike (Opens α) α
 
 instance : CanLift (Set α) (Opens α) (↑) IsOpen :=
   ⟨fun s h => ⟨⟨s, h⟩, rfl⟩⟩
@@ -139,7 +139,7 @@ def gi : GaloisCoinsertion (↑) (@Opens.interior α _) where
   choice_eq _s hs := le_antisymm hs interior_subset
 
 instance : CompleteLattice (Opens α) :=
-  CompleteLattice.copy (GaloisCoinsertion.liftCompleteLattice gi)
+  fast_instance% CompleteLattice.copy (GaloisCoinsertion.liftCompleteLattice gi)
     -- le
     (fun U V => (U : Set α) ⊆ V) rfl
     -- top
@@ -215,7 +215,6 @@ theorem coe_finset_sup (f : ι → Opens α) (s : Finset ι) : (↑(s.sup f) : S
 theorem coe_finset_inf (f : ι → Opens α) (s : Finset ι) : (↑(s.inf f) : Set α) = s.inf ((↑) ∘ f) :=
   map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Opens α) (Set α)) _ _
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_disjoint {s t : Opens α} : Disjoint (s : Set α) t ↔ Disjoint s t := by
   simp [disjoint_iff, ← SetLike.coe_set_eq]
@@ -249,14 +248,13 @@ theorem mem_iSup {ι} {x : α} {s : ι → Opens α} : x ∈ iSup s ↔ ∃ i, x
 theorem mem_sSup {Us : Set (Opens α)} {x : α} : x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u := by
   simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- Open sets in a topological space form a frame. -/
+@[implicit_reducible]
 def frameMinimalAxioms : Frame.MinimalAxioms (Opens α) where
   inf_sSup_le_iSup_inf a s :=
     (ext <| by simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]).le
 
-instance instFrame : Frame (Opens α) := .ofMinimalAxioms frameMinimalAxioms
+instance instFrame : Frame (Opens α) := fast_instance% .ofMinimalAxioms frameMinimalAxioms
 
 /-- The coercion from open sets to sets as a `FrameHom`. -/
 @[simps] protected def frameHom : FrameHom (Opens α) (Set α) where
@@ -275,21 +273,17 @@ theorem isOpenEmbedding_of_le {U V : Opens α} (i : U ≤ V) :
     rw [Set.range_inclusion i]
     exact U.isOpen.preimage continuous_subtype_val
 
-set_option backward.isDefEq.respectTransparency false in
 theorem not_nonempty_iff_eq_bot (U : Opens α) : ¬Set.Nonempty (U : Set α) ↔ U = ⊥ := by
   rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
 
 theorem ne_bot_iff_nonempty (U : Opens α) : U ≠ ⊥ ↔ Set.Nonempty (U : Set α) := by
   rw [Ne, ← not_nonempty_iff_eq_bot, not_not]
 
-set_option backward.isDefEq.respectTransparency false in
-/-- An open set in the indiscrete topology is either empty or the whole space. -/
 theorem eq_bot_or_top [IndiscreteTopology α] (U : Opens α) :
     U = ⊥ ∨ U = ⊤ := by
   rw [← coe_eq_empty, ← coe_eq_univ, ← IndiscreteTopology.isOpen_iff]
   exact U.2
 
-set_option backward.isDefEq.respectTransparency false in
 instance [Nonempty α] [IndiscreteTopology α] : IsSimpleOrder (Opens α) where
   eq_bot_or_eq_top := eq_bot_or_top
 
@@ -367,7 +361,6 @@ lemma IsBasis.of_isInducing {B : Set (Opens β)} (H : IsBasis B) {f : α → β}
   convert H.isInducing h
   ext; simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem isCompactElement_iff (s : Opens α) :
     IsCompactElement s ↔ IsCompact (s : Set α) := by
@@ -457,7 +450,7 @@ instance : SetLike (OpenNhdsOf x) α where
   coe U := U.1
   coe_injective' := SetLike.coe_injective.comp toOpens_injective
 
-instance : PartialOrder (OpenNhdsOf x) := .ofSetLike (OpenNhdsOf x) α
+instance : PartialOrder (OpenNhdsOf x) := fast_instance% .ofSetLike (OpenNhdsOf x) α
 
 instance canLiftSet : CanLift (Set α) (OpenNhdsOf x) (↑) fun s => IsOpen s ∧ x ∈ s :=
   ⟨fun s hs => ⟨⟨⟨s, hs.1⟩, hs.2⟩, rfl⟩⟩
@@ -479,7 +472,7 @@ instance : Max (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊔ V.1, Or.inl U.2⟩⟩
 instance [Subsingleton α] : Unique (OpenNhdsOf x) where
   uniq U := SetLike.ext' <| Subsingleton.eq_univ_of_nonempty ⟨x, U.mem⟩
 
-instance : DistribLattice (OpenNhdsOf x) :=
+instance : DistribLattice (OpenNhdsOf x) := fast_instance%
   toOpens_injective.distribLattice _ .rfl .rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl
 
 theorem basis_nhds : (𝓝 x).HasBasis (fun _ : OpenNhdsOf x => True) (↑) :=