delete LiftLets

leanprover-community · Dec 21, 2024 · ba4c611 · ba4c611
1 parent 17c25ae
commit ba4c611
Show file tree

Hide file tree

Showing 6 changed files with 0 additions and 246 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -4816,7 +4816,6 @@ import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Lift
-import Mathlib.Tactic.LiftLets
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Linarith.Frontend

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
@@ -6,7 +6,6 @@ Authors: Eric Wieser
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
 import Mathlib.LinearAlgebra.CliffordAlgebra.Even
 import Mathlib.LinearAlgebra.QuadraticForm.Prod
-import Mathlib.Tactic.LiftLets
 
 /-!
 # Isomorphisms with the even subalgebra of a Clifford algebra

diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -117,7 +117,6 @@ import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.Lift
-import Mathlib.Tactic.LiftLets
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Linarith.Frontend

diff --git a/Mathlib/Tactic/LiftLets.lean b/Mathlib/Tactic/LiftLets.lean
diff --git a/MathlibTest/LiftLets.lean b/MathlibTest/LiftLets.lean
diff --git a/scripts/noshake.json b/scripts/noshake.json
@@ -115,7 +115,6 @@
   "Mathlib.Tactic.Lemma",
   "Mathlib.Tactic.LibrarySearch",
   "Mathlib.Tactic.Lift",
-  "Mathlib.Tactic.LiftLets",
   "Mathlib.Tactic.Linarith",
   "Mathlib.Tactic.Linarith.Frontend",
   "Mathlib.Tactic.Linarith.Lemmas",