From 4241610f1b097c6d5e843f6405c689b6a5f85ec3 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 15 Jul 2024 19:14:57 +0200
Subject: [PATCH 1/4] chore(Data/Bool): merge Init.Data.Bool.* into
 Data.Bool.Basic

---
 Mathlib.lean                                  |   2 -
 Mathlib/Analysis/BoxIntegral/Basic.lean       |   2 +-
 Mathlib/Data/Bool/Basic.lean                  | 117 +++++++++++++
 Mathlib/Init/Data/Bool/Basic.lean             |  30 ----
 Mathlib/Init/Data/Bool/Lemmas.lean            | 163 ------------------
 Mathlib/Logic/Equiv/Defs.lean                 |   2 +-
 .../Topology/Category/Profinite/Nobeling.lean |   2 +-
 scripts/noshake.json                          |   4 +-
 8 files changed, 122 insertions(+), 200 deletions(-)
 delete mode 100644 Mathlib/Init/Data/Bool/Basic.lean
 delete mode 100644 Mathlib/Init/Data/Bool/Lemmas.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index a586e4c925eab6..a45a9e58ad5510 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2705,8 +2705,6 @@ import Mathlib.Init.Classical
 import Mathlib.Init.Control.Combinators
 import Mathlib.Init.Control.Lawful
 import Mathlib.Init.Core
-import Mathlib.Init.Data.Bool.Basic
-import Mathlib.Init.Data.Bool.Lemmas
 import Mathlib.Init.Data.Buffer.Parser
 import Mathlib.Init.Data.Fin.Basic
 import Mathlib.Init.Data.Int.Basic
diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean
index f31d14eaab2736..458cbc5b6d3a88 100644
--- a/Mathlib/Analysis/BoxIntegral/Basic.lean
+++ b/Mathlib/Analysis/BoxIntegral/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Filter
 import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Analysis.Oscillation
 import Mathlib.Topology.UniformSpace.Compact
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 
 #align_import analysis.box_integral.basic from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 
diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean
index 50634ac4a6f336..eae9ed88f2ed09 100644
--- a/Mathlib/Data/Bool/Basic.lean
+++ b/Mathlib/Data/Bool/Basic.lean
@@ -21,6 +21,123 @@ bool, boolean, Bool, De Morgan
 
 namespace Bool
 
