mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Construct an isomorphism of chain complexes from isomorphism of the objects
which commute with the differentials.  -/
HomologicalComplex.Hom.isoOfComponents : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          {C₁ C₂ : HomologicalComplex V c} →
            (f : (i : ι) → C₁.X i ≅ C₂.X i) →
              autoParam
                  (∀ (i j : ι),
                    c.Rel i j →
                      CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
                        CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom)
                  HomologicalComplex.Hom.isoOfComponents._auto_1 →
                (C₁ ≅ C₂)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.below : {L : FirstOrder.Language} →
  {α : Type u'} →
    {n : ℕ} → {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop} → {a : L.BoundedFormula α n} → a.IsQF → Prop
-- Init.Data.Order.Opposite
LE.opposite_def : ∀ {α : Type u_1} {le : LE α}, le.opposite = { le := fun a b => b ≤ a }
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.prod_single : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] (s : Finset ι)
  (m : ι → M) (r : ι → R),
  ∏ i ∈ s, AddMonoidAlgebra.single (m i) (r i) = AddMonoidAlgebra.single (∑ i ∈ s, m i) (∏ i ∈ s, r i)
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lie_of_same : ∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] [inst_1 : DecidableEq ι] {i : ι} (x y : L i),
  ⁅(DirectSum.of L i) x, (DirectSum.of L i) y⁆ = (DirectSum.of L i) ⁅x, y⁆
-- Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
/-- A unit trinomial is irreducible if it has no complex roots in common with its mirror.  -/
Polynomial.IsUnitTrinomial.irreducible_of_coprime' : ∀ {p : Polynomial ℤ},
  p.IsUnitTrinomial → (∀ (z : ℂ), ¬((Polynomial.aeval z) p = 0 ∧ (Polynomial.aeval z) p.mirror = 0)) → Irreducible p
-- Mathlib.Algebra.Group.Defs
NSMul.mk : {M : Type u} → (ℕ → M → M) → NSMul M
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instField : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Field R] → (v : Valuation R Γ₀) → Field (WithVal v)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.coe_of : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type v) [inst_1 : TopologicalSpace Y],
  ↑{ carrier := Y, str := inst_1 } = Y
-- Mathlib.LinearAlgebra.Prod
Submodule.sndEquiv_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : ↥(Submodule.snd R M M₂)), (Submodule.sndEquiv R M M₂) x = (↑x).2
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment_two_eq_variance : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → ProbabilityTheory.centralMoment X 2 μ = ProbabilityTheory.variance X μ
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.congr_set_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f t μ → s =ᵐ[μ] t → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Ioi_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  0 ≤ a → (↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋₊)
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.instHasHomotopyFiberOfHasBinaryBiproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [CategoryTheory.Limits.HasBinaryBiproducts C],
  HomologicalComplex.HasHomotopyFiber φ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.append.eq_1 : ∀ (p₂ : Int.Internal.Linear.Poly) (k : ℤ), (Int.Internal.Linear.Poly.num k).append p₂ = p₂.addConst k
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_ofNat : ∀ (n : ℕ), (↑n).repr = ↑n
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
orthonormal_vecCons_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ} {v : E} {vs : Fin n → E},
  Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ (i : Fin n), inner 𝕜 v (vs i) = 0) ∧ Orthonormal 𝕜 vs
-- Lean.Linter.MissingDocs
_private.Lean.Linter.MissingDocs.0.Lean.Linter.MissingDocs.docOptStatus : Lean.Syntax → Lean.Syntax → optParam Bool false → Lean.Elab.Command.CommandElabM (Option Bool)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.mk : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsCycle → p.tail.IsHamiltonian → p.IsHamiltonianCycle
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_lt_length : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.maxIdxOn f xs h < xs.length
-- Init.Data.Int.Lemmas
Int.negOfNat_eq : ∀ {n : ℕ}, Int.negOfNat n = -Int.ofNat n
-- Mathlib.Topology.EMetricSpace.Defs
Prod.edist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x y : α × β),
  edist x y = max (edist x.1 y.1) (edist x.2 y.2)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If the canonical morphism from a cone point to a limiting cone point is an iso, then the
first cone was limiting also.
 -/
CategoryTheory.Limits.IsLimit.ofPointIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cone F} →
            (P : CategoryTheory.Limits.IsLimit r) →
              [i : CategoryTheory.IsIso (P.lift t)] → CategoryTheory.Limits.IsLimit t
