mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Internal.Impl.ofList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : List ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.ofList l = ↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the left.  -/
iteratedFDeriv_comp_add_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a x : E), iteratedFDeriv 𝕜 n (fun z => f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNF_spec : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2] [inst_2 : Invertible 3],
  (W.toShortNF • W).IsShortNF
-- Aesop.Stats.Basic
Aesop.RuleStats : Type
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_iSup_le_sum : ∀ {ι : Type u} [Small.{v, u} ι] (f : ι → Cardinal.{v}), Cardinal.lift.{u, v} (⨆ i, f i) ≤ Cardinal.sum f
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ofUnitHom_eq : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : Rˣ →* R'ˣ),
  MulChar.ofUnitHom χ = MulChar.equivToUnitHom.symm χ
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_map_eq : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β),
  (∀ (a : α), ‖f a‖ = ‖a‖) → ‖A.map f‖ = ‖A‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp] {a : α}, Std.DTreeMap.Const.get? t a = t.get? a
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- The subgroup of the units of `Unitization R A` whose scalar part is `1`.  -/
Unitization.unitsFstOne : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] → [inst_4 : SMulCommClass R A A] → Subgroup (Unitization R A)ˣ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.snoc_castSucc : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubMulAction.ofStabilizer G a)) (i : Fin n), (SubMulAction.ofStabilizer.snoc x) i.castSucc = ↑(x i)
-- Mathlib.Algebra.Group.Commute.Units
Units.rightOfMul.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (a b : M) (hu : a * b = ↑u) (hc : Commute a b),
  u.rightOfMul a b hu hc = u.leftOfMul b a ⋯ ⋯
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.orientation_map : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {ι : Type u_4} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (e : Module.Basis ι R M) (f : M ≃ₗ[R] N),
  (e.map f).orientation = (Orientation.map ι f) e.orientation
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.indent : Lean.Widget.LazyTraceChildren → ℕ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.topEquiv_toAddMonoidHom : ∀ {M : Type u_5} [inst : AddZeroClass M], ↑AddSubmonoid.topEquiv = ⊤.subtype
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.nhds_basis_closedBall : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E},
  (nhds x).HasBasis (fun r => 0 < r) (Euclidean.closedBall x)
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toFin = OfNat.ofNat n
-- Init.Data.Float.Float32
/-- Computes the arc cosine (inverse cosine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`acosf`.
 -/
Float32.acos : Float32 → Float32
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnAlgHom_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] (R : Type u_2) [inst_1 : CommSemiring R] {A : Type u_3}
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A]
  (f : C(α, A)) (a : α), (ContinuousMap.coeFnAlgHom R) f a = f a
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquiv_symm : ∀ {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)),
  (e.subtypeEquiv h).symm = e.symm.subtypeEquiv ⋯
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.prod_inner : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  [inst_10 : StarOrderedRing A] (x y : WithCStarModule A (E × F)), inner A x y = inner A x.1 y.1 + inner A x.2 y.2
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoLT_ofRelIsoLT : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  (e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2), (OrderIso.ofRelIsoLT e).toRelIsoLT = e
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.X_u₁_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.X✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁✝ S) =
    FermatLastTheoremForThreeGen.Solution.x✝ S
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.integralClosure_eq_bot : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsIntegrallyClosedIn R A] [IsDomain R] [Module.IsTorsionFree R A] [Nontrivial A], integralClosure R A = ⊥
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given open range as a list in ascending order.
 -/