+#align bor or
+#align band and
+#align bnot not
+#align bxor xor
+
+section
+
+/-!
+This section contains lemmas about booleans which were present in core Lean 3.
+The remainder of this file contains lemmas about booleans from mathlib 3.
+-/
+
+theorem true_eq_false_eq_False : ¬true = false := by decide
+#align tt_eq_ff_eq_false Bool.true_eq_false_eq_False
+
+theorem false_eq_true_eq_False : ¬false = true := by decide
+#align ff_eq_tt_eq_false Bool.false_eq_true_eq_False
+
+theorem eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false) := by simp
+#align eq_ff_eq_not_eq_tt Bool.eq_false_eq_not_eq_true
+
+theorem eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true) := by simp
+#align eq_tt_eq_not_eq_ft Bool.eq_true_eq_not_eq_false
+
+theorem eq_false_of_not_eq_true {b : Bool} : ¬b = true → b = false :=
+  Eq.mp (eq_false_eq_not_eq_true b)
+#align eq_ff_of_not_eq_tt Bool.eq_false_of_not_eq_true
+
+theorem eq_true_of_not_eq_false {b : Bool} : ¬b = false → b = true :=
+  Eq.mp (eq_true_eq_not_eq_false b)
+#align eq_tt_of_not_eq_ff Bool.eq_true_of_not_eq_false
+
+theorem and_eq_true_eq_eq_true_and_eq_true (a b : Bool) :
+    ((a && b) = true) = (a = true ∧ b = true) := by simp
+#align band_eq_true_eq_eq_tt_and_eq_tt Bool.and_eq_true_eq_eq_true_and_eq_true
+
+theorem or_eq_true_eq_eq_true_or_eq_true (a b : Bool) :
+    ((a || b) = true) = (a = true ∨ b = true) := by simp
+#align bor_eq_true_eq_eq_tt_or_eq_tt Bool.or_eq_true_eq_eq_true_or_eq_true
+
+theorem not_eq_true_eq_eq_false (a : Bool) : (not a = true) = (a = false) := by cases a <;> simp
+#align bnot_eq_true_eq_eq_ff Bool.not_eq_true_eq_eq_false
+
+#adaptation_note /-- this is no longer a simp lemma,
+  as after nightly-2024-03-05 the LHS simplifies. -/
+theorem and_eq_false_eq_eq_false_or_eq_false (a b : Bool) :
+    ((a && b) = false) = (a = false ∨ b = false) := by
+  cases a <;> cases b <;> simp
+#align band_eq_false_eq_eq_ff_or_eq_ff Bool.and_eq_false_eq_eq_false_or_eq_false
+
+theorem or_eq_false_eq_eq_false_and_eq_false (a b : Bool) :
+    ((a || b) = false) = (a = false ∧ b = false) := by
+  cases a <;> cases b <;> simp
+#align bor_eq_false_eq_eq_ff_and_eq_ff Bool.or_eq_false_eq_eq_false_and_eq_false
+
+theorem not_eq_false_eq_eq_true (a : Bool) : (not a = false) = (a = true) := by cases a <;> simp
+#align bnot_eq_ff_eq_eq_tt Bool.not_eq_false_eq_eq_true
+
+theorem coe_false : ↑false = False := by simp
+#align coe_ff Bool.coe_false
+
+theorem coe_true : ↑true = True := by simp
+#align coe_tt Bool.coe_true
+
+theorem coe_sort_false : (false : Prop) = False := by simp
+#align coe_sort_ff Bool.coe_sort_false
+
+theorem coe_sort_true : (true : Prop) = True := by simp
+#align coe_sort_tt Bool.coe_sort_true
+
+theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp
+#align to_bool_iff Bool.decide_iff
+
+theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
+  (decide_iff p).2
+#align to_bool_true Bool.decide_true
+#align to_bool_tt Bool.decide_true
+
+theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
+  (decide_iff p).1
+#align of_to_bool_true Bool.of_decide_true
+
+theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> decide
+#align bool_iff_false Bool.bool_iff_false
+
+theorem bool_eq_false {b : Bool} : ¬b → b = false :=
+  bool_iff_false.1
+#align bool_eq_false Bool.bool_eq_false
+
+theorem decide_false_iff (p : Prop) {_ : Decidable p} : decide p = false ↔ ¬p :=
+  bool_iff_false.symm.trans (not_congr (decide_iff _))
+#align to_bool_ff_iff Bool.decide_false_iff
+
+theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
+  (decide_false_iff p).2
+#align to_bool_ff Bool.decide_false
+
+theorem of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p :=
+  (decide_false_iff p).1
+#align of_to_bool_ff Bool.of_decide_false
+
+theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
+  decide_eq_decide.mpr h
+#align to_bool_congr Bool.decide_congr
+
+@[deprecated (since := "2024-06-07")] alias coe_or_iff := or_eq_true_iff
+#align bor_coe_iff Bool.or_eq_true_iff
+
+@[deprecated (since := "2024-06-07")] alias coe_and_iff := and_eq_true_iff
+#align band_coe_iff Bool.and_eq_true_iff
+
+theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
+  cases a <;> cases b <;> decide
+#align bxor_coe_iff Bool.coe_xor_iff
+
+end
+
 @[deprecated (since := "2024-06-07")] alias decide_True := decide_true_eq_true
 #align bool.to_bool_true decide_true_eq_true
 