-- Mathlib.Algebra.Ring.Defs
instDistribOfSemiring : {α : Type u} → [Semiring α] → Distrib α
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ext_iff : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {f f' : MultilinearMap R M₁ M₂}, f = f' ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
-- Mathlib.GroupTheory.Complement
Subgroup.instInhabitedLeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  Subgroup.instInhabitedLeftTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }
-- Mathlib.Order.Cover
CovBy.unique_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ⋖ a → c ⋖ b → a = b
-- Lean.Parser.Basic
/-- Fail if previous token is immediately followed by ':'.  -/
Lean.Parser.checkNoImmediateColon : Lean.Parser.Parser
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- The restriction of a linear map on the target to a submodule of the target given by
an inclusion.  -/
LinearMap.codRestrictOfInjective : {R : Type u_1} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      {M₃ : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R M₃] →
                      (f : M₁ →ₗ[R] M₂) →
                        (i : M₃ →ₗ[R] M₂) → Function.Injective ⇑i → (∀ (x : M₁), f x ∈ i.range) → M₁ →ₗ[R] M₃
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.mem₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (self : J.ZeroHypercover S), self.presieve₀ ∈ J.coverings S
-- Mathlib.Data.Set.Function
Function.Semiconj.mapsTo_range : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → Set.MapsTo fb (Set.range f) (Set.range f)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_whisker_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))),
  CategoryTheory.Presheaf.imageSieve (CategoryTheory.Functor.whiskerRight f (CategoryTheory.forget A)) s =
    CategoryTheory.Presheaf.imageSieve f s
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A disjoint union of completely metrizable spaces is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.sigma : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (n : ι) → TopologicalSpace (X n)]
  [∀ (n : ι), TopologicalSpace.IsCompletelyMetrizableSpace (X n)],
  TopologicalSpace.IsCompletelyMetrizableSpace ((n : ι) × X n)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_bot : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊥ = ∅
-- Mathlib.Data.List.Defs
List.iterateTR_loop_eq : ∀ {α : Type u_1} (f : α → α) (a : α) (n : ℕ) (l : List α), List.iterateTR.loop f a n l = l.reverse ++ List.iterate f a n
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instPartialOrder : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → PartialOrder (TwoSidedIdeal R)
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- Let `S` be a nontrivial additive subgroup in an archimedean linear ordered
additive commutative group `G` with order topology. If the set of positive elements of `S` does not
have a minimal element, then `S` is dense `G`.  -/
AddSubgroup.dense_of_no_min : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] (S : AddSubgroup G), S ≠ ⊥ → (¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a) → Dense ↑S
-- Mathlib.Algebra.Order.Hom.Monoid
instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : FunLike F α β] [inst_5 : OrderHomClass F α β] [inst_6 : AddMonoidHomClass F α β],
  instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass = { coe := OrderMonoidHomClass.toOrderAddMonoidHom }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_int_cert.eq_1 : ∀ (e : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.norm_int_cert e p = e.toPoly_k.beq' p
-- Mathlib.Data.List.Sort
List.SortedGT.sortedGE : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, l.SortedGT → l.SortedGE
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.normBound.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S),
  ClassGroup.normBound abv bS =
    (Fintype.card ι).factorial •
      (Fintype.card ι •
          (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^
        Fintype.card ι
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Any left Kan extension along the Yoneda embedding preserves colimits.  -/
CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.one_lt_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a : α}, 1 < a⁻¹ ↔ a < 1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The norm of the difference of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is π.  -/
InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 → y ≠ 0 → (‖x - y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi)
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_iff_is_torsion_by_span : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Module.IsTorsionBySet R M s ↔ Module.IsTorsionBySet R M ↑(Ideal.span s)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.brecOn.go : {motive : ONote → Sort u} → (t : ONote) → ((t : ONote) → ONote.below t → motive t) → motive t ×' ONote.below t
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.mk.sizeOf_spec : ∀ (base : Lean.VisibilityMap✝ Lean.Kernel.Environment) (serverBaseExts : Array Lean.EnvExtensionState)
  (checked : Task Lean.Kernel.Environment) (asyncConstsMap : Lean.VisibilityMap✝ Lean.AsyncConsts✝)
  (asyncCtx? : Option Lean.AsyncContext✝) (importRealizationCtx? : Option Lean.RealizationContext✝)
  (localRealizationCtxMap : Lean.NameMap Lean.RealizationContext✝)
  (allRealizations : Task (Lean.NameMap Lean.AsyncConst✝)) (isExporting : Bool),
  sizeOf
      { base := base, serverBaseExts := serverBaseExts, checked := checked, asyncConstsMap := asyncConstsMap,
        asyncCtx? := asyncCtx?, importRealizationCtx? := importRealizationCtx?,
        localRealizationCtxMap := localRealizationCtxMap, allRealizations := allRealizations,
        isExporting := isExporting } =
    1 + sizeOf base + sizeOf serverBaseExts + sizeOf checked + sizeOf asyncConstsMap + sizeOf asyncCtx? +
            sizeOf importRealizationCtx? +
          sizeOf localRealizationCtxMap +
        sizeOf allRealizations +
      sizeOf isExporting
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNNRat_lt_false : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a na da →
    Mathlib.Meta.NormNum.IsNNRat b nb db → decide (nb * da ≤ na * db) = true → ¬a < b
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instLeAtTopSymmetricIoc : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] [NoBotOrder G], (SummationFilter.symmetricIoc G).LeAtTop
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
basisOfLinearIndependentOfCardEqFinrank.congr_simp : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {b b_1 : ι → V} (e_b : b = b_1) (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = Module.finrank K V),
  basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank ⋯ card_eq
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderComposition], CategoryTheory.MorphismProperty.isomorphisms C ≤ P → P.RespectsIso
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafExt_inv : ∀ {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (S : LightProfiniteᵒᵖ)
  (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G),
  (LightCondensed.lanPresheafExt i).inv.app S =
    CategoryTheory.Limits.colimMap
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op S).whiskerLeft i.inv)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact)
  (f : S₁ ⟶ S₂),
  (CategoryTheory.ShortComplex.ShortExact.singleTriangle.map h₁ h₂ f).hom₁ =
    (DerivedCategory.singleFunctor C 0).map f.τ₁
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- `HasWidePullback B objs arrows` means that `wideCospan B objs arrows` has a limit.  -/
CategoryTheory.Limits.HasWidePullback : {J : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (B : C) → (objs : J → C) → ((j : J) → objs j ⟶ B) → Prop
-- Mathlib.Topology.Algebra.UniformField
/-- A topological field is completable if it is separated and the image under
the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure)
which does not have a cluster point at 0 is a Cauchy filter
(with respect to the additive uniform structure). This ensures the completion is
a field.
 -/
