mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal_toSubmodule : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ : LinearMap.BilinForm R M)
  (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M),
  ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = Φ.orthogonal ↑N
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Ordnode.nil = 1
-- Mathlib.Topology.EMetricSpace.Defs
/-- Relation “two points are at a finite edistance” is an equivalence relation.  -/
Metric.edistLtTopSetoid : {α : Type u} → [PseudoEMetricSpace α] → Setoid α
-- Mathlib.CategoryTheory.Extensive
/-- A category is (finitary) extensive if it has finite coproducts,
and binary coproducts are van Kampen.  -/
CategoryTheory.FinitaryExtensive : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.GroupTheory.FreeGroup.Basic
Quot.map.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} (f f_1 : α → β) (e_f : f = f_1)
  (h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)) (a a_1 : Quot ra), a = a_1 → Quot.map f h a = Quot.map f_1 ⋯ a_1
-- Init.Data.List.Nat.Modify
List.drop_modify_of_lt : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), i < j → List.drop j (l.modify i f) = List.drop j l
-- Mathlib.AlgebraicGeometry.Scheme
/-- Given a morphism of schemes `f : X ⟶ Y`, and open `U ⊆ Y`,
this is the induced map `Γ(Y, U) ⟶ Γ(X, f ⁻¹ᵁ U)`.

This is treated as a suffix in lemma names.  -/
AlgebraicGeometry.Scheme.Hom.app : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))
-- Mathlib.RingTheory.Regular.IsSMulRegular
mem_of_isSMulRegular_quotient_of_smul_mem : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {r : R}, IsSMulRegular (M ⧸ N) r → ∀ {x : M}, r • x ∈ N → x ∈ N
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_ofFn : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  xs.mapFinIdx f = Array.ofFn fun i => f (↑i) xs[i] ⋯
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_add : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f g : ContIntertwiningMap π₁ π₂),
  (f + g).toContinuousLinearMap = f.toContinuousLinearMap + g.toContinuousLinearMap
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
/-- The set of points for which a sequence of measurable functions converges to a given value
is measurable.  -/
measurableSet_tendsto : ∀ {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x : MeasurableSpace β} [inst : MeasurableSpace γ] [Countable δ]
  {l : Filter δ} [l.IsCountablyGenerated] (l' : Filter γ) [l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated]
  {f : δ → β → γ}, (∀ (i : δ), Measurable (f i)) → MeasurableSet {x | Filter.Tendsto (fun n => f n x) l l'}
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X)
  (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) s.base = b
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerived_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  [inst_7 : H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.leftDerived n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived β n) h)
-- Mathlib.RingTheory.Localization.BaseChange
LocalizedModule.equivTensorProduct_symm_apply_tmul_one : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (x : M), (LocalizedModule.equivTensorProduct S M).symm (1 ⊗ₜ[R] x) = LocalizedModule.mk x 1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_zero : ∀ (x : ℕ), x.testBit 0 = decide (x % 2 = 1)
-- Mathlib.Tactic.Order.CollectFacts
/-- Updates the state with the atom `x`. If `x` is `⊤` or `⊥`, adds the corresponding fact. If `x`
is `y ⊔ z`, adds a fact about it, then recursively calls `addAtom` on `y` and `z`.
Similarly for `⊓`. Assumes that `type` is already added by `addType`.  -/
Mathlib.Tactic.Order.addAtom : {u : Lean.Level} → (type : Q(Type u)) → Q(«$type») → Mathlib.Tactic.Order.CollectFactsM ℕ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is nonzero, the first and third points are not
equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_sign_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₁ ≠ p₃
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Restriction of a ring homomorphism to a subsemiring of the domain.  -/
RingHom.domRestrict : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        {σR : Type u_1} → [inst_2 : SetLike σR R] → [inst_3 : SubsemiringClass σR R] → (R →+* S) → (s : σR) → ↥s →+* S
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.nonneg_subConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G},
  A.Nonempty → B.Nonempty → 1 ≤ A.subConst B
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instNonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Nonempty α], Nonempty (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.RingTheory.Trace.Basic
sum_embeddings_eq_finrank_mul : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : Type u_6)
  [inst_3 : Field F] [inst_4 : Algebra L F] [inst_5 : Algebra K F] [IsScalarTower K L F] (E : Type u_7)
  [inst_7 : Field E] [inst_8 : Algebra K E] [IsAlgClosed E] [inst_10 : FiniteDimensional K F] [Algebra.IsSeparable K F]
  (pb : PowerBasis K L), ∑ σ, σ ((algebraMap L F) pb.gen) = Module.finrank L F • ∑ σ, σ pb.gen
