mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- The solution is infeasible.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException.infeasible : Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException
-- Init.Data.List.Control
List.forIn'.loop : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] →
        (as : List α) → ((a : α) → a ∈ as → β → m (ForInStep β)) → (as' : List α) → β → (∃ bs, bs ++ as' = as) → m β
-- Mathlib.Analysis.Convex.Between
affineSegment_same : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x : P), affineSegment R x x = {x}
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In any preadditive category, any biproduct satisfies
`∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`
 -/
CategoryTheory.Limits.biproduct.total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f],
  ∑ j,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
        (CategoryTheory.Limits.biproduct.ι f j) =
    CategoryTheory.CategoryStruct.id (⨁ f)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.toCon_injective : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R], Function.Injective fun c => c.toCon
-- Mathlib.SetTheory.ZFC.PSet
PSet.eta : ∀ (x : PSet.{u_1}), PSet.mk x.Type x.Func = x
-- Mathlib.Data.ENNReal.Inv
ENNReal.isUnit_iff : ∀ {a : ENNReal}, IsUnit a ↔ a ≠ 0 ∧ a ≠ ⊤
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the second morphism in the factorization  -/
CategoryTheory.MorphismProperty.MapFactorizationData.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {X Y : C} → {f : X ⟶ Y} → (self : W₁.MapFactorizationData W₂ f) → self.Z ⟶ Y
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Finset.Ioi a = LocallyFiniteOrderTop.finsetIoi a
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] (A : Matrix m n α) {i i' : m},
  i ≠ i' → ∀ (x y : n → α), (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.ofUpper_le_ofUpper : ∀ {α : Type u_1} [inst : Preorder α] {x y : Topology.WithUpper α},
  Topology.WithUpper.ofUpper x ≤ Topology.WithUpper.ofUpper y ↔ x ≤ y
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Z : C} (Δ : SimplexCategoryᵒᵖ)
  (F : (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) → s.N (Opposite.unop A.fst).len ⟶ Z)
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.desc Δ F) h) =
    CategoryTheory.CategoryStruct.comp (F A) h
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.withComputedSize : {α : Type u} → {β : α → Type v} → Array (Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Raw α β
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.setOfPred_root_sub_zsmul_mem_eq_Icc : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    {k | P.root j - k • P.root i ∈ Set.range ⇑P.root} =
      Set.Icc (-↑(RootPairing.chainTopCoeff i j)) ↑(RootPairing.chainBotCoeff i j)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instSMul.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.instSMul = { smul := fun a s => { carrier := (fun x => a • x) '' ↑s, lower' := ⋯ } }
-- Init.Grind.ToInt
Lean.Grind.ToInt.Mul.mk : ∀ {α : Type u} [inst : Mul α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), ↑(x * y) = I.wrap (↑x * ↑y)) → Lean.Grind.ToInt.Mul α I
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c) = 1 + sizeOf c
-- Mathlib.Algebra.Algebra.Tower
/-- R ⟶ S induces S-Alg ⥤ R-Alg  -/
AlgHom.restrictScalars : (R : Type u) →
  {S : Type v} →
    {A : Type w} →
      {B : Type u₁} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra S B] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] → [IsScalarTower R S A] → [IsScalarTower R S B] → (A →ₐ[S] B) → A →ₐ[R] B
-- Mathlib.CategoryTheory.EssentialImage
/-- Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential
image of `F`.
 -/
CategoryTheory.Functor.toEssImage : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → CategoryTheory.Functor C F.EssImageSubcategory
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKeyD.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : α) (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKeyD x = k
-- Init.Data.BitVec.Bitblast
BitVec.ne_zero_of_msb_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → x ≠ 0#w
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), MeasureTheory.Measure.haar.addCHaar K₀ K₀.toCompacts = 1
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Metric.exists_isLocalMin_mem_ball : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [ProperSpace α] [inst_2 : TopologicalSpace β]
  [inst_3 : ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a z : α} {r : ℝ},
  ContinuousOn f (Metric.closedBall a r) →
    z ∈ Metric.closedBall a r → (∀ z' ∈ Metric.sphere a r, f z < f z') → ∃ z ∈ Metric.ball a r, IsLocalMin f z
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.instTargetAffineLocallyOfIsLocal : ∀ (Q : AlgebraicGeometry.AffineTargetMorphismProperty) [Q.IsLocal],
  AlgebraicGeometry.HasAffineProperty (AlgebraicGeometry.targetAffineLocally Q) Q
