mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.WithTop
WithBot.tendsto_unbot : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (a : ↑{a | a ≠ ⊥}),
  Filter.Tendsto (fun x => (↑x).unbot ⋯) (nhds a) (nhds ((↑a).unbot ⋯))
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
/-- The map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous cohomology induced by a continuous group
homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
`f : res φ X ⟶ Y`.  -/
ContinuousCohomology.map : {k : Type u} →
  {G H : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              [inst_5 : Group H] →
                [inst_6 : TopologicalSpace H] →
                  [inst_7 : IsTopologicalGroup H] →
                    {X : TopRep k G} →
                      {Y : TopRep k H} →
                        (φ : H →ₜ* G) →
                          (TopRep.res (↑φ) X ⟶ Y) → (n : ℕ) → continuousCohomology n X ⟶ continuousCohomology n Y
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_pos_iff_infinitePos_inv : ∀ {x : ℝ*}, x⁻¹.InfinitePos ↔ x.Infinitesimal ∧ 0 < x
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.comp_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N K : Action V G}
  (p : M.Hom N) (q : N.Hom K), (p.comp q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_filter_key : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool} {k : α},
  (Std.ExtDHashMap.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnAddMonoidHom.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G],
  ContMDiffMap.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.mk : {Γ : Type u} →
  {Γ' : Type v} →
    [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → (f : Γ → Γ') → f default = default → Turing.PointedMap Γ Γ'
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_ite_index : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (p : Prop) [inst_1 : Decidable p] (s t : Finset ι) (f : ι → M),
  ∑ x ∈ if p then s else t, f x = if p then ∑ x ∈ s, f x else ∑ x ∈ t, f x
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_mk : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDomain A] [inst_5 : IsDomain B]
  (I : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ),
  (ClassGroup.extendedHom A B) ((ClassGroup.mk (FractionRing A)) I) =
    (ClassGroup.mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)
-- Aesop.Util.Basic
Aesop.runTacticMCapturingPostState : Lean.Elab.Tactic.TacticM Unit →
  Lean.Meta.SavedState → List Lean.MVarId → Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Helper function for throwing exceptions with respect to the main goal.  -/
Mathlib.Tactic.BicategoryCoherence.exception' : Lean.MessageData → Lean.Elab.Tactic.TacticM Unit
-- Lean.Data.KVMap
Lean.DataValue.ofString : String → Lean.DataValue
-- Mathlib.Algebra.Category.ModuleCat.Ext.Finite
ModuleCat.finite_ext : ∀ (R : Type u) [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (N M : ModuleCat R)
  [Module.Finite R ↑N] [Module.Finite R ↑M] (i : ℕ), Module.Finite R (CategoryTheory.Abelian.Ext N M i)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Ioc_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.Ioc (i.addNat m) (j.addNat m) = Set.Ioc i j
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.map'_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ)
  (hi : autoParam (i ≤ n) CategoryTheory.ComposableArrows.map'_self._auto_1),
  F.map' i i ⋯ hi = CategoryTheory.CategoryStruct.id (F.obj ⟨i, ⋯⟩)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.is_extension : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} (self : Module.Baer.ExtensionOf i f) (m : M), f m = ↑self.toLinearPMap ⟨i m, ⋯⟩
-- Mathlib.Analysis.Complex.Basic
Complex.isUniformEmbedding_ofReal : IsUniformEmbedding Complex.ofReal
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.of_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  (b : Module.Basis ι R M), Module.Free R M
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.submodule_eq_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  (p : α → Submodule R M), Finsupp.submodule p = ⨆ i, Submodule.map (Finsupp.lsingle i) (p i)
-- Mathlib.Analysis.Convex.FunctionTopology
ConvexOn.eq_1 : ∀ (𝕜 : 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 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] (s : Set E) (f : E → β),
  ConvexOn 𝕜 s f =
    (Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y)
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α], ¬Order.IsSuccLimit a ↔ IsMin a ∨ ¬Order.IsSuccPrelimit a
-- Mathlib.Data.List.Flatten
List.Sublist.flatten : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, l₁.Sublist l₂ → l₁.flatten.Sublist l₂.flatten
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.CycleType.count_def : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} (n : ℕ),
  Multiset.count n σ.cycleType = Fintype.card { c // (↑c).support.card = n }
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Mathlib.Analysis.Normed.Order.UpperLower
IsClosed.lowerClosure_pi : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)}, IsClosed s → BddAbove s → IsClosed ↑(lowerClosure s)
-- Mathlib.Control.Bifunctor
Bifunctor.flip : {F : Type u₀ → Type u₁ → Type u₂} → [Bifunctor F] → Bifunctor (flip F)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainGoal.fromJson : Lean.Json → Except String Lean.Lsp.PlainGoal
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} {f g : sq₁ ⟶ sq₂},
  f.τ₁ = g.τ₁ → f.τ₂ = g.τ₂ → f.τ₃ = g.τ₃ → f.τ₄ = g.τ₄ → f = g
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.instAddMonoidId.eq_1 : ∀ {M : Type u_2} {X : Type u_4} [inst : VAdd M X],
  AddActionHom.End.instAddMonoidId =
    { add := fun f g => f.comp g, add_assoc := ⋯, zero := AddActionHom.id M, zero_add := ⋯, add_zero := ⋯,
      nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.getElem_ofBoolListBE : ∀ {i : ℕ} {bs : List Bool} (h : i < bs.length), (BitVec.ofBoolListBE bs)[i] = bs[bs.length - 1 - i]
-- Mathlib.Data.String.Basic
String.ltb.induct_unfolding : ∀ (motive : String.Legacy.Iterator → String.Legacy.Iterator → Bool → Prop),
  (∀ (s₁ s₂ : String.Legacy.Iterator),
      s₂.hasNext = true →
        s₁.hasNext = true →
          s₁.curr = s₂.curr →
            motive s₁.next s₂.next (String.ltb s₁.next s₂.next) → motive s₁ s₂ (String.ltb s₁.next s₂.next)) →
    (∀ (s₁ s₂ : String.Legacy.Iterator),
        s₂.hasNext = true → s₁.hasNext = true → ¬s₁.curr = s₂.curr → motive s₁ s₂ (decide (s₁.curr < s₂.curr))) →
      (∀ (s₁ s₂ : String.Legacy.Iterator), s₂.hasNext = true → ¬s₁.hasNext = true → motive s₁ s₂ true) →
        (∀ (s₁ s₂ : String.Legacy.Iterator), ¬s₂.hasNext = true → motive s₁ s₂ false) →
          ∀ (s₁ s₂ : String.Legacy.Iterator), motive s₁ s₂ (String.ltb s₁ s₂)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_not : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, φ.not.Realize v xs ↔ ¬φ.Realize v xs
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h)
  [inst_1 : CategoryTheory.IsIso η],
  CategoryTheory.inv (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.inv η)