CompletableTopField : (K : Type u_1) → [Field K] → [UniformSpace K] → Prop
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.instBEqAlphaKey : BEq Lean.Meta.Sym.AlphaKey
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
/-- The contribution to `Finpartition.energy` of a pair of distinct parts of a `Finpartition`.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.SzemerediRegularity.distinctPairs : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {P : Finpartition Finset.univ} →
        P.IsEquipartition →
          (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → ↥P.parts.offDiag → Finset (Finset α × Finset α)
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.coe_untop₀_of_ne_top : ∀ {α : Type u_1} [inst : Zero α] {a : WithTop α}, a ≠ ⊤ → ↑a.untop₀ = a
-- Init.Prelude
Lean.instInhabitedTSyntax : {ks : Lean.SyntaxNodeKinds} → Inhabited (Lean.TSyntax ks)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.CommRing.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (k₁ k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂_1 : Lean.Grind.CommRing.Poly),
  p₁ = Lean.Grind.CommRing.Poly.num k₁ →
    p₂ = Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_1 →
      (match p₁, p₂ with
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) ≍
        h_2 k₁ k₂ m₂ p₂_1
-- Mathlib.Order.KrullDimension
/-- The **coheight** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and beginning with `a`.

This is not the definition of `coheight`. The definition of `coheight` is via the `height` in the
dual order, in order to easily transfer theorems between `height` and `coheight`.
 -/
Order.coheight_eq : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.coheight a = ⨆ p, ⨆ (_ : a ≤ RelSeries.head p), ↑p.length
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V = V') {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V' ⋯)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom i).op) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (lhs rhs cin : aig.Ref),
  Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig { lhs := lhs, rhs := rhs, cin := cin } =
    (aig.mkXorCached { lhs := lhs, rhs := rhs }).aig.mkXorCached
      { lhs := (aig.mkXorCached { lhs := lhs, rhs := rhs }).ref, rhs := cin.cast ⋯ }
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- Unexpander for the notation `|a|` for `abs a`.
Tries to add discretionary parentheses in unparsable cases.  -/
abs.unexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.comp_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (g f : CentroidHom α) (a : α), (g.comp f) a = g (f a)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.opNorm_nonneg : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), 0 ≤ ‖f‖
-- Mathlib.Topology.Connected.Basic
connectedSpace_iff_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α], ConnectedSpace α ↔ ∃ x, connectedComponent x = Set.univ
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.ne_zero_of_inner_self_ne_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] {x : F}, inner 𝕜 x x ≠ 0 → x ≠ 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (x : ↑X.toTopCat), CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
-- Mathlib.Data.Stream.Init
Stream'.get_append_left : ∀ {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) (h : n < x.length), (x ++ₛ a).get n = x[n]
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_hom_fst_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 P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl.op h
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.mul_sq_le_sum_sq : ∀ {ι : Type u_2} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s t : Finset ι}
  {x : 𝕜},
  s ⊆ t → ∀ (f : ι → 𝕜), x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card) ^ 2 → ↑s.card ≠ 0 → ↑s.card * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2