feat: port Logic.Equiv.TransferInstance (#3206)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Apr 19, 2023 · 34a32cd · 34a32cd
1 parent df4f506
commit 34a32cd
Show file tree

Hide file tree

Showing 2 changed files with 591 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1370,6 +1370,7 @@ import Mathlib.Logic.Equiv.MfldSimpsAttr
 import Mathlib.Logic.Equiv.Nat
 import Mathlib.Logic.Equiv.Option
 import Mathlib.Logic.Equiv.Set
+import Mathlib.Logic.Equiv.TransferInstance
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Function.Conjugate
 import Mathlib.Logic.Function.Iterate