mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_le : ∀ {c : Cardinal.{u_1}} {o : Ordinal.{u_1}}, c.ord ≤ o ↔ c ≤ o.card
-- Mathlib.GroupTheory.Coxeter.Basic
PresentedGroup.toGroup.congr_simp : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f f_1 : α → G} (e_f : f = f_1) {rels : Set (FreeGroup α)}
  (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1), PresentedGroup.toGroup h = PresentedGroup.toGroup ⋯
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_inter_Ico_consecutive : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b c : α),
  Finset.Ico a b ∩ Finset.Ico b c = ∅
-- Mathlib.Analysis.Calculus.Implicit
/-- `HasStrictFDerivAt.implicitFunctionOfComplemented` sends `(z, y)` to a point in `f ⁻¹' z`.  -/
HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  ∀ᶠ (p : F × ↥(↑f').ker) in nhds (f a, 0),
    f (HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker p.1 p.2) = p.1
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toAdditive_symm_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : MulOneClass H] (f : Additive G ≃+ Additive H) (a : G),
  (MulEquiv.toAdditive.symm f) a = (MonoidHom.toAdditive.symm f.toAddMonoidHom) a
-- Lean.Elab.App
/-- If the result type of an application is the `outParam` of some local instance, then special support may be needed
because type class resolution interacts poorly with coercions in this kind of situation.
This flag enables the special support.

The idea is quite simple, if the result type is the `outParam` of some local instance, we simply
execute `synthesizeSyntheticMVarsUsingDefault`. We added this feature to make sure examples as follows
are correctly elaborated.
```lean
class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
  getElem (xs : Cont) (i : Idx) : Elem

export GetElem (getElem)

instance : GetElem (Array α) Nat α where
  getElem xs i := xs.get ⟨i, sorry⟩

opaque f : Option Bool → Bool
opaque g : Bool → Bool

def bad (xs : Array Bool) : Bool :=
  let x := getElem xs 0
  f x && g x
```
Without the special support, Lean fails at `g x` saying `x` has type `Option Bool` but is expected to have type `Bool`.
From the user's point of view this is a bug, since `let x := getElem xs 0` clearly constrains `x` to be `Bool`, but
we only obtain this information after we apply the `OfNat` default instance for `0`.

Before converging to this solution, we have tried to create a "coercion placeholder" when `resultIsOutParamSupport = true`,
but it did not work well in practice. For example, it failed in the example above.
 -/
Lean.Elab.Term.ElabAppArgs.Context.resultIsOutParamSupport : Lean.Elab.Term.ElabAppArgs.Context → Bool
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj_map_updateFinset : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {n : ℕ} (x : (i : ↥(Finset.Iic n)) → X ↑i),
  MeasureTheory.Measure.map (fun x_1 => Function.updateFinset x_1 (Finset.Iic n) x)
      ((ProbabilityTheory.Kernel.traj κ n) x) =
    (ProbabilityTheory.Kernel.traj κ n) x
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_injective_of_right : ∀ {α : Sort u_1} [inst : DecidableEq α] (a : α), Function.Injective fun x => Equiv.swap x a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α}
  [inst_1 : Inhabited (β a)], ∅.get! a = default
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_omega0 : Ordinal.omega0.card = Cardinal.aleph0
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- Localization of composition is the composition of localization  -/
IsLocalizedModule.map_comp' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [inst_1 : AddCommMonoid M₀]
  [inst_2 : AddCommMonoid M₀'] [inst_3 : Module R M₀] [inst_4 : Module R M₀'] (f₀ : M₀ →ₗ[R] M₀')
  [inst_5 : IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_11} [inst_6 : AddCommMonoid M₁]
  [inst_7 : AddCommMonoid M₁'] [inst_8 : Module R M₁] [inst_9 : Module R M₁'] (f₁ : M₁ →ₗ[R] M₁')
  [inst_10 : IsLocalizedModule S f₁] {M₂ : Type u_8} {M₂' : Type u_10} [inst_11 : AddCommMonoid M₂]
  [inst_12 : AddCommMonoid M₂'] [inst_13 : Module R M₂] [inst_14 : Module R M₂'] (f₂ : M₂ →ₗ[R] M₂')
  [inst_15 : IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂),
  (IsLocalizedModule.map S f₀ f₂) (h ∘ₗ g) = (IsLocalizedModule.map S f₁ f₂) h ∘ₗ (IsLocalizedModule.map S f₀ f₁) g
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Cᵒᵖ A),
  Φ.toPresheafFiber X x P =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp P) (Opposite.op ⟨X, x⟩)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullHom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentData f) ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S)
  (hq : CategoryTheory.CategoryStruct.comp g q = q') ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
  (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
  (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (self.hom q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
    self.hom q' gf₁ gf₂ ⋯ ⋯
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_Ioi_iff_Ici : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Ioi x) x ↔ HasDerivWithinAt f f' (Set.Ici x) x
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.unassign : Lean.Meta.Grind.EMatch.Choice → ℕ → Lean.Meta.Grind.EMatch.Choice
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_mod_65536 : ∀ (n : UInt16), n.toUInt64 % 65536 = n.toUInt64
-- Mathlib.Data.Finset.Range
Finset.range_one : Finset.range 1 = {0}
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.disjoint_smul_set_right : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t
-- Init.Data.Nat.Bitwise.Lemmas
Nat.one_and_eq_mod_two : ∀ (n : ℕ), 1 &&& n = n % 2
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.neg : ∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α}
  {f : α → G}, Measurable f → Measurable (-f)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.star_eq_symm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H), star ↑↑e = ↑↑e.symm
-- Mathlib.CategoryTheory.Functor.Basic
/-- The action of a functor on objects.  -/
CategoryTheory.Functor.obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → C → D
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.is_homogeneous' : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  (self : HomogeneousSubsemiring 𝒜), DirectSum.SetLike.IsHomogeneous 𝒜 self.toSubsemiring
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.encodePosNum.match_1.eq_1 : ∀ (motive : PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match PosNum.one with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_1 ()
-- Mathlib.Topology.Category.UniformSpace
/-- An object in the category of uniform spaces.  -/
UniformSpaceCat : Type (u + 1)
-- Lean.Parser.Command
Lean.Parser.Command.openScoped.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.weierstrassP_add_coe_aux : ∀ (L : PeriodPair) (z : ℂ) (l : ↥L.lattice), ↑l / 2 ∉ L.lattice → L.weierstrassP (z + ↑l) = L.weierstrassP z
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_lt : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  Submodule.restrictScalars S s < Submodule.restrictScalars S t ↔ s < t
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inr =
    t.ι.app { as := CategoryTheory.Limits.WalkingPair.right }
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Define the sheaf hom on individual basic opens for the unit.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp : (X : AlgebraicGeometry.LocallyRingedSpace) →
  (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) →
    (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj.obj
        (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶
      X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_of_lt_of_lt : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c d : α},
  a < b → c < d → a + c < b + d
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.map_mk_le : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M} {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N),
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → MulArchimedeanClass.mk (f a) ≤ MulArchimedeanClass.mk (f b)
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Closeds.isometry_singleton : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry fun x => {x}
-- Lean.Data.Format
Lean.Std.Format.format.width : Lean.Option ℕ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_univ : ∀ {α : Type u_2} [inst : Neg α], -Set.univ = Set.univ
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.add_isLittleO : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c₁ l f₁ g → f₂ =o[l] g → c₁ < c₂ → Asymptotics.IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g
-- Init.RCases
/-- An `rcases` pattern is an `rintro` pattern  -/
Lean.Parser.Tactic.rintroPat.one : Lean.ParserDescr
-- Mathlib.Topology.ClusterPt
ClusterPt.of_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f : Filter X}, f ≤ nhds x → ∀ [f.NeBot], ClusterPt x f
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.sign_eq_prod_prod_Iio : ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), Equiv.Perm.sign σ = ∏ j, ∏ i < j, if σ i < σ j then 1 else -1
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.FundamentalSequenceProp.match_1.eq_1 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (h_1 : Unit → motive (Sum.inl none))
  (h_2 : (a : ONote) → motive (Sum.inl (some a))) (h_3 : (f : ℕ → ONote) → motive (Sum.inr f)),
  (match Sum.inl none with
    | Sum.inl none => h_1 ()
    | Sum.inl (some a) => h_2 a
    | Sum.inr f => h_3 f) =
    h_1 ()
