mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.TensorProduct
/-- A weaker form of the universal property for tensor product of modules of a Lie algebra.

Note that maps `f` of type `M →ₗ⁅R,L⁆ N →ₗ[R] P` are exactly those `R`-bilinear maps satisfying
`⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆` for all `x, m, n` (see e.g, `LieModuleHom.map_lie₂`).  -/
TensorProduct.LieModule.liftLie : (R : Type u) →
  [inst : CommRing R] →
    (L : Type v) →
      (M : Type w) →
        (N : Type w₁) →
          (P : Type w₂) →
            [inst_1 : LieRing L] →
              [inst_2 : LieAlgebra R L] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : LieRingModule L M] →
                      [inst_6 : LieModule R L M] →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : Module R N] →
                            [inst_9 : LieRingModule L N] →
                              [inst_10 : LieModule R L N] →
                                [inst_11 : AddCommGroup P] →
                                  [inst_12 : Module R P] →
                                    [inst_13 : LieRingModule L P] →
                                      [inst_14 : LieModule R L P] →
                                        (M →ₗ⁅R,L⁆ N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ⁅R,L⁆ P
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `I` is be ideal of `R`,
then `S ⊗[R] M ⧸ I(S ⊗[R] M)` is isomorphic to `S ⊗[R] (M ⧸ IM)` as `S` modules.  -/
TensorProduct.tensorQuotMapSMulEquivTensorQuot : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (S : Type u_4) →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                (I : Ideal R) →
                  (TensorProduct R S M ⧸ Ideal.map (algebraMap R S) I • ⊤) ≃ₗ[S] TensorProduct R S (M ⧸ I • ⊤)
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.eq_cast_iff_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v'),
  e' = Quiver.Hom.cast hu hv e ↔ e' ≍ e
-- Mathlib.Computability.TuringMachine.Tape
/-- The `nth` function of a tape is integer-valued, with index `0` being the head, negative indexes
on the left and positive indexes on the right. (Picture a number line.)  -/
Turing.Tape.nth : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → ℤ → Γ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  Finset.map AddOpposite.opEquiv.toEmbedding (s + t) =
    Finset.map AddOpposite.opEquiv.toEmbedding t + Finset.map AddOpposite.opEquiv.toEmbedding s
-- Std.Http.Data.Method
/-- Unlock a resource.
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.11
 -/
Std.Http.Method.unlock : Std.Http.Method
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.add_toPreZeroHypercover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : Y ⟶ X)
  (hf : autoParam (P f) AlgebraicGeometry.Scheme.Cover.add._auto_1), (𝒰.add f hf).toPreZeroHypercover = 𝒰.add f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Units.coe_prod : ∀ {M : Type u_3} {α : Type u_6} [inst : CommMonoid M] (f : α → Mˣ) (s : Finset α), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- Composing two open partial homeomorphisms, by restricting to the maximal domain where their