diff --git a/Mathlib/Init/Data/Bool/Basic.lean b/Mathlib/Init/Data/Bool/Basic.lean
deleted file mode 100644
index f71faf73ddb703..00000000000000
--- a/Mathlib/Init/Data/Bool/Basic.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Mathlib.Mathport.Rename
-
-/-!
-# Note about `Mathlib/Init/`
-The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
-(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
-
-We intend to move all the content of these files out into the main `Mathlib` directory structure.
-Contributions assisting with this are appreciated.
-
-`#align` statements without corresponding declarations
-(i.e. because the declaration is in Batteries or Lean) can be left here.
-These will be deleted soon so will not significantly delay deleting otherwise empty `Init` files.
-
-# Boolean operations
-
-In Lean 3 this file contained the definitions of `cond`, `bor`, `band` and `bnot`,
-the boolean functions.
-These are now in Lean 4 core or Batteries (as `cond`, `or`, `and`, `not`, `xor`).
--/
-
-#align bor or
-#align band and
-#align bnot not
-#align bxor xor
diff --git a/Mathlib/Init/Data/Bool/Lemmas.lean b/Mathlib/Init/Data/Bool/Lemmas.lean
deleted file mode 100644
index ef7d193ed84d6b..00000000000000
--- a/Mathlib/Init/Data/Bool/Lemmas.lean
+++ /dev/null
@@ -1,163 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Mathlib.Init.Logic
-import Mathlib.Tactic.AdaptationNote
-import Mathlib.Tactic.Coe
-
-/-!
-# Note about `Mathlib/Init/`
-The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
-(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
-
-We intend to move all the content of these files out into the main `Mathlib` directory structure.
-Contributions assisting with this are appreciated.
-
-`#align` statements without corresponding declarations
-(i.e. because the declaration is in Batteries or Lean) can be left here.
-These will be deleted soon so will not significantly delay deleting otherwise empty `Init` files.
-
-# Lemmas about booleans
-
-These are the lemmas about booleans which were present in core Lean 3. See also
-the file Mathlib.Data.Bool.Basic which contains lemmas about booleans from
-mathlib 3.
-
--/
-
--- We align Lean 3 lemmas with lemmas in `Init.SimpLemmas` in Lean 4.
-#align band_self Bool.and_self
-#align band_tt Bool.and_true
-#align band_ff Bool.and_false
-#align tt_band Bool.true_and
-#align ff_band Bool.false_and
-#align bor_self Bool.or_self
-#align bor_tt Bool.or_true
-#align bor_ff Bool.or_false
-#align tt_bor Bool.true_or
-#align ff_bor Bool.false_or
-#align bnot_bnot Bool.not_not
-
-namespace Bool
-
-#align bool.cond_tt Bool.cond_true
-#align bool.cond_ff Bool.cond_false
-#align cond_a_a Bool.cond_self
-
-attribute [simp] xor_self
-#align bxor_self Bool.xor_self
-
-#align bxor_tt Bool.xor_true
-#align bxor_ff Bool.xor_false
-#align tt_bxor Bool.true_xor
-#align ff_bxor Bool.false_xor
-
-theorem true_eq_false_eq_False : ¬true = false := by decide
-#align tt_eq_ff_eq_false Bool.true_eq_false_eq_False
-
-theorem false_eq_true_eq_False : ¬false = true := by decide
-#align ff_eq_tt_eq_false Bool.false_eq_true_eq_False
-
-theorem eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false) := by simp
-#align eq_ff_eq_not_eq_tt Bool.eq_false_eq_not_eq_true
-
-theorem eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true) := by simp
-#align eq_tt_eq_not_eq_ft Bool.eq_true_eq_not_eq_false
-
-theorem eq_false_of_not_eq_true {b : Bool} : ¬b = true → b = false :=
-  Eq.mp (eq_false_eq_not_eq_true b)
-#align eq_ff_of_not_eq_tt Bool.eq_false_of_not_eq_true
-
-theorem eq_true_of_not_eq_false {b : Bool} : ¬b = false → b = true :=
-  Eq.mp (eq_true_eq_not_eq_false b)
-#align eq_tt_of_not_eq_ff Bool.eq_true_of_not_eq_false
-
-theorem and_eq_true_eq_eq_true_and_eq_true (a b : Bool) :
-    ((a && b) = true) = (a = true ∧ b = true) := by simp
-#align band_eq_true_eq_eq_tt_and_eq_tt Bool.and_eq_true_eq_eq_true_and_eq_true
-
-theorem or_eq_true_eq_eq_true_or_eq_true (a b : Bool) :
-    ((a || b) = true) = (a = true ∨ b = true) := by simp
-#align bor_eq_true_eq_eq_tt_or_eq_tt Bool.or_eq_true_eq_eq_true_or_eq_true
-
-theorem not_eq_true_eq_eq_false (a : Bool) : (not a = true) = (a = false) := by cases a <;> simp
-#align bnot_eq_true_eq_eq_ff Bool.not_eq_true_eq_eq_false
-
-#adaptation_note /-- this is no longer a simp lemma,
-  as after nightly-2024-03-05 the LHS simplifies. -/
-theorem and_eq_false_eq_eq_false_or_eq_false (a b : Bool) :
-    ((a && b) = false) = (a = false ∨ b = false) := by
-  cases a <;> cases b <;> simp
-#align band_eq_false_eq_eq_ff_or_eq_ff Bool.and_eq_false_eq_eq_false_or_eq_false
-
-theorem or_eq_false_eq_eq_false_and_eq_false (a b : Bool) :
-    ((a || b) = false) = (a = false ∧ b = false) := by
-  cases a <;> cases b <;> simp
-#align bor_eq_false_eq_eq_ff_and_eq_ff Bool.or_eq_false_eq_eq_false_and_eq_false
-
-theorem not_eq_false_eq_eq_true (a : Bool) : (not a = false) = (a = true) := by cases a <;> simp
-#align bnot_eq_ff_eq_eq_tt Bool.not_eq_false_eq_eq_true
-
-theorem coe_false : ↑false = False := by simp
-#align coe_ff Bool.coe_false
-
-theorem coe_true : ↑true = True := by simp
-#align coe_tt Bool.coe_true
-
-theorem coe_sort_false : (false : Prop) = False := by simp
-#align coe_sort_ff Bool.coe_sort_false
-
-theorem coe_sort_true : (true : Prop) = True := by simp
-#align coe_sort_tt Bool.coe_sort_true
-
-theorem decide_iff (p : Prop) [d : Decidable p] : decide p = true ↔ p := by simp
-#align to_bool_iff Bool.decide_iff
-
-theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
-  (decide_iff p).2
-#align to_bool_true Bool.decide_true
-#align to_bool_tt Bool.decide_true
-
-theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
-  (decide_iff p).1
-#align of_to_bool_true Bool.of_decide_true
-
-theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> decide
-#align bool_iff_false Bool.bool_iff_false
-
-theorem bool_eq_false {b : Bool} : ¬b → b = false :=
-  bool_iff_false.1
-#align bool_eq_false Bool.bool_eq_false
-
-theorem decide_false_iff (p : Prop) {_ : Decidable p} : decide p = false ↔ ¬p :=
-  bool_iff_false.symm.trans (not_congr (decide_iff _))
-#align to_bool_ff_iff Bool.decide_false_iff
-
-theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
-  (decide_false_iff p).2
-#align to_bool_ff Bool.decide_false
-
-theorem of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p :=
-  (decide_false_iff p).1
-#align of_to_bool_ff Bool.of_decide_false
-
-theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
-  decide_eq_decide.mpr h
-#align to_bool_congr Bool.decide_congr
-
-@[deprecated (since := "2024-06-07")] alias coe_or_iff := or_eq_true_iff
-#align bor_coe_iff Bool.or_eq_true_iff
-
-@[deprecated (since := "2024-06-07")] alias coe_and_iff := and_eq_true_iff
-#align band_coe_iff Bool.and_eq_true_iff
-
-theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
-  cases a <;> cases b <;> decide
-#align bxor_coe_iff Bool.coe_xor_iff
-
-#align ite_eq_tt_distrib Bool.ite_eq_true_distrib
-#align ite_eq_ff_distrib Bool.ite_eq_false_distrib
-
-end Bool
diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
index fb402af66fd959..e5622299ae341e 100644
--- a/Mathlib/Logic/Equiv/Defs.lean
+++ b/Mathlib/Logic/Equiv/Defs.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Data.FunLike.Equiv
 import Mathlib.Data.Quot
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 import Mathlib.Logic.Unique
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.Conv
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean
index b2156047afabbb..2e726893be89d9 100644
--- a/Mathlib/Topology/Category/Profinite/Nobeling.lean
+++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.ModuleCat.Free
 import Mathlib.Topology.Category.Profinite.CofilteredLimit
 import Mathlib.Topology.Category.Profinite.Product
 import Mathlib.Topology.LocallyConstant.Algebra
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Data.Bool.Basic
 
 /-!
 