-- Mathlib.LinearAlgebra.Pi
LinearMap.iSup_range_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι], ⨆ i, (LinearMap.single R φ i).range = ⊤
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Creates the packed signed infinity representation for the given specification.  -/
Float.Model.UnpackedFloat.packedInfinity : (spec : Float.Model.Format) → Float.Model.UnpackedFloat.Sign → BitVec spec.numBits
-- Init.Data.Iterators.Basic
/-- An iterator that sequentially emits values of type `β`. It may be finite
or infinite.

See the root module `Std.Data.Iterators` for a more comprehensive overview over the iterator
framework.

See `Std.Data.Iterators.Producers` for ways to iterate over common data structures.
By convention, the monadic iterator associated with an object can be obtained via dot notation.
For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.

See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
convert an iterator `it` into a list and `it.ensureTermination.toList` guarantees that this
operation will terminate, given a proof that the iterator is finite.
It is also always possible to manually iterate using
`it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.

See `IterM` for iterators that operate in a monad.

Internally, `Iter β` wraps an element of type `α` containing state information.
The type `α` determines the implementation of the iterator using a typeclass mechanism.
The concrete typeclass implementing the iterator is `Iterator α m β`.

When using combinators, `α` can become very complicated. It is an implicit parameter
of `α` so that the pretty printer will not print this large type by default. If a declaration
returns an iterator, the following will not work:

```lean
def x : Iter Nat := [1, 2, 3].iter
```

Instead the declaration type needs to be completely omitted:

```lean
def x := [1, 2, 3].iter