-- Lean.Meta.Basic
/-- Given a user-facing name for a free variable, return its declaration in the current local context.
Throw an exception if free variable is not declared.
 -/
Lean.Meta.getLocalDeclFromUserName : Lean.Name → Lean.MetaM Lean.LocalDecl
-- Mathlib.NumberTheory.Padics.PadicNumbers
instInhabitedPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Inhabited ℚ_[p]
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- **Alias** of the forward direction of `Polynomial.natDegree_le_iff_degree_le`. -/
Polynomial.degree_le_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n → p.degree ≤ ↑n
-- Mathlib.Analysis.Normed.Group.Basic
nontrivialTopology_iff_exists_norm_ne_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], NontrivialTopology E ↔ ∃ x, ‖x‖ ≠ 0
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.filter f` is another iterator that applies a
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

In situations where `f` is monadic, use `filterM` instead.

**Marble diagram (without monadic effects):**

```text
it            ---a--b--c--d-e--⊥
it.filter     ---a-----c-------⊥
```

(given that `f a = f c = true` and `f b = f d = d e = false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though
no `Productive` instance is provided. For example, if `f` always returns `True`, the resulting
iterator will be productive as long as `it` is. In such situations, the missing instance needs to
be proved manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned value.
 -/
Std.Iter.filter : {α β : Type w} → [Std.Iterator α Id β] → (f : β → Bool) → Std.Iter β → Std.Iter β
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.of_counit : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : HopfAlgebra R X],
  CoalgebraStruct.counit = CoalgebraStruct.counit
