mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Quotient
IsometryEquiv.divLeft.congr_simp : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c c_1 : G), c = c_1 → IsometryEquiv.divLeft c = IsometryEquiv.divLeft c_1
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
IsGroupLikeElem.antipode : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {a : A},
  IsGroupLikeElem R a → IsGroupLikeElem R ((HopfAlgebraStruct.antipode R) a)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairEquiv_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D'),
  (CategoryTheory.Join.mapPairEquiv e e').counitIso =
    (CategoryTheory.Join.mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
      CategoryTheory.Join.mapIsoWhiskerRight e.counitIso (e'.inverse.comp e'.functor) ≪≫
        CategoryTheory.Join.mapIsoWhiskerLeft (CategoryTheory.Functor.id C') e'.counitIso ≪≫
          CategoryTheory.Join.mapPairId
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f f_1 : X ⟶ K.X q)
  (e_f : f = f_1) {n : ℤ} (h : p + n = q) (q' q'_1 : ℤ) (e_q' : q' = q'_1) (hq' : q + 1 = q')
  (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0),
  CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf =
    CochainComplex.HomComplex.Cocycle.fromSingleMk f_1 h q'_1 ⋯ ⋯
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar.eq_1 : ∀ (bytes : ByteArray) (i : ℕ) (h : (bytes.utf8DecodeChar? i).isSome = true),
  bytes.utf8DecodeChar i h = (bytes.utf8DecodeChar? i).get h
-- Init.Data.SInt.Lemmas
Int8.lt_asymm : ∀ {a b : Int8}, a < b → ¬b < a
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.args : Lean.AttributeExtensionOLeanEntry → List Lean.DataValue
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_top : ∀ {V : Type u} {v : V}, ⊤.neighborSet v = {v}ᶜ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables, general form for scalar functions. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
`f '' [a, b]`, and `(g ∘ f) x * f' x` is integrable on `[a, b]`, then we can substitute `u = f x`
to get `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
 -/
intervalIntegral.integral_comp_mul_deriv''' : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn g (f '' Set.Ioo (min a b) (max a b)) →
        MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume →
          MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) (Set.uIcc a b) MeasureTheory.volume →
            ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfSet_isMaximal_iff : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  (s : TopologicalSpace.Opens X), (ContinuousMap.idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s
-- Mathlib.Order.BooleanAlgebra.Basic
/-- Transfer `GeneralizedBooleanAlgebra` across an `Equiv`.  -/
Equiv.generalizedBooleanAlgebra : {α : Type u} → {β : Type u_1} → α ≃ β → [GeneralizedBooleanAlgebra β] → GeneralizedBooleanAlgebra α
-- Init.Data.Array.Find
Array.find?_replicate_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool}, Array.find? p (Array.replicate n a) = none ↔ n = 0 ∨ (!p a) = true
-- Mathlib.Topology.Compactness.LocallyCompact
/-- In general it suffices that all but finitely many of the spaces are compact,
but that's not straightforward to state and use.  -/
Pi.locallyCompactSpace_of_finite : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyCompactSpace (X i)]
  [Finite ι], LocallyCompactSpace ((i : ι) → X i)
-- Mathlib.Order.Atoms
GaloisInsertion.isCoatom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α] [IsCoatomic α]
  [inst_4 : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u),
  (∀ (a : α), IsCoatom a → u (l a) = a) → ∀ (b : β), IsCoatom (u b) ↔ IsCoatom b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_smul_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P ≈ Q → ∀ {u v : R}, IsUnit u → IsUnit v → W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q
-- Mathlib.Algebra.Order.Group.PosPart
negPart_min : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α), (a ⊓ b)⁻ = a⁻ ⊔ b⁻
-- Mathlib.Data.Multiset.Dedup
/-- Note that the stronger `List.Subset.dedup_append_right` is proved earlier.  -/
List.Subset.dedup_append_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : List α}, t ⊆ s → (s ++ t).dedup.Perm s.dedup
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.instHasLeftResolutionsOppositeOpOpOfHasRightResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.HasRightResolutions],
  Φ.op.HasLeftResolutions
-- Init.Data.Function
Function.injective_id : ∀ {α : Sort u_1}, Function.Injective id
-- Mathlib.Data.Fintype.Perm
Equiv.instFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → [DecidableEq β] → [Fintype α] → [Fintype β] → Fintype (α ≃ β)
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.basis_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V)
  (ibc : IsBaseChange S ε) (i : ι), (IsBaseChange.basis b ibc) i = ε (b i)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj { len := 0 }))
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isDivInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_residue_zero : Filter.Tendsto (fun s => s * s.Gammaℝ) (nhdsWithin 0 {0}ᶜ) (nhds 2)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instStarAddMonoid : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : Nonempty ι] →
                  [inst_5 : (i : ι) → AddMonoid (G i)] →
                    [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] →
                      [inst_7 : (i : ι) → StarAddMonoid (G i)] →
                        [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] → StarAddMonoid (DirectLimit G f)
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator.eq_1 : ∀ (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],
  CategoryTheory.sum.inverseAssociator C D E =
    ((CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
      (((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
        (CategoryTheory.Sum.inr_ (C ⊕ D) E))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddRightReflectLE.mk : ∀ {M : Type u_1} [inst : Add M] [inst_1 : LE M], (∀ {b a₁ a₂ : M}, a₁ + b ≤ a₂ + b → a₁ ≤ a₂) → AddRightReflectLE M
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqEMatchDiagNode : BEq Lean.Meta.Grind.EMatchDiagNode
-- Lean.Util.PPExt
Lean.PPFns.ppLevel : Lean.PPFns → Lean.PPContext → Lean.Level → IO Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_hom_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr.op h
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α),
  Std.DTreeMap.Internal.Impl.getKeyLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.SetTheory.Ordinal.Basic
/-- The `#s`-th element of `α` is an upper-bound for the set's mex (minimum excluded value),
ordered by `r`, when `s` is finite. See `card_typein_min_le_mk` for the `Ordinal` version.  -/
Ordinal.not_lt_enum_ord_mk_min_compl : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty),
  ¬r ((Ordinal.enum r) ⟨(Cardinal.mk ↑s).ord, ⋯⟩) (⋯.min sᶜ h)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  Function.Surjective ⇑e
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.addCommMonoidObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) (j : J),
  AddCommMonCat.addCommMonoidObj F j =
    { toAdd := AddCommMonCat.addCommMonoidObj._aux_1 F j, add_assoc := ⋯,
      toZero := AddCommMonCat.addCommMonoidObj._aux_4 F j, zero_add := ⋯, add_zero := ⋯,
      toNSMul := AddCommMonCat.addCommMonoidObj._aux_8 F j, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureInformation.fromJson : Lean.Json → Except String Lean.Lsp.SignatureInformation
-- Mathlib.SetTheory.Ordinal.Notation
/-- This is a recursor-like theorem for `NONote` suggesting an inductive definition, which can't
actually be defined this way due to conflicting dependencies.  -/
NONote.recOn : {C : NONote → Sort u_1} →
  (o : NONote) → C 0 → ((e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)) → C o
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.compatible_singleton_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (f : X ⟶ Y) (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.singleton f)),
  x.Compatible ↔
    ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      CategoryTheory.CategoryStruct.comp p₁ f = CategoryTheory.CategoryStruct.comp p₂ f →
        (CategoryTheory.ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) =
          (CategoryTheory.ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)
-- Mathlib.Analysis.LocallyConvex.Separation
/-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is
closed, and `t` is compact, there is a continuous linear functional which strongly separates them.
 -/
geometric_hahn_banach_closed_compact : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  Convex ℝ s →
    IsClosed s → Convex ℝ t → IsCompact t → Disjoint s t → ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
-- Mathlib.Logic.Equiv.Prod
Equiv.arrowProdEquivProdArrow_symm_apply : ∀ (α : Type u_9) (β : α → Type u_10) (γ : α → Type u_11) (p : ((i : α) → β i) × ((i : α) → γ i)) (c : α),
  (Equiv.arrowProdEquivProdArrow α β γ).symm p c = (p.1 c, p.2 c)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.symm : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → g.Disjoint f
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_toArray : ∀ {α : Type u_1} {xs : Subarray α}, (Std.Slice.toArray xs).toList = Std.Slice.toList xs
-- Mathlib.Topology.Covering.Basic
/-- If `x : X` is evenly covered by `f` with fiber `I`, then `I` is homeomorphic to `f ⁻¹' {x}`.  -/
IsEvenlyCovered.fiberHomeomorph : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {I : Type u_3} → [inst_2 : TopologicalSpace I] → {x : X} → IsEvenlyCovered f x I → I ≃ₜ ↑(f ⁻¹' {x})
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_limsup_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Indep (Filter.limsup s f) (Filter.limsup s f) μ
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.orderIsoOfIso_apply : ∀ {X Y : SSet} (e : X ≅ Y) (x : X.N),
  (SSet.N.orderIsoOfIso e) x =
    SSet.N.mk ((CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim }))) x.simplex) ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If the range of an injective indexed family of points is affinely