Std.Roo.toList : {α : Type u} →
  [inst : LT α] →
    [DecidableLT α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Roo α → List α
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.ofIsUnitDet_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  {f : M →ₗ[R] M'} {v : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det)
  (a : M), (LinearEquiv.ofIsUnitDet h) a = f a
-- Mathlib.Logic.Embedding.Set
subtypeOrEquiv_apply : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] (h : Disjoint p q) (a : { x // p x ∨ q x }),
  (subtypeOrEquiv p q h) a = (subtypeOrLeftEmbedding p q) a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_revSkipWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos.revSkipWhile p ≠ s.startPos},
  p (((pos.revSkipWhile p).prev h).get ⋯) = false
-- Std.Data.ByteSlice
/-- The stopping index is no later than the end of the byte array.

The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of
the byte array is in the byte slice.
 -/
ByteSlice.stop_le_size_byteArray : ∀ (xs : ByteSlice), xs.stop ≤ xs.byteArray.size
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_fst_le_agm : ∀ {x y : NNReal} (n : ℕ), (x.agmSequences y n).1 ≤ x.agm y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.parts.inj : ∀ {p p_1 : Array Lean.Lsp.InlayHintLabelPart},
  Lean.Lsp.InlayHintLabel.parts p = Lean.Lsp.InlayHintLabel.parts p_1 → p = p_1
-- Mathlib.Logic.Equiv.Finset
Denumerable.lower'.eq_1 : ∀ (x : ℕ), Denumerable.lower' [] x = []
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastArithShiftRightConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.of_equiv : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  {S' : Type u_7} [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [h : Algebra.IsPushout R R' S S'] {T : Type u_8} [inst_11 : CommSemiring T] [inst_12 : Algebra R' T]
  [inst_13 : Algebra S T] [inst_14 : Algebra R T] [inst_15 : IsScalarTower R S T] [inst_16 : IsScalarTower R R' T]
  (e : S' ≃ₐ[R'] T), e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T → Algebra.IsPushout R R' S T
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.toMessageData : Lean.Meta.Match.Example → Lean.MessageData
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The Riemann Zeta Function does not vanish on the closed half-plane `re s ≥ 1`.
(Note that the value at `s = 1` is a junk value, which happens to be nonzero.)  -/
riemannZeta_ne_zero_of_one_le_re : ∀ ⦃s : ℂ⦄, 1 ≤ s.re → riemannZeta s ≠ 0
-- Mathlib.Order.Hom.Basic
OrderIso.symm_apply_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β}, e.symm y = x ↔ y = e x
-- Init.Data.String.Iterate
String.Internal.foldlImpl : (String → Char → String) → String → String → String
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.decl.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.CasesTarget.decl decl = Aesop.CasesTarget.decl decl_1) = (decl = decl_1)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkEvalMonoidalM : Mathlib.Tactic.BicategoryLike.MkEval Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toExtensionHom_toRingHom : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P'), f.toExtensionHom.toRingHom = f.toAlgHom.toRingHom
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- A cycle is a non-identity permutation where any two nonfixed points of the permutation are
related by repeated application of the permutation.  -/
Equiv.Perm.IsCycle : {α : Type u_2} → Equiv.Perm α → Prop
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonAssocRingOfIsTopologicalRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : NonAssocRing β] → [IsTopologicalRing β] → NonAssocRing C(α, β)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_iff_forall_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ ∀ (a : α), t.contains a = false
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'_apply_apply : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ),
  ((finsuppTensorFinsupp' R ι κ) (f ⊗ₜ[R] g)) (a, b) = f a * g b
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `none` if the set is empty.
 -/
Std.TreeSet.Raw.min? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Option α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.homAddMonoidHom.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal],
  F.homAddMonoidHom = { toFun := F.map, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD
            k' fallback =
          k
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v' : V'}
  {C : G.ConnectedComponent},
  G.connectedComponentMk (φ.symm v') = C ↔
    G'.connectedComponentMk v' = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.toPerfPair_comp_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ⇑P.toPerfPair ∘ ⇑P.root = P.root'
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_functor_obj : ∀ {J : Type u_1} {K : Type u_2} (a : CategoryTheory.Discrete (J × K)),
  CategoryTheory.Discrete.productEquiv.functor.obj a = ({ as := a.as.1 }, { as := a.as.2 })
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isGLB_u_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {s : Set α} {a : α}, IsGLB s a → IsGLB (u '' s) (u a)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.pickMaxFVar? : Lean.LocalContext → Array Lean.FVarId → Option Lean.FVarId
-- Batteries.Recycling.RBTree.WF
/-- The `DelProp` property is a strengthened version of the red-red invariant.  -/
RBTree.RBNode.DelProp.redred : ∀ {c : RBTree.RBColor} {α : Type u_1} {t : RBTree.RBNode α} {n : ℕ},
  RBTree.RBNode.DelProp c t n → ∃ n', RBTree.RBNode.RedRed (c = RBTree.RBColor.black) t n'
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.preservesFiniteProductsOfAdditive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.Additive], CategoryTheory.Limits.PreservesFiniteProducts F
-- Init.Data.SInt.Lemmas
Int16.div_self : ∀ {a : Int16}, a / a = if a = 0 then 0 else 1
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (A : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X : C),
  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).X = A.X.obj X
-- Mathlib.Order.Lattice.Nat
Set.biUnion_lt_succ' : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋃ k, ⋃ (_ : k < n + 1), u k = u 0 ∪ ⋃ k, ⋃ (_ : k < n), u (k + 1)
-- Mathlib.Data.Int.Star
Int.instStarOrderedRing : StarOrderedRing ℤ
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balRight.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (l : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) →
          (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b)) →
        ((a : RBTree.RBNode α) →
            (x : α) →
              (b : RBTree.RBNode α) →
                (y : α) →
                  (c : RBTree.RBNode α) →
                    motive
                      (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c))) →
          ((l : RBTree.RBNode α) →
              (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                  l = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
                (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                    l = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) →
                      False) →
                  motive l) →
            motive l
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} → String.Slice.SplitIterator pat s → Option (Std.Iter (String.Slice.Pattern.SearchStep s))
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.instIsGaussianMapNeg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ],
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun x => -x) μ)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHomClass.toOneHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : MulOne M} {inst_1 : MulOne N}
  {inst_2 : FunLike F M N} [self : MonoidHomClass F M N], OneHomClass F M N