composition is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ₕ f` for this.  -/
OpenPartialHomeomorph.trans : {X : Type u_1} →
  {Y : Type u_3} →
    {Z : Type u_5} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            OpenPartialHomeomorph X Y → OpenPartialHomeomorph Y Z → OpenPartialHomeomorph X Z
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f.right F),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.right = g.right
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_le_of_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {n : ι}, (∀ (ω : Ω), τ ω ≤ ↑n) → hτ.measurableSpace ≤ m
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDF_scale_zero : ∀ (x₀ : ℝ), ProbabilityTheory.cauchyPDF x₀ 0 = 0
-- Init.Data.SInt.Lemmas
Int16.mul_neg : ∀ (a b : Int16), a * -b = -(a * b)
-- Mathlib.Analysis.SpecificLimits.Basic
NNReal.tendsto_pow_atTop_nhds_zero_iff : ∀ {r : NNReal}, Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0) ↔ r < 1
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph},
  M.IsPerfectMatching → G'.IsAlternating M.spanningCoe → G'.IsCycles → ⊤.IsPerfectMatching
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubsemiring_subtype : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.subtype = ↑S.val
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.instDiffeologicalSpaceEuclideanSpaceRealOfFintype : {ι : Type u_1} → [Fintype ι] → DiffeologicalSpace (EuclideanSpace ℝ ι)
-- Mathlib.Logic.Relator
Relator.rel_and : Relator.LiftFun (fun x1 x2 => x1 ↔ x2) (Relator.LiftFun (fun x1 x2 => x1 ↔ x2) fun x1 x2 => x1 ↔ x2)
  (fun x1 x2 => x1 ∧ x2) fun x1 x2 => x1 ∧ x2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_filter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Bool}, t.Ordered → (Std.DTreeMap.Internal.Impl.filter f t h).impl.Ordered
-- Init.Tactics
/-- Extracts `let` and `have` expressions from within the target or a local hypothesis,
introducing new local definitions.

- `extract_lets` extracts all the lets from the target.
- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
  Using `_` for a name leaves it unnamed.
- `extract_lets x y z at h` operates on the local hypothesis `h` instead of the target.

For example, given a local hypotheses if the form `h : let x := v; b x`, then `extract_lets z at h`
introduces a new local definition `z := v` and changes `h` to be `h : b z`.
 -/
Lean.Parser.Tactic.extractLets : Lean.ParserDescr
-- Mathlib.RingTheory.Congruence.Hom
/-- The **third isomorphism theorem for algebras**.  -/
RingCon.quotientQuotientEquivQuotientₐ : {M : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring M] →
        [inst_2 : Algebra R M] →
          {c d : RingCon M} → (h : c ≤ d) → (RingCon.ker ↑(RingCon.factorₐ R h)).Quotient ≃ₐ[R] d.Quotient
-- Mathlib.Order.Heyting.Hom
/-- `id` as a `BiheytingHom`.  -/
BiheytingHom.id : (α : Type u_2) → [inst : BiheytingAlgebra α] → BiheytingHom α α
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {A B : C}, CategoryTheory.Limits.imageSubobject 0 = ⊥
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileM.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : MonadAttach m] {P : β → m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) (hP : MonadAttach.CanReturn (P out) { down := false })
  (h_1 : (hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩)
  (h_2 : (hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩),
  (match ⟨{ down := false }, hP⟩ with
    | ⟨{ down := true }, hP⟩ => h_1 hP
    | ⟨{ down := false }, hP⟩ => h_2 hP) =
    h_2 hP
-- Init.Data.String.Lemmas.Order
String.Pos.not_endPos_lt : ∀ {s : String} {p : s.Pos}, ¬s.endPos < p
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.mul_one : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation.below ⋯
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_zero_iff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_eq_zero_iff._auto_1 → (μ.real s = 0 ↔ μ s = 0)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_sum : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Semiring S] (f : M → N)
  (x : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M),
  MonoidAlgebra.mapDomain f (x.coeff.sum v) = x.coeff.sum fun a b => MonoidAlgebra.mapDomain f (v a b)
-- Init.Data.Array.Find
Array.getElem_zero_flatten.proof : ∀ {α : Type u_1} {xss : Array (Array α)}, 0 < xss.flatten.size → (Array.findSome? (fun xs => xs[0]?) xss).isSome = true
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_b₂ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).b₂ = f W.b₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Batteries.Data.List.Basic
/-- `Subperm l₁ l₂`, denoted `l₁ <+~ l₂`, means that `l₁` is a sublist of
a permutation of `l₂`. This is an analogue of `l₁ ⊆ l₂` which respects
multiplicities of elements, and is used for the `≤` relation on multisets.
 -/
List.«term_<+~_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instSMulCommClass : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] (I : Ideal R) (M : Type u_4)
  [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : SMul S R] [inst_4 : SMul T R] [inst_5 : SMul S M]
  [inst_6 : SMul T M] [inst_7 : IsScalarTower S R M] [inst_8 : IsScalarTower T R M] [SMulCommClass S T M],
  SMulCommClass S T (AdicCompletion I M)
-- Init.GrindInstances.Ring.UInt
UInt32.intCast_neg : ∀ (x : ℤ), ↑(-x) = -↑x
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_odd : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k m : ℤ),
  complEDS b c d k (2 * m + 1) =
    complEDS b c d k m ^ 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) -
      complEDS b c d k (m + 1) ^ 2 * normEDS b c d (m * k + 1) * normEDS b c d (m * k - 1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T},
  (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id T)).obj f = f
-- Mathlib.Data.DFinsupp.Lex
/-- The partial order on `DFinsupp`s obtained by the lexicographic ordering.
See `DFinsupp.Lex.linearOrder` for a proof that this partial order is in fact linear.  -/
DFinsupp.Lex.partialOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [LinearOrder ι] → [(i : ι) → PartialOrder (α i)] → PartialOrder (Lex (Π₀ (i : ι), α i))
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_lt_top : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.levyProkhorovEDist μ ν < ⊤
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
smoothingSeminorm.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (μ μ_1 : RingSeminorm R) (e_μ : μ = μ_1) (hμ1 : μ 1 ≤ 1)
  (hna : IsNonarchimedean ⇑μ), smoothingSeminorm μ hμ1 hna = smoothingSeminorm μ_1 ⋯ ⋯
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_residueFieldMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (Y.residue (f x)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) (X.residue x)
-- Lean.Meta.Tactic.Simp.Main
/-- Try to rewrite `e` children using the given congruence theorem  -/
Lean.Meta.Simp.trySimpCongrTheorem? : Lean.Meta.SimpCongrTheorem → Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.aeval_eq_of_algebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f : Polynomial S)
  (p : Polynomial R), (Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) (Polynomial.map (algebraMap R S) p)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.smul_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : MeasurableConstSMul G α] (c : G), ⇑(MeasurableEquiv.smul c) = fun x => c • x
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divLeft_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a a_1 : α),
  (OrderIso.divLeft a) a_1 = OrderDual.toDual (a / a_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_lt_of_sum_lt : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] {f g : ι → M} {s : Finset ι}
  [AddLeftMono M], ∑ i ∈ s, f i < ∑ i ∈ s, g i → ∃ i ∈ s, f i < g i
-- Lean.MetavarContext
Lean.LocalInstance.fvar : Lean.LocalInstance → Lean.Expr
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_self : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∧ P ⊣⊢ₛ P
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The canonical linear map from `M₂ ⊗[R₂] (P →ₛₗ[σ₁₂] N₂)` to `P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂`.  -/
TensorProduct.lTensorHomToHomLTensor : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (P : Type u_9) →
            (M₂ : Type u_12) →
              (N₂ : Type u_14) →
                [inst_2 : AddCommMonoid P] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : AddCommMonoid N₂] →
                      [inst_5 : Module R₂ M₂] →
                        [inst_6 : Module R₂ N₂] →
                          [inst_7 : Module R P] →
                            TensorProduct R₂ M₂ (P →ₛₗ[σ₁₂] N₂) →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Mathlib.Algebra.Category.Ring.Constructions
_private.Mathlib.Algebra.Category.Ring.Constructions.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.left with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_1 ()
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_smul_of_isUnit : ∀ {R : Type u} [inst : CommSemiring R] {r : R},
  IsUnit r → ∀ (s : Set R), PrimeSpectrum.zeroLocus (r • s) = PrimeSpectrum.zeroLocus s
-- Init.MetaTypes
/-- If `implicitDefEqProofs := true`, `simp` does not create proof terms when the
input and output terms are definitionally equal.
 -/
Lean.Meta.Simp.Config.implicitDefEqProofs : Lean.Meta.Simp.Config → Bool
-- Init.Data.String.Basic
/-- Constructs a valid position on `t` from a valid position on `s` and a proof that `s = t`.  -/
String.Pos.cast : {s t : String} → s.Pos → s = t → t.Pos
-- Lean.Server.Completion.CompletionInfoSelection
/-- Finds all `CompletionInfo`s (both from the `InfoTree` and synthetic ones), prioritizes them,
arranges them in partitions of `CompletionInfo`s with the same priority and sorts these partitions
so that `CompletionInfo`s with the highest priority come first.
The returned `CompletionInfo`s are also tagged with their index in `findCompletionInfosAt` so that
when resolving a `CompletionItem`, we can reconstruct which `CompletionInfo` it was created from.

In general, the `InfoTree` may contain multiple different `CompletionInfo`s covering `hoverPos`,
and so we need to decide which of these `CompletionInfo`s we want to use to show completions to the
user. We choose priorities by the following rules:
- Synthetic completions have the lowest priority since they are only intended as a backup.
- Non-identifier completions have the highest priority since they tend to be much more helpful than
  identifier completions when available since there are typically way too many of the latter.
- Within the three groups [non-id completions, id completions, synthetic completions],
  `CompletionInfo`s with a smaller range are considered to be better.
 -/
Lean.Server.Completion.findPrioritizedCompletionPartitionsAt : Lean.FileMap →
  String.Pos.Raw →
    Lean.Syntax → Lean.Elab.InfoTree → Array (Array (Lean.Server.Completion.ContextualizedCompletionInfo × ℕ)) × Bool
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {T : F →L[ℝ] F},
  (↑T).IsSymmetric → ∀ (x₀ : F), HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_tensorLId_apply : ∀ {R : Type uR} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [inst_3 : Invertible 2] (Q₂ : QuadraticForm R M₂) (x : TensorProduct R R M₂),
  Q₂ ((TensorProduct.lid R M₂) x) = (QuadraticForm.tmul QuadraticMap.sq Q₂) x
-- Mathlib.CategoryTheory.Shift.Localization
/-- The localized category `W.Localization` is endowed with the induced shift.  -/
CategoryTheory.HasShift.localization : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [W.IsCompatibleWithShift A] → CategoryTheory.HasShift W.Localization A
-- Mathlib.GroupTheory.Sylow
QuotientGroup.card_preimage_mk : ∀ {G : Type u} [inst : Group G] (s : Subgroup G) (t : Set (G ⧸ s)),
  Nat.card ↑(QuotientGroup.mk ⁻¹' t) = Nat.card ↥s * Nat.card ↑t
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.ext_iff : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type v} {x y : Std.Iterators.HetT m α},
  x = y ↔
    ∃ (h : x.Property = y.Property),
      ∀ (β : Type w) (f : (a : α) → x.Property a → m β), x.prun f = y.prun fun a ha => f a ⋯
-- Batteries.Data.List.Lemmas
List.le_getElem_findIdxs : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ} (h : i < (List.findIdxs p xs s).length),
  s ≤ (List.findIdxs p xs s)[i]
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∉ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size
-- Batteries.Lean.NameMapAttribute
/-- The inputs to `registerNameMapAttribute`.  -/
Lean.NameMapAttributeImpl : Type → Type
-- Mathlib.CategoryTheory.Limits.Final
/-- If `F` is initial and `F ⋙ G` creates limits of `H`, then so does `G`.  -/
CategoryTheory.Functor.Initial.createsLimitOfComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  {B : Type u₄} →
                    [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                      {H : CategoryTheory.Functor E B} →
                        [CategoryTheory.CreatesLimit (F.comp G) H] → CategoryTheory.CreatesLimit G H
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.mk.injEq : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) (i : I) (a : D.obj i ⟶ X)
  (ha : t.app i = CategoryTheory.CategoryStruct.comp a f) (b : D.obj i ⟶ X)
  (hb : t.app i = CategoryTheory.CategoryStruct.comp b f)
  (hab : CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app i) b)
  (𝒰S : S.OpenCover) [h𝒰S : ∀ (i : 𝒰S.I₀), AlgebraicGeometry.IsAffine (𝒰S.X i)]
  (𝒰X :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).X i).OpenCover)
  [h𝒰X :
    ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) (j : (𝒰X i).I₀),
      AlgebraicGeometry.IsAffine ((𝒰X i).X j)]
  (c_1 : CategoryTheory.Limits.Cone D) (hc_1 : CategoryTheory.Limits.IsLimit c_1) (i_1 : I) (a_1 : D.obj i_1 ⟶ X)
  (ha_1 : t.app i_1 = CategoryTheory.CategoryStruct.comp a_1 f) (b_1 : D.obj i_1 ⟶ X)
  (hb_1 : t.app i_1 = CategoryTheory.CategoryStruct.comp b_1 f)
  (hab_1 :
    CategoryTheory.CategoryStruct.comp (c_1.π.app i_1) a_1 = CategoryTheory.CategoryStruct.comp (c_1.π.app i_1) b_1)
  (𝒰S_1 : S.OpenCover) (h𝒰S_1 : ∀ (i : 𝒰S_1.I₀), AlgebraicGeometry.IsAffine (𝒰S_1.X i))
  (𝒰X_1 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).X i).OpenCover)
  (h𝒰X_1 :
    ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).I₀) (j : (𝒰X_1 i).I₀),
      AlgebraicGeometry.IsAffine ((𝒰X_1 i).X j)),
  ({ c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := 𝒰S, h𝒰S := h𝒰S, 𝒰X := 𝒰X,
        h𝒰X := h𝒰X } =
      { c := c_1, hc := hc_1, i := i_1, a := a_1, ha := ha_1, b := b_1, hb := hb_1, hab := hab_1, 𝒰S := 𝒰S_1,
        h𝒰S := h𝒰S_1, 𝒰X := 𝒰X_1, h𝒰X := h𝒰X_1 }) =
    (c = c_1 ∧ hc ≍ hc_1 ∧ i = i_1 ∧ a ≍ a_1 ∧ b ≍ b_1 ∧ 𝒰S = 𝒰S_1 ∧ 𝒰X ≍ 𝒰X_1)
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalFinOfNeZeroNat_qq : {n : ℕ} → [NeZero n] → Lean.Meta.ReduceEval (Fin n)
-- Init.Data.SInt.Lemmas
Int16.le_rfl : ∀ {a : Int16}, a ≤ a
-- Mathlib.Geometry.Manifold.IsManifold.Basic
modelWithCorners_prod_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H)
  (I' : ModelWithCorners 𝕜 E' H'), ↑(I.prod I') = Prod.map ↑I ↑I'
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- If a measurable equivalence is ergodic, then so is the inverse map.  -/
Ergodic.symm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α},
  Ergodic (⇑e) μ → Ergodic (⇑e.symm) μ
-- Mathlib.Control.Monad.Cont
ContT.instMonad : {r : Type u} → {m : Type u → Type v} → Monad (ContT r m)