-- Mathlib.Order.Atoms
IsCompl.isCoatom_iff_isAtom : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] {a b : α},
  IsCompl a b → (IsCoatom a ↔ IsAtom b)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mul.eq_3 : ∀ (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote),
  (e₁.oadd n₁ a₁).mul (e₂.oadd n₂ a₂) =
    if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ ((e₁.oadd n₁ a₁).mul a₂)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instBEqIndGroupInfo : BEq Lean.Elab.Structural.IndGroupInfo
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The type of morphisms in the category `Φ.LeftResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.Hom : {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₂} →
              {X₂ : C₂} → Φ.LeftResolution X₂ → Φ.LeftResolution X₂ → Type v_1
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (semiringInst : Lean.Expr)
  (addFn? mulFn? powFn? natCastFn? : Option Lean.Expr),
  sizeOf
      { id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?,
        powFn? := powFn?, natCastFn? := natCastFn? } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf semiringInst + sizeOf addFn? + sizeOf mulFn? + sizeOf powFn? +
      sizeOf natCastFn?
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_ofHom : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  TopCat.Hom.hom (TopCat.ofHom f) = f
-- Mathlib.Data.Prod.Lex
/-- Dictionary / lexicographic linear order for pairs.  -/
Prod.Lex.instLinearOrder : (α : Type u_3) → (β : Type u_4) → [LinearOrder α] → [LinearOrder β] → LinearOrder (Lex (α × β))
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.one_bind : ∀ {α β : Type u} (f : α → FreeGroup β), 1 >>= f = 1
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveAt_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ dt : ℝ},
  IsMIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt) ↔ IsMIntegralCurveAt γ v t₀
-- Lean.Meta.Tactic.LibrarySearch
/-- Get star-indexed lemmas (lazily computed during tree initialization).  -/
Lean.Meta.LibrarySearch.getStarLemmas : Lean.MetaM (Array (Lean.Name × Lean.Meta.LibrarySearch.DeclMod))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_left_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).left.H = S.homology
-- Mathlib.Analysis.Convex.Radon
/-- **Radon's theorem on convex sets**.

Any family `f` of affine dependent vectors contains a set `I` with the property that convex hulls of
`I` and `Iᶜ` intersect nontrivially.
In particular, any `d + 2` points in a `d`-dimensional space can be partitioned this way, since they
are affinely dependent (see `finrank_vectorSpan_le_iff_not_affineIndependent`).  -/
Convex.radon_partition : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : ι → E},
  ¬AffineIndependent 𝕜 f → ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
-- Mathlib.Algebra.CharP.Basic
Prod.charZero_of_left : ∀ (R : Type u_1) (S : Type u_2) [inst : AddMonoidWithOne R] [inst_1 : AddMonoidWithOne S] [CharZero R], CharZero (R × S)
-- Mathlib.Order.PartialSups
partialSups_le_iff : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  {f : ι → α} {i : ι} {a : α}, (partialSups f) i ≤ a ↔ ∀ j ≤ i, f j ≤ a
-- Mathlib.Topology.Algebra.Group.Basic
exists_nhds_half_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s : Set G},
  s ∈ nhds 0 → ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v - w ∈ s
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- A heterogeneous universe version of the universal property of the colimit is
satisfied by `F.ColimitType` together with the maps `F.ιColimitType j`.  -/
CategoryTheory.Functor.descColimitType : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J (Type w₀)) → (c : F.CoconeTypes) → F.ColimitType → c.pt
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.instInhabitedSparseCasesOnInfo : Inhabited Lean.Meta.SparseCasesOnInfo
-- Mathlib.Control.LawfulFix
Part.toUnitMono_coe : ∀ {α : Type u_1} (f : Part α →o Part α) (x : Unit → Part α) (u : Unit), (Part.toUnitMono f) x u = f (x u)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.base_injective : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i}, (∀ (i : ι), Function.Injective ⇑(φ i)) → Function.Injective ⇑(Monoid.PushoutI.base φ)
-- Mathlib.Topology.Order.Basic
nhds_top_basis : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : OrderTop α] [OrderTopology α]
  [Nontrivial α], (nhds ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
-- Mathlib.Topology.Instances.Irrational
IsGδ.setOfPred_irrational : IsGδ {x | Irrational x}
-- Lean.Exception
/-- Throws an internal interrupt exception that skips standard `catch` clauses and should be caught only
at the top level of elaboration.
 -/
Lean.throwInterruptException : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadOptions m] → m α
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasFDerivAt.hasLineDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {x : E} {L : E →L[𝕜] F}, HasFDerivAt f L x → ∀ (v : E), HasLineDerivAt 𝕜 f (L v) x v
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInterFilter_inf : ∀ {α : Type u} (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂],
  CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.instIsStablyFiniteRingOfCommSemiring : ∀ {R : Type u_3} [inst : CommSemiring R], IsStablyFiniteRing R
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.isUnit_to_map_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R), IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.type : Lean.Meta.SimpAll.Entry → Lean.Expr
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Iso.retract_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y), e.retract.r = e.inv
-- Mathlib.RingTheory.Ideal.Maps
/-- `liftOfRightInverse f hf g hg` is the unique ring homomorphism `φ`

* such that `φ.comp f = g` (`RingHom.liftOfRightInverse_comp`),
* where `f : A →+* B` has a right inverse `f_inv` (`hf`),
* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.

See `RingHom.eq_liftOfRightInverse` for the uniqueness lemma.

```
   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ
```
 -/
RingHom.liftOfRightInverse : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Ring A] →
        [inst_1 : Ring B] →
          [inst_2 : Ring C] →
            (f : A →+* B) →
              (f_inv : B → A) → Function.RightInverse f_inv ⇑f → { g // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.chainable : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α}
  {f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α}
  {inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f} [self : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (aig : Std.Sat.AIG α) (input1 input2 : aig.BinaryInput) (h : aig.decls.size ≤ (f aig input1).aig.decls.size)
  (assign : α → Bool), ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions.mk.inj : ∀ {highlightMatchesProvider? : Option Lean.Lsp.HighlightMatchesOptions} {rpcWireFormat? : Option Lean.Lsp.RpcWireFormat}
  {highlightMatchesProvider?_1 : Option Lean.Lsp.HighlightMatchesOptions}
  {rpcWireFormat?_1 : Option Lean.Lsp.RpcWireFormat},
  { highlightMatchesProvider? := highlightMatchesProvider?, rpcWireFormat? := rpcWireFormat? } =
      { highlightMatchesProvider? := highlightMatchesProvider?_1, rpcWireFormat? := rpcWireFormat?_1 } →
    highlightMatchesProvider? = highlightMatchesProvider?_1 ∧ rpcWireFormat? = rpcWireFormat?_1
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
/-- The function defining the compatibility tensor for `∇` w.r.t. `g`:
prefer using `derivMetricTensor` instead  -/
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.derivMetricTensorAux : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            {M : Type u_3} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {F : Type u_4} →
                    [inst_5 : NormedAddCommGroup F] →
                      [inst_6 : NormedSpace ℝ F] →
                        {V : M → Type u_5} →
                          [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] →
                            [inst_8 : (x : M) → NormedAddCommGroup (V x)] →
                              [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] →
                                [inst_10 : FiberBundle F V] →
                                  CovariantDerivative I F V →
                                    ((x : M) → V x) → ((x : M) → V x) → (x : M) → TangentSpace I x →L[ℝ] ℝ
-- Mathlib.Analysis.Convex.Star
starConvex_pi : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {ι : Type u_4} {E : ι → Type u_5}
  [inst_2 : (i : ι) → AddCommMonoid (E i)] [inst_3 : (i : ι) → SMul 𝕜 (E i)] {x : (i : ι) → E i} {s : Set ι}
  {t : (i : ι) → Set (E i)}, (∀ ⦃i : ι⦄, i ∈ s → StarConvex 𝕜 (x i) (t i)) → StarConvex 𝕜 x (s.pi t)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.positive.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)}
  {pf pf_1 : Q(0 < «$e»)},
  Mathlib.Meta.Positivity.Strictness.positive pf = Mathlib.Meta.Positivity.Strictness.positive pf_1 → pf = pf_1
-- Mathlib.RingTheory.Polynomial.Chebyshev
_private.Mathlib.RingTheory.Polynomial.Chebyshev.0.Polynomial.Chebyshev.T.match_1.eq_4 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : ℕ) → motive (Int.ofNat n.succ.succ)) (h_4 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | Int.ofNat n.succ.succ => h_3 n
    | Int.negSucc n => h_4 n) =
    h_4 n
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {M : CategoryTheory.Functor C MonCat}
  {x y : CategoryTheory.SubmonoidFunctor M}, x.obj = y.obj → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mk : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    (fst : CategoryTheory.Functor X A) →
                      (snd : CategoryTheory.Functor X C) →
                        (fst.comp F ≅ snd.comp G) → CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X
-- Mathlib.Order.RelIso.Basic
/-- A relation isomorphism is also a relation isomorphism between dual relations.  -/
RelIso.swap : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → Function.swap r ≃r Function.swap s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] (I : ModelWithCorners 𝕜 E H)
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] (I' : ModelWithCorners 𝕜 E' H') [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] (x : M) (f : M → M'),
  writtenInExtChartAt I I' x f = ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.Std.Slice.Internal.iter.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] (s : Std.Slice γ),
  Std.Slice.Internal.iter s = Std.ToIterator.iter s
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.isLocallySurjective_iff_epi' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology 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]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A]
  [CategoryTheory.HasSheafify J A] [J.HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Balanced (CategoryTheory.Sheaf J A)] {F G : CategoryTheory.Sheaf J A} (φ : F ⟶ G),
  CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ
-- Init.Data.Nat.Basic
Nat.two_mul : ∀ (n : ℕ), 2 * n = n + n
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : C(α, β)}
  {U : TopologicalSpace.Opens β} {x : α}, x ∈ (TopologicalSpace.Opens.comap f) U ↔ f x ∈ U
-- Mathlib.Data.Finset.Defs
Finset.setOfPred_mem : ∀ {α : Type u_4} {s : Finset α}, {a | a ∈ s} = ↑s
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.deriv_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜}, f₁ =ᶠ[nhds x] f → deriv f₁ x = deriv f x
-- Init.Control.ExceptCps
ExceptCpsT.runCatch_bind_throw : ∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Monad m] (e : β) (f : α → ExceptCpsT β m β),
  (throw e >>= f).runCatch = pure e
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.categoryAsType_id : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  (x : CategoryTheory.FinCategory.AsType α),
  CategoryTheory.CategoryStruct.id x = (Fintype.equivFin (x ⟶ x)) (CategoryTheory.CategoryStruct.id x)
-- Init.RCases
/-- A medium precedence `rcases` pattern is a list of `rcasesPat` separated by `|`  -/
Lean.Parser.Tactic.rcasesPatMed : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.liftOrderHom_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : { a // a ≠ 0 } → α)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ ≤ FiniteArchimedeanClass.mk ↑b ⋯ → f a ≤ f b) {a : M}
  (ha : a ≠ 0), (FiniteArchimedeanClass.liftOrderHom f h) (FiniteArchimedeanClass.mk a ha) = f ⟨a, ha⟩
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    ((x : ℕ) → motive x 0) →
      ((m : ℕ) → motive 0 m.succ) → ((k m : ℕ) → (m = 0 → False) → motive k.succ m) → motive x x_1