-- if you want to ensure that `x` is an iterator emitting `Nat`
def x := ([1, 2, 3].iter : Iter Nat)
```
 -/
Std.Iter : {α : Type w} → Type w → Type w
-- Init.GrindInstances.ToInt
Lean.Grind.instLTInt16SintOfNatNat : Lean.Grind.ToInt.LT Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.fromQuotient_toQuotient : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) (x : relations.G →₀ A),
  solution.fromQuotient (relations.toQuotient x) = solution.π x
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_image_iff_exists_fun : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {x : M} {s : Set α}, x ∈ Submodule.span R (v '' s) ↔ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractAndExtendAux_zero : ∀ {w k len : ℕ} {x : BitVec w} {acc : BitVec (k * len)} (heq : w = k),
  BitVec.extractAndExtendAux k len x acc ⋯ = BitVec.cast ⋯ acc
-- Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
SSet.instIsStableUnderFilteredColimitsMonomorphisms : CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{u, u, u, u + 1}
  (CategoryTheory.MorphismProperty.monomorphisms SSet)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.instSFiniteProdCompProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β}, MeasureTheory.SFinite (μ.compProd κ)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_inv_of_apply_inv_eq_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveInv α] {s : Set α} [inst_1 : InvolutiveInv β] {f g : α → β},
  (∀ x ∈ s, f x⁻¹ = (g x)⁻¹) → f '' s⁻¹ = (g '' s)⁻¹
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii.sizeOf_spec : sizeOf Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii = 1
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The index on which `a` and `b` lives. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.i : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} → AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f → I
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_bot : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ↑⊥ = 0
-- Mathlib.Topology.Inseparable
/-- A continuous function is monotone with respect to the specialization preorders on the domain and
the codomain.  -/
Continuous.specialization_monotone : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Monotone f
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom : ∀ {R : Type u} [inst : CommRing R] {X Y : HopfAlgCat R} (i : X ≅ Y), ↑i.toHopfAlgEquiv = i.hom.toBialgHom'
-- Mathlib.Order.SuccPred.Archimedean
LE.le.exists_pred_iterate : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {a b : α},
  b ≤ a → ∃ n, Order.pred^[n] a = b
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
/-- The precomposition `Ext Y Z a →ₗ[R] Ext X Z b` with `α : Ext X Y n` when `n + a = b`.  -/
CategoryTheory.Abelian.Ext.precompOfLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext X Y n →
              (R : Type t) →
                [inst_3 : CommRing R] →
                  [inst_4 : CategoryTheory.Linear R C] →
                    (Z : C) →
                      {a b : ℕ} → n + a = b → CategoryTheory.Abelian.Ext Y Z a →ₗ[R] CategoryTheory.Abelian.Ext X Z b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.IsComm.comm : ∀ {R : Type u_1} {inst : CommRing R} {F : FormalGroup R} [self : F.IsComm],
  F.toPowerSeries = MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 0] F.toPowerSeries
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ φ_1 : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂),
  φ = φ_1 →
    ∀ ⦃Y' : C⦄ (g g_1 : Y' ⟶ Y) (e_g : g = g_1) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂)
      (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂ =
        CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ_1 g_1 gf₁ gf₂ ⋯ ⋯
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.coe_zero : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : Zero α], ↑0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.ind : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {β : G.ComponentCompl K → Prop},
  (∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)) → ∀ (C : G.ComponentCompl K), β C
-- Mathlib.RingTheory.LocalProperties.Projective
Module.projective_of_localization_maximal : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∀ (I : Ideal R) (x : I.IsMaximal), Module.Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)) →
    ∀ [Module.FinitePresentation R M], Module.Projective R M
-- Mathlib.Order.SymmDiff
bihimp_eq_top : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, bihimp a b = ⊤ ↔ a = b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constInsertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  t₁.Equiv t₂ →
    ∀ (l : List α), (Std.DTreeMap.Const.insertManyIfNewUnit t₁ l).Equiv (Std.DTreeMap.Const.insertManyIfNewUnit t₂ l)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- `n + 2` points have a `vectorSpan` with dimension at most `n` if
and only if they are not affinely independent.  -/
finrank_vectorSpan_le_iff_not_affineIndependent : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
  Fintype.card ι = n + 2 → (Module.finrank k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬AffineIndependent k p)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, (m.insertManyIfNewUnit l).contains k = (m.contains k || l.contains k)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.coe_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] (s t : Finset β), ↑(s -ᵥ t) = ↑s -ᵥ ↑t
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), a ∉ t)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instFaithfulSMul : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [inst_3 : SMul R T] [FaithfulSMul R T], FaithfulSMul (WithAbs v) T
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ_desc_apply : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : CategoryTheory.CategoryStruct.comp f g = 0} (x : Y.carrier),
  (CategoryTheory.ConcreteCategory.hom (SemiNormedGrp.explicitCokernelDesc cond))
      ((CategoryTheory.ConcreteCategory.hom (SemiNormedGrp.explicitCokernelπ f)) x) =
    (CategoryTheory.ConcreteCategory.hom g) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.arg_eq_zero : ∀ {z : Circle}, (↑z).arg = 0 ↔ z = 1
-- Init.Data.Repr
Repr.mk : {α : Type u} → (α → ℕ → Std.Format) → Repr α
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.eq_of_eq_union_iUnion : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C]
  (I J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)),
  ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j → I = J
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.sum_pow_filter_eq_faulhaber : ∀ {k : ℕ} (p : ℕ),
  0 < k →
    ∑ v ∈ Finset.Ico 1 p, ↑v ^ (2 * k) =
      ∑ i ∈ Finset.range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
        ↑p * bernoulli (2 * k)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C}
  (Y : CategoryTheory.Over X), ∀ S ∈ J Y.left, (CategoryTheory.Sieve.overEquiv Y).symm S ∈ (J.over X) Y
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hom_ofHom : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), SemiRingCat.Hom.hom (SemiRingCat.ofHom f) = f
-- Init.Core
Subtype.mk.injEq : ∀ {α : Sort u} {p : α → Prop} (val : α) (property : p val) (val_1 : α) (property_1 : p val_1),
  (⟨val, property⟩ = ⟨val_1, property_1⟩) = (val = val_1)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.Internal.List.containsKey a l' = false → Std.Internal.List.getEntry! a (l ++ l') = Std.Internal.List.getEntry! a l
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α},
  s.Nonempty → t.Nonempty → (s.diffs t).Nonempty
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instOrderBotOfOrderTop.eq_1 : ∀ (α : Type u) [inst : LE α] [h : OrderTop α],
  OrderDual.instOrderBotOfOrderTop α = { toBot := OrderDual.instBotOfTop α, bot_le := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_smul_order_add_order : ∀ {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid V] {Γ : Type u_6} [inst_1 : AddCommMonoid Γ]
  [inst_2 : LinearOrder Γ] [inst_3 : IsOrderedCancelAddMonoid Γ] [inst_4 : Zero R] [inst_5 : SMulWithZero R V]
  (x : HahnSeries Γ R) (y : HahnModule Γ R V),
  ((HahnModule.of R).symm (x • y)).coeff (x.order + ((HahnModule.of R).symm y).order) =
    x.leadingCoeff • ((HahnModule.of R).symm y).leadingCoeff
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.strongRec_eq`. -/
Nat.strongRec'_spec : ∀ {motive : ℕ → Sort u_1} (ind : (n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) (t : ℕ),
  Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasSum_jacobiTheta₂'_term : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → HasSum (fun n => jacobiTheta₂'_term n z τ) (jacobiTheta₂' z τ)
-- Aesop.Search.SearchM
Aesop.wasMaxRuleApplicationDepthReached : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Bool