diff --git a/scripts/noshake.json b/scripts/noshake.json
index 334b65cd2e297a..1f28154df33077 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -289,7 +289,7 @@
   "Mathlib.NumberTheory.ArithmeticFunction": ["Mathlib.Tactic.ArithMult"],
   "Mathlib.MeasureTheory.MeasurableSpace.Defs": ["Mathlib.Tactic.FunProp.Attr"],
   "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"],
-  "Mathlib.Logic.Equiv.Defs": ["Mathlib.Init.Data.Bool.Lemmas"],
+  "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic"],
   "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"],
   "Mathlib.LinearAlgebra.Basic": ["Mathlib.Algebra.BigOperators.Group.Finset"],
   "Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional": ["Mathlib.Init.Core"],
@@ -303,7 +303,7 @@
   "Mathlib.Init.Data.Nat.GCD": ["Batteries.Data.Nat.Gcd"],
   "Mathlib.Init.Data.List.Basic": ["Batteries.Data.List.Basic"],
   "Mathlib.Init.Data.Int.Basic": ["Batteries.Data.Int.Order"],
-  "Mathlib.Init.Data.Bool.Lemmas": ["Mathlib.Tactic.AdaptationNote"],
+  "Mathlib.Data.Bool.Basic": ["Mathlib.Tactic.AdaptationNote"],
   "Mathlib.GroupTheory.MonoidLocalization": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Geometry.Manifold.Sheaf.Smooth":
   ["Mathlib.CategoryTheory.Sites.Whiskering"],