-- Lean.Meta.WHNF
/-- Similar to `getConstInfo?` but using `getUnfoldableConstNoEx?`.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.getConstInfoNoEx? : Lean.Name → Bool → Lean.MetaM (Option Lean.ConstantInfo)
-- Mathlib.RingTheory.MvPowerSeries.Rename
/-- Rename all the variables in a multivariable power series by a map with finite fibers.  -/
MvPowerSeries.rename : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_4} →
      (f : σ → τ) → [Filter.TendstoCofinite f] → [inst : CommSemiring R] → MvPowerSeries σ R →ₐ[R] MvPowerSeries τ R
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Ioo_eq_Ioi : ∀ {n : ℕ} (a : Fin n), (Finset.Ioo (↑a) n).attachFin ⋯ = Finset.Ioi a
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.options : Lean.PrettyPrinter.Formatter.Context → Lean.Options
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- `basicOpen r` is the open subset containing all prime ideals not containing `r`.  -/
ProjectiveSpectrum.basicOpen : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → A → TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.functorMapReverse : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (F : CategoryTheory.Functor C D), F.toPrefunctor.MapReverse
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_assoc' : ∀ {a b : ℝ} (x y z : ↑(Set.Icc a b)) (s t : ↑unitInterval),
  Set.Icc.convexComb (Set.Icc.convexComb x y s) z t =
    Set.Icc.convexComb x (Set.Icc.convexComb y z (Set.Icc.convexComb_assoc_coeff₂' s t))
      (Set.Icc.convexComb_assoc_coeff₁' s t)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars.isScalarTower : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (p : Submodule R M),
  IsScalarTower S R ↥(Submodule.restrictScalars S p)
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite : ∀ {G : Type u} [inst : AddMonoid G],
  (∀ (g : G), 0 < addOrderOf g) → (AddMonoid.exponent G = 0 ↔ (Set.range addOrderOf).Infinite)
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_sumIDeriv : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ),
  ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        (Polynomial.X - Polynomial.C r) ^ q ∣ Polynomial.map (algebraMap R A) p →
          (Polynomial.aeval r) (Polynomial.sumIDeriv p) = q.factorial • (Polynomial.aeval r) gp
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfMultiset.congr_simp : ∀ {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} (a_1 : m.Nodup) (a_2 : ∀ i ∈ m, s i ≠ 0)
  (a_3 : {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s)),
  Nat.chineseRemainderOfMultiset a s a_1 a_2 a_3 = Nat.chineseRemainderOfMultiset a s a_1 a_2 a_3
-- Mathlib.CategoryTheory.Category.PartialFun
PartialFun.Iso.mk_inv : ∀ {α β : PartialFun} (e : α ≃ β) (x : β), (PartialFun.Iso.mk e).inv x = ↑(some (e.symm x))
-- Mathlib.Algebra.Star.Unitary
Unitary.instIsScalarTowerSubtypeMemSubmonoidUnitary : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid A]
  [inst_3 : StarMul R] [inst_4 : StarMul S] [inst_5 : StarMul A] [inst_6 : MulAction R S] [inst_7 : MulAction R A]
  [inst_8 : MulAction S A] [inst_9 : StarModule R S] [inst_10 : StarModule R A] [inst_11 : StarModule S A]
  [inst_12 : IsScalarTower R A A] [inst_13 : IsScalarTower S A A] [inst_14 : SMulCommClass R A A]
  [inst_15 : SMulCommClass S A A] [inst_16 : IsScalarTower R S S] [inst_17 : SMulCommClass R S S] [IsScalarTower R S A],
  IsScalarTower ↥(unitary R) ↥(unitary S) ↥(unitary A)
-- Batteries.Tactic.PermuteGoals
/-- `on_goal n => tacSeq` creates a block scope for the `n`-th goal and tries the sequence
of tactics `tacSeq` on it.

`on_goal -n => tacSeq` does the same, but the `n`-th goal is chosen by counting from the
bottom.

The goal is not required to be solved and any resulting subgoals are inserted back into the
list of goals, replacing the chosen goal.
 -/
Batteries.Tactic.«tacticOn_goal-_=>_» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasFiniteColimits : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteColimits C], CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.ShortComplex C)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_inter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜}, t ∈ nhds x → derivWithin f (s ∩ t) x = derivWithin f s x
-- Mathlib.SetTheory.Cardinal.Continuum
/-- Cardinality of the continuum.  -/
Cardinal.term𝔠 : Lean.ParserDescr
-- Lean.Environment
Lean.EffectiveImport.mk.injEq : ∀ (toImport : Lean.Import) (irPhases : Lean.IRPhases) (hasData : Bool) (toImport_1 : Lean.Import)
  (irPhases_1 : Lean.IRPhases) (hasData_1 : Bool),
  ({ toImport := toImport, irPhases := irPhases, hasData := hasData } =
      { toImport := toImport_1, irPhases := irPhases_1, hasData := hasData_1 }) =
    (toImport = toImport_1 ∧ irPhases = irPhases_1 ∧ hasData = hasData_1)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instCompactSpaceSubtypeMem : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.Compacts α), CompactSpace ↥K