independent, so is that family.  -/
AffineIndependent.of_set_of_injective : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  (AffineIndependent k fun x => ↑x) → Function.Injective p → AffineIndependent k p
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
-- Mathlib.Data.Set.Subset
Set.image_val_union_self_right_eq : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, A ∪ Subtype.val '' D = A
-- Mathlib.Computability.RecursiveIn
recursiveIn_empty_iff : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ},
  RecursiveIn ∅ f ↔ Partrec f
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousAt.fun_const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β}, ContinuousAt g b → ∀ (c : M), ContinuousAt (fun i => c +ᵥ g i) b
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.starProjection_eq_sum_rankOne : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection]
  (b : OrthonormalBasis ι 𝕜 ↥U), U.starProjection = ∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)
-- Mathlib.Topology.Category.Compactum
/-- The structure map of a compactum actually computes limits.  -/
Compactum.lim_eq_str : ∀ {X : Compactum} (F : Ultrafilter X.A), F.lim = X.str F
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.parallelepiped_map : ∀ {ι : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] (b : Module.Basis ι ℝ E)
  (e : E ≃ₗ[ℝ] F), (b.map e).parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑e ⋯ ⋯ b.parallelepiped
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_neg_of_lt : ∀ {n k : ℕ}, n < k → (ascPochhammer ℕ k).smeval (-↑n) = 0
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel κ.snd
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- Euler's homogeneous function theorem in Jacobian coordinates.  -/
WeierstrassCurve.Jacobian.polynomial_relation : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  6 * (MvPolynomial.eval P) W'.polynomial =
    2 * P 0 * (MvPolynomial.eval P) W'.polynomialX + 3 * P 1 * (MvPolynomial.eval P) W'.polynomialY +
      P 2 * (MvPolynomial.eval P) W'.polynomialZ