From 12a8aefe5faf6d665b4486ee37ab6f1ecae5e26a Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 15 Jul 2024 22:13:04 +0200
Subject: [PATCH 2/4] Update scripts/noshake.json

---
 scripts/noshake.json | 1 -
 1 file changed, 1 deletion(-)

diff --git a/scripts/noshake.json b/scripts/noshake.json
index 1f28154df33077..bbe39cf2c3067f 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -303,7 +303,6 @@
   "Mathlib.Init.Data.Nat.GCD": ["Batteries.Data.Nat.Gcd"],
   "Mathlib.Init.Data.List.Basic": ["Batteries.Data.List.Basic"],
   "Mathlib.Init.Data.Int.Basic": ["Batteries.Data.Int.Order"],
-  "Mathlib.Data.Bool.Basic": ["Mathlib.Tactic.AdaptationNote"],
   "Mathlib.GroupTheory.MonoidLocalization": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Geometry.Manifold.Sheaf.Smooth":
   ["Mathlib.CategoryTheory.Sites.Whiskering"],

From b46722c01714bc2eb6d97ccfe184ff183076c78f Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 16 Jul 2024 10:04:48 +0200
Subject: [PATCH 3/4] import

---
 Mathlib/Order/Monotone/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index 1e5d6bf82813a9..a78f99d4e6464c 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.Init.Data.Int.Order
 import Mathlib.Order.Compare
 import Mathlib.Order.Max
 import Mathlib.Order.RelClasses
+import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Choose
 
 #align_import order.monotone.basic from "leanprover-community/mathlib"@"554bb38de8ded0dafe93b7f18f0bfee6ef77dc5d"

From 3cbafd794979bba490988f5240ac0c04e7036c79 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 16 Jul 2024 10:18:17 +0200
Subject: [PATCH 4/4] import

---
 Mathlib/Logic/Equiv/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index 64581fe86e3c44..316f3538d4a757 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -12,6 +12,7 @@ import Mathlib.Data.Sum.Basic
 import Mathlib.Init.Data.Sigma.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Function.Conjugate
+import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Contrapose