-- Init.Data.SInt.Lemmas
UInt8.ofBitVec_int8ToBitVec : ∀ (x : Int8), { toBitVec := x.toBitVec } = x.toUInt8
-- Mathlib.Algebra.DirectSum.Ring
/-- The `SMulWithZero` structure on the grade zero part
of a `GNonUnitalNonAssocSemiring`.  -/
DirectSum.instSMulWithZeroOfNat : {ι : Type u_1} →
  [inst : DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst_1 : AddZeroClass ι] →
        [inst_2 : (i : ι) → AddCommMonoid (A i)] →
          [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] → (i : ι) → SMulWithZero (A 0) (A i)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.parent_link : ∀ {self : Batteries.UnionFind} {x y : Fin self.size} (yroot : self.parent ↑y = ↑y) {i : ℕ},
  (self.link x y yroot).parent i =
    if ↑x = ↑y then self.parent i
    else
      if self.rank ↑y < self.rank ↑x then if ↑y = i then ↑x else self.parent i else if ↑x = i then ↑y else self.parent i
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.instToStringOrderType : ToString Mathlib.Tactic.Order.OrderType
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.monotone_triangEnvelopeIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → ∀ (n : ℕ), P.triangEnvelopeIter n ≤ Q.triangEnvelopeIter n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.ofIso_inr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q'),
  (b.ofIso eP eQ).inr = CategoryTheory.CategoryStruct.comp eQ.inv b.inr
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The constant multivariate formal power series.  -/
MvPowerSeries.C : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → R →+* MvPowerSeries σ R
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- The minimum of locally Lipschitz functions is locally Lipschitz.  -/
LocallyLipschitz.min : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => min (f x) (g x)
-- Init.Data.List.Lemmas
List.elem_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {as : List α}, List.elem a as = true ↔ a ∈ as
-- Mathlib.Lean.GoalsLocation
/-- The `SubExpr.Pos` specified by the `GoalsLocation`.  -/
Lean.SubExpr.GoalsLocation.pos : Lean.SubExpr.GoalsLocation → Lean.SubExpr.Pos
-- Mathlib.Topology.Instances.CantorSet
/-- Points of the Cantor set correspond to infinite paths in the full binary tree.
at each level `n`, the set `preCantorSet (n + 1)` splits each interval in
`preCantorSet n` into two parts.
Given `x ∈ cantorSet`, the point `x` lies in one of the intervals of `preCantorSet n`.
This function tracks which of the two intervals in `preCantorSet (n + 1)`
contains `x` at each step, producing the corresponding path as a stream of booleans.  -/
cantorToBinary : ℝ → Stream' Bool
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_StateT_eq : ∀ {m : Type u_1 → Type u_2} {α ρ : Type u_1} {p : α → Prop} {x : StateT ρ m α} [inst : Monad m] [LawfulMonad m],
  SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM (fun x => p x.1) (x.run s)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff : ∀ {R : Type u} [inst : CommSemiring R] {s t : Set (PrimeSpectrum R)},
  IsClosed s → IsClosed t → (s ⊂ t ↔ PrimeSpectrum.vanishingIdeal t < PrimeSpectrum.vanishingIdeal s)
-- Mathlib.Order.Interval.Finset.Defs
instSubsingletonLocallyFiniteOrderBot : ∀ {α : Type u_1} [inst : Preorder α], Subsingleton (LocallyFiniteOrderBot α)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.connected_toSimpleGraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.toSimpleGraph.Connected
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.orderTopToTypeSucc : (o : Ordinal.{u_4}) → OrderTop (Order.succ o).ToType
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.partialMatch_prefixFunction : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size),
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat
    (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst) (stackPos + 1)
-- Lean.Meta.Basic
/-- Similar to `isDefEq`, but returns `false` if an exception has been thrown.  -/
Lean.Meta.isDefEqGuarded : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsWeaklyRegular.isRegular_of_isLocalization_of_mem : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] [IsLocalization.AtPrime S p] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular R rs →
    (∀ r ∈ rs, r ∈ p) → RingTheory.Sequence.IsRegular S (List.map (⇑(algebraMap R S)) rs)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_two : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), normEDS b c d 2 = b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_get?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termY₃ : Lean.ParserDescr
