mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.Compact
Function.Surjective.compactSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ [CompactSpace X], Function.Surjective f → CompactSpace Y
-- Lean.Meta.Tactic.FVarSubst
/-- Some tactics substitute hypotheses with expressions.
We track these substitutions using `FVarSubst`.
It is just a mapping from the original FVarId (internal) name
to an expression. The free variables occurring in the expression must
be defined in the new goal.  -/
Lean.Meta.FVarSubst : Type
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.PadicInt.appr.match_1.eq_1 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (motive : ℤ_[p] → ℕ → Sort u_1) (_x : ℤ_[p])
  (h_1 : (_x : ℤ_[p]) → motive _x 0) (h_2 : (x : ℤ_[p]) → (n : ℕ) → motive x n.succ),
  (match _x, 0 with
    | _x, 0 => h_1 _x
    | x, n.succ => h_2 x n) =
    h_1 _x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_add_sin : ∀ (x y : ℂ), Complex.sin x + Complex.sin y = 2 * Complex.sin ((x + y) / 2) * Complex.cos ((x - y) / 2)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_ext_iff : ∀ {R S : CommRingCat} {f g : R ⟶ S}, f = g ↔ CommRingCat.Hom.hom f = CommRingCat.Hom.hom g
-- Mathlib.GroupTheory.Torsion
AddEquiv.addSubmonoidCongr.congr_simp : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S = T),
  AddEquiv.addSubmonoidCongr h = AddEquiv.addSubmonoidCongr h
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
and `R` a sheaf of rings, this is the adjunction
`sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α`.  -/
PresheafOfModules.sheafificationAdjunction : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                    PresheafOfModules.sheafification α ⊣
                      (SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- An absolute value on a semiring `R` without zero divisors is *nontrivial* if it takes
a value `≠ 1` on a nonzero element.

This has the advantage over `v ≠ .trivial` that it does not require decidability
of `· = 0` in `R`.  -/
AbsoluteValue.IsNontrivial : {R : Type u_5} →
  [inst : Semiring R] → {S : Type u_6} → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → Prop
-- Mathlib.Algebra.Order.Module.Defs
antitone_smul_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β],
  a ≤ 0 → Antitone fun x => a • x
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.algebraMap_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Ring S] [Nontrivial S] [inst_4 : Algebra R S]
  {ι : Type u_5} (b : Module.Basis ι R S), Function.Injective ⇑(algebraMap R S)
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
DiscreteUniformity.eq_principal_setRelId : ∀ (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X], uniformity X = Filter.principal SetRel.id
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.cone_π_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite)
  (i : CategoryTheory.StructuredArrow S FintypeCat.toProfinite), (Profinite.Extend.cone G S).π.app i = G.map i.hom
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : Preorder α} {x_1 : Preorder β} {x_2 : MulOneClass α} {x_3 : MulOneClass β}
  (f : α →*o β), f.toMonoidHom = ↑f