-- Mathlib.Data.Fintype.Basic
List.toFinset_finRange : ∀ (n : ℕ), (List.finRange n).toFinset = Finset.univ
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.char.sizeOf_spec : sizeOf Lean.Meta.Hint.DiffGranularity.char = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (cmp ((t.insert k).minD fallback) k).isLE = true
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.normal.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (a : Λ), sizeOf (Turing.TM2to1.Λ'.normal a) = 1 + sizeOf a
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` at `x` within a set `s`, then
`f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`
within `s × s`.  -/
HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x →
    (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[nhdsWithin (x, x) (insert x s ×ˢ insert x s)] fun y =>
      ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Init.Data.SInt.Lemmas
Int16.ofInt_mul : ∀ (a b : ℤ), Int16.ofInt (a * b) = Int16.ofInt a * Int16.ofInt b
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.mem_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P}, s₁.IsExtTangentAt s₂ p → p ∈ s₂
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → MonoidWithZero (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] →
                      MonoidWithZero (DirectLimit G f)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_iff_zero_or_omega0_opow`.

---

The main characterization theorem for additive principal ordinals.  -/
Ordinal.principal_add_iff_zero_or_omega0_opow : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x => Ordinal.omega0 ^ x
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonnegg_comm : ∀ {c d : ℕ} {x y : ℤ}, Zsqrtd.Nonnegg c d x y = Zsqrtd.Nonnegg d c y x
-- Lean.Expr
/-- The range of de-Bruijn variables that are loose.
That is, bvars that are not bound by a binder.
For example, `bvar i` has range `i + 1` and
an expression with no loose bvars has range `0`.
 -/
Lean.Expr.looseBVarRange : Lean.Expr → ℕ
-- Mathlib.Order.RelClasses
/-- Creates data, given a way to generate a value from all that compare as less under a well-founded
relation. See also `IsWellFounded.fix_eq`.  -/
IsWellFounded.fix : {α : Type u} →
  (r : α → α → Prop) →
    [IsWellFounded α r] →
      {motive : α → Sort u_1} → ((x : α) → ((y : α) → r y x → motive y) → motive x) → (x : α) → motive x
-- Mathlib.Algebra.Polynomial.Basic
/-- To prove something about polynomials,
it suffices to show the condition is closed under taking sums,
and it holds for monomials.
 -/
Polynomial.induction_on' : ∀ {R : Type u} [inst : Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R),
  (∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) →
    (∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)) → motive p
-- Mathlib.FieldTheory.Normal.Basic
/-- If a set of algebraic elements in a field extension `K/F` have minimal polynomials that
split in another extension `L/F`, then all minimal polynomials in the intermediate field
generated by the set also split in `L/F`.  -/
IntermediateField.splits_of_mem_adjoin : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {L : Type u_3}
  [inst_3 : Field L] [inst_4 : Algebra F L] {S : Set K},
  (∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    ∀ {x : K}, x ∈ IntermediateField.adjoin F S → (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_iInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), UpperSemicontinuous (f i)) → UpperSemicontinuous fun x' => ⨅ i, f i x'
-- Init.Prelude
/-- `a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. -/
HPow.hPow : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HPow α β γ] → α → β → γ
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_two_mul_add_one : ∀ (n : ℕ), (2 * n + 1).bitIndices = 0 :: List.map (fun x => x + 1) n.bitIndices
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
/-- A precoverage `K` generates the topology `J` if a presheaf on `C` is a sheaf
for `K` if and only if it is a sheaf for `J`.  -/
CategoryTheory.Precoverage.Generates : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Precoverage C → CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.Condensed.Light.Module
/-- The left adjoint to the forgetful functor. The *free light condensed `R`-module* on a light
condensed set.
 -/
LightCondensed.free : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor LightCondSet (LightCondMod R)