-- Init.MetaTypes
Lean.Meta.instInhabitedTransparencyMode : Inhabited Lean.Meta.TransparencyMode
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_iff' : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (f : PowerSeries R),
  PowerSeries.IsRestricted c f ↔ Filter.Tendsto (fun t => ‖(PowerSeries.coeff t) f‖ * c ^ t) Filter.atTop (nhds 0)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- **Alias** of `Bundle.Trivialization.mdifferentiable`. -/
Bundle.Trivialization.Bundle.Trivialization.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_12} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_13} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {F : Type u_14}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {M : Type u_15} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] (Z : M → Type u_16) [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z] [inst_11 : (b : M) → AddCommMonoid (Z b)]
  [inst_12 : (b : M) → Module 𝕜 (Z b)] [inst_13 : VectorBundle 𝕜 F Z] [ContMDiffVectorBundle 1 F Z I]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
  OpenPartialHomeomorph.MDifferentiable (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F))
    e.toOpenPartialHomeomorph
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_scaleRoots : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (r : R),
  (f.scaleRoots r).resultant (g.scaleRoots r) = r ^ (f.natDegree * g.natDegree) * f.resultant g
-- Mathlib.Topology.Sequences
SequentialSpace.coinduced : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SequentialSpace X] {Y : Type u_3} (f : X → Y), SequentialSpace Y
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.splitAtPred.match_3.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A proper space is complete  -/
complete_of_proper : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], CompleteSpace α
-- Init.Data.String.Slice
/-- Advances `pos` as long as `pat` matches.
 -/
String.Slice.Pos.skipWhile : {ρ : Type} → {s : String.Slice} → s.Pos → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → s.Pos
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (carrier : Type v) [commRing : CommRing carrier] [algebra : Algebra R carrier]
  (carrier_1 : Type v) (commRing_1 : CommRing carrier_1) (algebra_1 : Algebra R carrier_1),
  ({ carrier := carrier, commRing := commRing, algebra := algebra } =
      { carrier := carrier_1, commRing := commRing_1, algebra := algebra_1 }) =
    (carrier = carrier_1 ∧ commRing ≍ commRing_1 ∧ algebra ≍ algebra_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mem_iSup : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {ι : Sort u_1} {p : ι → SubAddAction R M} {x : M},
  x ∈ ⨆ i, p i ↔ ∃ i, x ∈ p i
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeUnop_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F.unop ⟶ G.unop) (X : Cᵒᵖ),
  (CategoryTheory.NatTrans.removeUnop α).app X = (α.app (Opposite.unop X)).op
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLawfulEqOrdQuarter : Std.LawfulEqOrd Std.Time.Month.Quarter
-- Mathlib.Order.Directed
directed_id : ∀ {α : Type u_1} {r : α → α → Prop} [IsDirected α r], Directed r id
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R)
  [NoZeroDivisors R], m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
-- Mathlib.Computability.TuringMachine.Tape
/-- Apply a pointed map to a tape to change the alphabet.  -/
Turing.Tape.map : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → Turing.PointedMap Γ Γ' → Turing.Tape Γ → Turing.Tape Γ'
-- Mathlib.FieldTheory.Separable
Polynomial.rootMultiplicity_le_one_of_separable : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : Polynomial R},
  p.Separable → ∀ (x : R), Polynomial.rootMultiplicity x p ≤ 1
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_bot_eq_top : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subgroupOf ⊥ = ⊤
-- Lean.Parser.Term.Basic
Lean.Parser.Term.typeSpec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_uIcc : ∀ {a b : ℝ}, a ≠ b → UniqueDiffOn ℝ (Set.uIcc a b)
-- Mathlib.Logic.Basic
xor_comm : ∀ (a b : Prop), Xor a b = Xor b a
-- Lean.Elab.PreDefinition.Main
/-- Set any lingering level mvars to `.zero`, for error recovery.
 -/
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.setLevelMVarsAtPreDef : Lean.Elab.PreDefinition → Lean.Elab.PreDefinition
-- Mathlib.RingTheory.FractionalIdeal.Norm
/-- The absolute norm of the fractional ideal `I` extending by multiplicativity the absolute norm
on (integral) ideals.  -/
FractionalIdeal.absNorm : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      [Module.Free ℤ R] →
        [Module.Finite ℤ R] →
          {K : Type u_2} →
            [inst_4 : CommRing K] →
              [inst_5 : Algebra R K] → [IsFractionRing R K] → FractionalIdeal (nonZeroDivisors R) K →*₀ ℚ
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebraStruct.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [toBialgebra : Bialgebra R A] → (A →ₗ[R] A) → HopfAlgebraStruct R A
-- Mathlib.Order.Filter.Pi
Filter.tendsto_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : Type u_3} {m : β → (i : ι) → α i} {l : Filter β},
  Filter.Tendsto m l (Filter.pi f) ↔ ∀ (i : ι), Filter.Tendsto (fun x => m x i) l (f i)