-- Std.Net.Addr
Std.Net.IPAddr.v4 : Std.Net.IPv4Addr → Std.Net.IPAddr
-- Init.Data.Array.Lemmas
Array.filter_filter : ∀ {α : Type u_1} {p q : α → Bool} {xs : Array α},
  Array.filter p (Array.filter q xs) = Array.filter (fun a => p a && q a) xs
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, Std.ExtDHashMap.Const.getD (m.erase k) k fallback = fallback
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e.,
`p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such
that `∀ i ∈ s, p (g i)`. Then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.  -/
Finset.le_prod_of_submultiplicative_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : Preorder N]
  [IsOrderedMonoid N] (f : M → N) (p : M → Prop),
  f 1 ≤ 1 →
    (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
      (∀ (x y : M), p x → p y → p (x * y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ i ∈ s, p (g i)) → f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isQuotientMap_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsQuotientMap ⇑DomMulAct.mk.symm
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.skipWhile.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((nextCurr : s.Pos) → motive (some nextCurr)) → (Unit → motive none) → motive x
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- A homomorphism of the graph of a submatrix of an adjacency matrix to the graph of the
adjacency matrix itself  -/
Matrix.IsAdjMatrix.toGraphSubmatrixHom : {α : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      (A : Matrix V V α) →
        [inst : MulZeroOneClass α] →
          [inst_1 : Nontrivial α] → (h : A.IsAdjMatrix) → (f : W → V) → ⋯.toGraph →g h.toGraph
-- Mathlib.RingTheory.PolynomialAlgebra
/-- (Implementation detail).
The algebra homomorphism `A ⊗[R] R[X] →ₐ[R] A[X]`.
 -/
PolyEquivTensor.toFunAlgHom : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A (Polynomial R) →ₐ[R] Polynomial A
-- Init.Tactics
/-- `mhave` is like `have`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mhaveMacro : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α} {h' : a ∈ m}, m.getKey a h' = m.getKey! a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.toProd : {𝕜 : Type u} →
  {A : Type v} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] → DoubleCentralizer 𝕜 A → (A →L[𝕜] A) × (A →L[𝕜] A)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_descCochain_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + -1 = p₂) (h₂₃ : p₂ + n = p₃) {Z : C} (h_1 : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descCochain φ α β h).v p₂ p₃ h₂₃) h_1) =
    CategoryTheory.CategoryStruct.comp (α.v p₁ p₃ ⋯) h_1
-- Mathlib.Data.Finset.Max
Finset.min_eq_bot : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset α}, s.min = ⊥ ↔ ⊥ ∈ s
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsWF.min_mul : ∀ {α : Type u_1} {s t : Set α} [inst : CommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelMonoid α]
  (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty), ⋯.min ⋯ = hs.min hsn * ht.min htn
-- Init.Data.Option.Attach
Option.attach_none : ∀ {α : Type u_1}, none.attach = none
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  {f : α → β → Option γ},
  m.WF →
    (Std.HashMap.Raw.filterMap f m).toList.Perm
      (List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) m.toList)
-- Mathlib.Topology.Order.LeftRightNhds
eventually_abs_sub_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] (a : α) {ε : α}, 0 < ε → ∀ᶠ (x : α) in nhds a, |x - a| < ε
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `ι`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.φH (CategoryTheory.CategoryStruct.comp h₂.ι h) =
    CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.CategoryStruct.comp self.φQ h)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittSub_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittSub p 0 = MvPolynomial.X (0, 0) - MvPolynomial.X (1, 0)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.MatchResult.covered.inj : ∀ {f : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt} {exhaustive : Bool}
  {f_1 : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt} {exhaustive_1 : Bool},
  Lean.Elab.Term.Quotation.MatchResult.covered f exhaustive =
      Lean.Elab.Term.Quotation.MatchResult.covered f_1 exhaustive_1 →
    f = f_1 ∧ exhaustive = exhaustive_1
-- Mathlib.GroupTheory.OrderOfElement
/-- A nonempty idempotent subset of a finite group is a subgroup  -/
subgroupOfIdempotent : {G : Type u_6} → [inst : Group G] → [Finite G] → (S : Set G) → S.Nonempty → S * S = S → Subgroup G
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.algEquiv_symm_apply_toCLM : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] (S : Type u_5) [inst_4 : CommSemiring S] [inst_5 : Module S E] [inst_6 : SMulCommClass 𝕜₁ S E]
  [inst_7 : SMul S 𝕜₁] [inst_8 : IsScalarTower S 𝕜₁ E] [inst_9 : ContinuousConstSMul S E]
  [inst_10 : IsTopologicalAddGroup E] (toCLM : E →L[𝕜₁] E),
  ((ContinuousLinearMapWOT.algEquiv S).symm toCLM).toCLM = toCLM
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.comp_hom_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y Z : CategoryTheory.InducedCategory D F} (f : X.Hom Y) (g : Y.Hom Z) {Z_1 : D} (h : F Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.Order.Ideal
Order.Ideal.inter_nonempty : ∀ {P : Type u_1} [inst : LE P] [IsCodirectedOrder P] (I J : Order.Ideal P), (↑I ∩ ↑J).Nonempty
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β},
  t.modify k f ≠ ∅ →
    ∀ {fallback : α},
      (t.modify k f).maxKeyD fallback = if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constVAdd.eq_1 : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : IsIsometricVAdd G X] (c : G),
  IsometryEquiv.constVAdd c = { toEquiv := AddAction.toPerm c, isometry_toFun := ⋯ }
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.instBEqFunInfoEnvCacheKey.beq : Lean.Meta.FunInfoEnvCacheKey✝ → Lean.Meta.FunInfoEnvCacheKey✝ → Bool
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If `P` respects isos, then `stalkwise P` is local at the target.  -/
AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    AlgebraicGeometry.IsZariskiLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited Lean.Lsp.CallHierarchyIncomingCall
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.comap_subtype_self : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.comap p.subtype p = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  {f : R →+* S}, Function.Injective ⇑f → ∀ (P : Fin 3 → R), (W'.map f).Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P
-- Init.Data.Dyadic.Basic
Dyadic.toRat.eq_2 : ∀ (n : ℤ) (k : ℕ) (hn : n % 2 = 1),
  (Dyadic.ofOdd n (Int.ofNat k) hn).toRat = { num := n, den := 2 ^ k, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.monic_multisetProd_X_sub_C : ∀ {R : Type u} [inst : CommRing R] (s : Multiset R),
  (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.Monic
-- Mathlib.Data.Sum.Order
Sum.LiftRel.refl : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s] (x : α ⊕ β),
  Sum.LiftRel r s x x
-- Mathlib.Logic.Embedding.Set
/-- The injection map is an embedding between subsets.  -/
Set.embeddingOfSubset : {α : Type u_1} → (s t : Set α) → s ⊆ t → ↑s ↪ ↑t
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.mk.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v, u₂} D} {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {hom hom_1 : F X ⟶ F Y}, { hom := hom } = { hom := hom_1 } → hom = hom_1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
/-- Assuming we have a sequence of subsets `X n : Set (Cochain K L d)` for all `n : ℕ`,
a sequence of maps `φ n : X n → X (n + 1)` for `n : ℕ`, and an element `x₀ : X 0`,
this is the dependent sequence in `∀ (n : ℕ), X n` obtained by evaluation iterations of `φ`
on `x₀`.  -/
CochainComplex.HomComplex.Cochain.InductionUp.sequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {d : ℤ} →
          {X : ℕ → Set (CochainComplex.HomComplex.Cochain K L d)} →
            ((n : ℕ) → ↑(X n) → ↑(X (n + 1))) → ↑(X 0) → (n : ℕ) → ↑(X n)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).isColimit₂ = c.isColimit₂
-- Mathlib.RingTheory.Unramified.Locus
Algebra.exists_formallyUnramified_of_isUnramifiedAt : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.EssFiniteType R A] (p : Ideal A) [inst_4 : p.IsPrime] [Algebra.IsUnramifiedAt R p],
  ∃ f ∉ p, Algebra.FormallyUnramified R (Localization.Away f)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- The diagonal path `d` of a homotopy `H` on a path `p`  -/
ContinuousMap.Homotopy.diagonalPath : {X Y : TopCat} →
  {f g : C(↑X, ↑Y)} →
    (H : f.Homotopy g) →
      {x₀ x₁ : ↑X} →
        (FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁) →
          (FundamentalGroupoid.fromTop (H (0, x₀)) ⟶ FundamentalGroupoid.fromTop (H (1, x₁)))
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.abs_repr_lt_of_norm_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ),
  ‖x‖ < ZLattice.normBound b * ↑n → ∀ (i : ι), |(b.repr x) i| < ↑n
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_map : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (b : Module.Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M'), (b.map f).det v = b.det (⇑f.symm ∘ v)
-- Init.Data.UInt.BasicAux
/-- Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed
via the `DecidableLE USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : USize) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : USize) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : USize) ≤ 7 by decide`
 -/
USize.decLe : (a b : USize) → Decidable (a ≤ b)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instInf : Min ℚ
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.of_subsingleton : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G} [Subsingleton G], UniqueAdd A B a0 b0
-- Mathlib.Order.RelIso.Basic
/-- An embedding `f : α ↪ β` induces a relation embedding from an `α`-relation `r` to
`Relation.Map r f f`.  -/
RelEmbedding.toMap : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (f : α ↪ β) → r ↪r Relation.Map r ⇑f ⇑f
-- Mathlib.Analysis.Convex.Function
/-- Left translation preserves concavity.  -/
ConcaveOn.translate_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f : E → β}, ConcaveOn 𝕜 s f → ∀ (c : E), ConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.coroot_mem_or_neg_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (self : P.Base)
  (i : ι),
  P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑self.support) ∨
    -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑self.support)
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.merge.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (xs ys : List α) →
      ((ys : List α) → motive [] ys) →
        ((xs : List α) → (xs = [] → False) → motive xs []) →
          ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive xs ys
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_sub : ∀ (x y : ℂ), Complex.sin (x - y) = Complex.sin x * Complex.cos y - Complex.cos x * Complex.sin y
-- Init.Data.String.Lemmas.Splits
String.Pos.sliceFrom_cast : ∀ {s t : String} {hst : s = t} (p q : s.Pos) {h : p.cast hst ≤ q.cast hst},
  (p.cast hst).sliceFrom (q.cast hst) h = (p.sliceFrom q ⋯).cast ⋯
-- Init.Data.SInt.Bitwise
Int32.xor_right_inj : ∀ {a b : Int32} (c : Int32), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.inv_smul_integral_comp_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ),
  c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_map' : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  (q : PolynomialModule R M) (r : R),
  (PolynomialModule.eval r) ((PolynomialModule.map R f) q) = f ((PolynomialModule.eval r) q)
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.down_sSup : ∀ {α : Type u_1} [inst : SupSet α] (s : Set (ULift.{v, u_1} α)), (sSup s).down = sSup (ULift.up ⁻¹' s)
-- Init.Data.Array.Lemmas
Array.getElem_eq_iff : ∀ {α : Type u_1} {x : α} {xs : Array α} {i : ℕ} {h : i < xs.size}, xs[i] = x ↔ xs[i]? = some x
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Std.Time.Date.Unit.Basic
/-- Convert `Day.Offset` into `Week.Offset`.
 -/
Std.Time.Day.Offset.toWeeks : Std.Time.Day.Offset → Std.Time.Week.Offset
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.AltParamInfo.mk : ℕ → ℕ → Bool → Lean.Meta.Match.AltParamInfo
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The functor of adjoining a neutral element `zero` to a semigroup  -/
AddMonCat.adjoinZero : CategoryTheory.Functor AddSemigrp AddMonCat
-- Mathlib.Data.List.TakeWhile
_private.Mathlib.Data.List.TakeWhile.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go : (aig : Std.Sat.AIG ℕ) →
  (upper : ℕ) →
    (h : upper < aig.decls.size) →
      (state : Std.Sat.AIG.toCNF.State✝ aig) → { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out upper h }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? pref.length Std.PRange.UpwardEnumerable.least).get ⋯
-- Lean.Attributes
Lean.AttributeApplicationTime : Type
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If all but one point of a family are affinely independent, and that point does not lie in
the affine span of that family, the family is affinely independent.  -/
AffineIndependent.affineIndependent_of_notMem_span : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P} {i : ι},
  (AffineIndependent k fun x => p ↑x) → p i ∉ affineSpan k (p '' {x | x ≠ i}) → AffineIndependent k p
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epi becomes a normal mono in the opposite category.  -/
CategoryTheory.normalMonoOfNormalEpiUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.NormalEpi f.unop → CategoryTheory.NormalMono f
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.endRingEquiv_apply : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (M : TopModuleCat R) (f : M.Hom M),
  M.endRingEquiv f = f.hom