-- Lean.Structure
Lean.StructureFieldInfo.mk : Lean.Name → Lean.Name → Option Lean.Name → Lean.BinderInfo → Option Lean.Expr → Lean.StructureFieldInfo
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain_eq_embDomain_subtype : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M),
  f.extendDomain = Finsupp.embDomain (Function.Embedding.subtype P) f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.fold_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DHashMap.fold (fun d a x => f d a) init m = List.foldl f init m.keys
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_div_div : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k / f l) μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 = 0 → WeierstrassCurve.Projective.Point.toAffine W P = 0
-- Mathlib.Combinatorics.KatonaCircle
/-- A numbering of a fintype `X` is a bijection between `X` and `Fin (card X)`.  -/
Numbering : (X : Type u_1) → [Fintype X] → Type u_1
-- Lean.ResolveName
Lean.ensureReservedNameAvailable : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → String → m Unit
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_top_eq_top_of_essSurj_of_full : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) [F.EssSurj] [F.Full], ⊤.map F = ⊤
-- Mathlib.ModelTheory.Syntax
/-- Take the conjunction of finitely many formulas.

Note that this is an arbitrary formula defined using the axiom of choice. It is only well-defined up
to equivalence of formulas.  -/
FirstOrder.Language.Formula.iInf : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → [Finite α] → (α → L.Formula β) → L.Formula β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
BitVec.cpopTree.eq_1 : ∀ {len w : ℕ} (l : BitVec (len * w)),
  l.cpopTree = if h : len = 0 then 0#w else if h : len = 1 then BitVec.cast ⋯ l else (l.cpopLayer 0#(0 * w) ⋯).cpopTree
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.startPos_ne_endPos : ∀ {s : String.Slice}, s.isEmpty = false → s.startPos ≠ s.endPos
-- Mathlib.Algebra.DualNumber
DualNumber.inv_eps : ∀ {R : Type u_1} [inst : DivisionRing R], DualNumber.eps⁻¹ = 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The cycles functor `ShortComplex C ⥤ C` which sends a short complex `S` to `S.cycles`
which is a kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.cyclesFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.EquivalenceJ.inverse_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (f : w.CostructuredArrowDownwards g),
  (CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).obj f =
    CategoryTheory.StructuredArrow.mk
      (CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CostructuredArrow.left f).hom ⋯)
-- Batteries.Data.HashMap.Basic
/-- Folds a monadic function over the elements in the map (in arbitrary order).
```
def sumEven (sum: Nat) (k : String) (v : Nat) : Except String Nat :=
  if v % 2 == 0 then pure (sum + v) else throw s!"value {v} at key {k} is not even"

foldM sumEven 0 (ofList [("one", 1), ("three", 3)]) =
  Except.error "value 3 at key three is not even"
foldM sumEven 0 (ofList [("two", 2), ("four", 4)]) = Except.ok 6
```
 -/
Batteries.HashMap.foldM : {α : Type u_1} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {m : Type u_2 → Type u_3} →
        {δ : Type u_2} → {β : Type u_4} → [Monad m] → (δ → α → β → m δ) → δ → Batteries.HashMap α β → m δ
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The isomorphism between right lifts induced by a left unitor.  -/
CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (t : CategoryTheory.Bicategory.RightLift f g) → (t.whisker (CategoryTheory.CategoryStruct.id c)).ofIdComp ≅ t
-- Batteries.Classes.Order
Std.LawfulLECmp.isGE_iff_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [inst : LE α] [Std.LawfulLECmp cmp], (cmp x y).isGE = true ↔ y ≤ x
-- Mathlib.Algebra.Module.Injective
Module.Baer.iff_injective : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] [Small.{v, u} R],
  Module.Baer R Q ↔ Module.Injective R Q
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_span_singleton_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Submodule.torsionBySet R M ↑(R ∙ a) = Submodule.torsionBy R M a
-- Mathlib.Analysis.Normed.Module.Ray
not_sameRay_iff_of_norm_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
  ‖x‖ = ‖y‖ → (¬SameRay ℝ x y ↔ x ≠ y)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (M' : Submonoid M),
  f.submonoidMap M' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ofNat_lt_card : ∀ {o : Ordinal.{u_1}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < o.card ↔ OfNat.ofNat n < o
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂]
  {Z : D} (h : (S₂.map F).rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapRightHomologyIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ)) h)
-- Init.Data.List.Attach
List.attachWith_eq_map_attach : ∀ {α : Type u_1} {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a},
  xs.attachWith P H =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (self : CategoryTheory.Triangulated.TStructure C) (n a n' : ℤ),
  a + n' = n → ∀ (X : C), self.ge n X → self.ge n' ((CategoryTheory.shiftFunctor C a).obj X)
-- Init.Data.String.Bootstrap
String.Internal.dropRight : String → ℕ → String
-- Mathlib.Topology.Algebra.Module.Basic
linearMapOfTendsto_apply : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [inst : TopologicalSpace M₂]
  [inst_1 : T2Space M₂] [inst_2 : Semiring R] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₁]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M₁] [inst_7 : Module S M₂] [inst_8 : ContinuousConstSMul S M₂]
  [inst_9 : ContinuousAdd M₂] {σ : R →+* S} {l : Filter α} (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [inst_10 : l.NeBot]
  (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)), ⇑(linearMapOfTendsto f g h) = f