-- Mathlib.Algebra.Group.Hom.Basic
coe_negAddMonoidHom : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α], ⇑negAddMonoidHom = Neg.neg
-- Mathlib.GroupTheory.Nilpotent
/-- Nilpotency respects isomorphisms.  -/
AddGroup.nilpotent_of_addEquiv : ∀ {G : Type u_1} [inst : AddGroup G] {G' : Type u_2} [inst_1 : AddGroup G'] [_h : AddGroup.IsNilpotent G] (f : G ≃+ G'),
  AddGroup.IsNilpotent G'
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((_ : α) × β)}
  {toInsert : List (α × β)} {k : α},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getKey! k (Std.Internal.List.insertListConst l toInsert) = Std.Internal.List.getKey! k l
-- Mathlib.Analysis.InnerProductSpace.Positive
Matrix.posSemidef_iff_eq_sum_vecMulVec : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_4} [Finite n] {M : Matrix n n 𝕜},
  M.PosSemidef ↔ ∃ m v, M = ∑ i, Matrix.vecMulVec (v i) (star (v i))
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorPrebundle.contMDiffCoordChange_apply : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsContMDiff IB a n]
  {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas)
  (he' : e' ∈ a.pretrivializationAtlas) {b : B},
  b ∈ e.baseSet ∩ e'.baseSet →
    ∀ (v : F), (VectorPrebundle.contMDiffCoordChange n IB a he he' b) v = (↑e' ⟨b, e.symm b v⟩).2
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instSemilatticeInfClosedSubgroup : (G : Type u) → [inst : Group G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (ClosedSubgroup G)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- All open cells are disjoint with the base. Use `RelCWComplex.disjointBase` instead.  -/
Topology.RelCWComplex.disjointBase' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Disjoint (↑(Topology.RelCWComplex.map n i) '' Metric.ball 0 1) D
-- Mathlib.Analysis.Normed.Field.Lemmas
tendsto_norm_inv_nhdsNE_zero_atTop : ∀ {α : Type u_1} [inst : NormedDivisionRing α], Filter.Tendsto (fun x => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  (val val_1 : A.obj ⟶ B.obj) (e_val : val = val_1)
  (comp : (CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt),
  { val := val, comp := comp } = { val := val_1, comp := ⋯ }
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_isLink : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (e : β) (x y : α),
  (G.deleteEdges F).IsLink e x y = (G.IsLink e x y ∧ e ∉ F)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.addUnit.eq_1 : ∀ {M : Type u_6} [inst : AddMonoid M] {x : M} (hx : IsOfFinAddOrder x),
  hx.addUnit = { val := x, neg := (addOrderOf x - 1) • x, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.move.injEq : ∀ {Γ : Type u_1} (a a_1 : Turing.Dir), (Turing.TM0.Stmt.move a = Turing.TM0.Stmt.move a_1) = (a = a_1)
-- Std.Data.TreeSet.Basic
/-- Internal implementation detail of the tree map.  -/
Std.TreeSet.inner : {α : Type u} → {cmp : autoParam (α → α → Ordering) Std.TreeSet._auto_1} → Std.TreeSet α cmp → Std.TreeMap α Unit cmp
-- Mathlib.Topology.Order
le_induced_generateFrom : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β},
  (∀ a ∈ b, IsOpen (f ⁻¹' a)) → t ≤ TopologicalSpace.induced f (TopologicalSpace.generateFrom b)
-- Mathlib.Topology.UniformSpace.Completion
/-- Lift a two variable map to the Hausdorff completions.  -/
UniformSpace.Completion.map₂ : {α : Type u_1} →
  [inst : UniformSpace α] →
    {β : Type u_2} →
      [inst_1 : UniformSpace β] →
        {γ : Type u_3} →
          [inst_2 : UniformSpace γ] →
            (α → β → γ) → UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ
-- Mathlib.Data.Finset.Filter
Finset.mem_of_mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, ∀ x ∈ Finset.filter p s, x ∈ s