mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- If `PreservesLimit₂ K₁ K₂ G`, obtain that `G.mapCone₂ c₁ c₂` is a limit cone
whenever c₁ c₂ are limit cones.  -/
CategoryTheory.Limits.isLimitOfPreserves₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    {K₁ : CategoryTheory.Functor J₁ C₁} →
                      {K₂ : CategoryTheory.Functor J₂ C₂} →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] →
                            {c₁ : CategoryTheory.Limits.Cone K₁} →
                              CategoryTheory.Limits.IsLimit c₁ →
                                {c₂ : CategoryTheory.Limits.Cone K₂} →
                                  CategoryTheory.Limits.IsLimit c₂ → CategoryTheory.Limits.IsLimit (G.mapCone₂ c₁ c₂)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.closure_eq_setOfPred_isBasis_insert`. -/
Matroid.Indep.closure_eq_setOf_isBasis_insert : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → M.closure I = {x | M.IsBasis I (insert x I)}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_diff_eq_false_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.diff m₂).contains k = false
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_tangentSet_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P},
  as ∈ s.tangentSet ↔ ∃ p ∈ s, s.orthRadius p = as
-- Mathlib.Topology.MetricSpace.PiNat
/-- Metric space structure on `Π (n : ℕ), E n` when the spaces `E n` have the discrete uniformity,
where the distance is given by `dist x y = (1/2)^n`, where `n` is the smallest index where `x` and
`y` differ. Not registered as a global instance by default.  -/
PiNat.metricSpaceOfDiscreteUniformity : {E : ℕ → Type u_2} →
  [inst : (n : ℕ) → UniformSpace (E n)] →
    (∀ (n : ℕ), uniformity (E n) = Filter.principal SetRel.id) → MetricSpace ((n : ℕ) → E n)
-- Std.Time.Zoned.Database.TZdb
/-- Resolves the local timezone file path from the `TZ` environment variable, searching
`zonesPaths` for relative paths and timezone IDs. Falls back to `/etc/localtime` if
`TZ` is unset. Throws if `TZ` is set but its value cannot be found on disk.
 -/
Std.Time.Database.TZdb.resolveLocalPath : Array System.FilePath → IO System.FilePath
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.IsHashSelf.uset : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Array (Std.DHashMap.Internal.AssocList α β)}
  {i : USize} {h : i.toNat < m.size} {d : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.List.HashesTo m[i].toList i.toNat m.size →
      Std.DHashMap.Internal.List.HashesTo d.toList i.toNat m.size) →
    Std.DHashMap.Internal.IsHashSelf m → Std.DHashMap.Internal.IsHashSelf (m.uset i d h)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKeyD.eq_3 : ∀ {α : Type u} {β : α → Type v} (x : α) (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ)
  (k_1 : α) (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKeyD x =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKeyD x
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.tendstoUniformlyOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformly F f p → TendstoUniformlyOnFilter F f p ⊤
-- Mathlib.Analysis.Seminorm
Seminorm.le_def : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, p ≤ q ↔ ∀ (x : E), p x ≤ q x
-- Init.Meta.Defs
/-- Syntax that represent a hexadecimal number without the `0x` prefix.
 -/
Lean.Syntax.HexNum : Type
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- This prevents `ofCoeff x` being printed as `{ coeff := x }` by `delabStructureInstance`.  -/
MonoidAlgebra.delabOfCoeff : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Algebra.UniformConvergence
instMulUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Mul β] → Mul (UniformOnFun α β 𝔖)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- **Alias** of the forward direction of `affineIndependent_vadd`. -/
AffineIndependent.of_vadd : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V}, AffineIndependent k (v +ᵥ p) → AffineIndependent k p
-- Mathlib.RingTheory.PicardGroup
instCommGroupPic : (R : Type u) → [inst : CommSemiring R] → CommGroup (CommRing.Pic R)
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instIsCancelVAddSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd M' α]
  [IsCancelVAdd M' α], IsCancelVAdd (↥s) α
-- Init.WF
/-- If the first projections of two pairs are equal, then they are lexicographically ordered if the
second projections are ordered.
 -/
Prod.Lex.right : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.mapIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ≅ g b),
  (CategoryTheory.Limits.biproduct.mapIso p).inv = CategoryTheory.Limits.biproduct.map fun b => (p b).inv
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.map_monoOfLE : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y),
  (CategoryTheory.ConcreteCategory.hom (X.map (SSet.N.monoOfLE h).op)) y.simplex = x.simplex
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing cocone  -/
CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] →
      [CategoryTheory.Limits.HasPushouts C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) → CategoryTheory.Limits.Cocone F
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertList.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertList l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) l_1
-- Mathlib.Tactic.GCongr.ForwardAttr
/-- Read a `gcongr_forward` extension from a declaration of the right type.  -/
Mathlib.Tactic.GCongr.mkForwardExt : Lean.Name → Lean.ImportM Mathlib.Tactic.GCongr.ForwardExt
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.resolveParserNameCore.isParser : Lean.Environment → Lean.Name → Option Bool
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Iio : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Iio b ↔ x < b
-- Mathlib.Data.Set.Prod
Set.diagonal_nonempty : ∀ {α : Type u_1} [Nonempty α], (Set.diagonal α).Nonempty
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1)
      (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) =
    f.f 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inl_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.desc f g) = f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.closed.injEq : ∀ (seq seq_1 : List Lean.Meta.Grind.TGrind),
  (Lean.Meta.Grind.ActionResult.closed seq = Lean.Meta.Grind.ActionResult.closed seq_1) = (seq = seq_1)
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.eq_def : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (l : List α),
  List.minOn? f l =
    match l with
    | [] => none
    | x :: xs => some (List.foldl (minOn f) x xs)
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- The extensive topology on a finitary pre-extensive category is subcanonical.  -/
CategoryTheory.extensiveTopology.subcanonical : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C],
  (CategoryTheory.extensiveTopology C).Subcanonical
-- Mathlib.Topology.Order.ExtrClosure
IsLocalMinOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsLocalMinOn f s a → ContinuousOn f (closure s) → IsLocalMinOn f (closure s) a
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iExsUnique.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (β : Type v') [inst : Finite β] (φ : L.Formula (α ⊕ β)),
  FirstOrder.Language.Formula.iExsUnique β φ =
    FirstOrder.Language.Formula.iExs β
      (φ ⊓
        FirstOrder.Language.Formula.iAlls β
          ((FirstOrder.Language.Formula.relabel (fun a => Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
            (FirstOrder.Language.BoundedFormula.iInf fun g =>
              (FirstOrder.Language.var (Sum.inr g)).equal (FirstOrder.Language.var (Sum.inl (Sum.inr g))))))
-- Std.Sync.Broadcast
Std.Broadcast.Receiver.instAsyncWriteOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncWrite (Std.Broadcast α) α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_inf_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : SemilatticeInf M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ},
  (a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_homologyπ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] {Z : C} (h : K.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.Iterators.Lemmas.Producers.Vector
Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_not_lt : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, ¬pos < n → (xs.iterFromIdx pos).IsPlausibleStep Std.IterStep.done
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.eq_zero_of_add_right : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R},
  IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_ne_nhdsWithin : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ᶠ (x' : X) in nhdsWithin x {x}ᶜ, ↑e x' ≠ ↑e x
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : CategoryTheory.Mod D A} {hom : M.X ⟶ N.X}
  {isModHom : CategoryTheory.IsModHom A hom} {hom_1 : M.X ⟶ N.X} {isModHom_1 : CategoryTheory.IsModHom A hom_1},
  { hom := hom, isModHom := isModHom } = { hom := hom_1, isModHom := isModHom_1 } → hom = hom_1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findM?_pure : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → ULift.{w, 0} Bool}, (it.findM? fun x => pure (f x)) = it.find? fun x => (f x).down
-- Mathlib.Analysis.Meromorphic.Divisor
MeromorphicOn.divisor_of_eventuallyEq_codiscreteWithin_preperfect : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      Preperfect U → f₁ =ᶠ[Filter.codiscreteWithin U] f₂ → MeromorphicOn.divisor f₁ U = MeromorphicOn.divisor f₂ U
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMonoid.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instMonoid =
    { toMul := BoundedContinuousFunction.instMul, mul_assoc := ⋯, toOne := BoundedContinuousFunction.instOne,
      one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Algebra.Group.Basic
sub_eq_self : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = a ↔ b = 0
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldr_flip_eq_foldl`.

---

**Second Bird–Wadler duality theorem**.  -/
List.foldl_eq_foldr' : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v],
  List.foldr (flip v) b l = List.foldl v b l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k : α} [inst : Inhabited β] {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.modify k f t) k =
        (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH1_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (groupCohomology.shortComplexH1 A).g = groupCohomology.d₁₂ A
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mk.injEq : ∀ {R : Type u_2} [inst : NonAssocRing R] (toMulRingSeminorm : MulRingSeminorm R)
  (eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0) (toMulRingSeminorm_1 : MulRingSeminorm R)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0),
  ({ toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }) =
    (toMulRingSeminorm = toMulRingSeminorm_1)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The functor sending a natural number `i` to the `i`-th power of the ideal `J`  -/
localCohomology.idealPowersDiagram : {R : Type u} → [inst : CommRing R] → Ideal R → CategoryTheory.Functor ℕᵒᵖ (Ideal R)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.map_homInvId : ∀ {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y),
  (I.map f).homInvId = (I.homInvId.map f).ofEq ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instFunLike.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (φ : M →* N) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] (B : Type u_5) [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B],
  DistribMulActionHom.instFunLike φ A B = { coe := fun m => m.toFun, coe_injective := ⋯ }
-- Init.Classical
/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches.  -/
Classical.dite_not : ∀ {p : Prop} {α : Sort u_1} [hn : Decidable ¬p] (x : ¬p → α) (y : ¬¬p → α), dite (¬p) x y = dite p (fun h => y ⋯) x
-- Mathlib.Data.DFinsupp.Interval
/-- Pointwise `Finset.singleton` bundled as a `DFinsupp`.  -/
DFinsupp.singleton : {ι : Type u_1} → {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → (Π₀ (i : ι), α i) → Π₀ (i : ι), Finset (α i)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductives : Lean.Meta.IndPredBelow.Context✝ → Lean.MetaM Unit
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCategoryWithWeakEquivalencesOpposite : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → HomotopicalAlgebra.CategoryWithWeakEquivalences Cᵒᵖ
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_atTop_atTop : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ioo Filter.atTop Filter.atTop
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Replacing the first point by one on the same line does not change twice the oriented angle.  -/
Collinear.two_zsmul_oangle_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₁' p₂ p₃ : P},
  Collinear ℝ {p₁, p₂, p₁'} →
    p₁ ≠ p₂ → p₁' ≠ p₂ → 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁' p₂ p₃
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is upper hemicontinuous at `x` within a set `s` if, whenever `t` is
a neighborhood of `f x`, then `t` is a neighborhood of `f x'` for all `x'` sufficiently close to
`x` within `s`.  -/
UpperHemicontinuousWithinAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Set α → α → Prop
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramState.mk.sizeOf_spec : ∀ (sub : String) (embeds : Std.HashMap String (String × ProofWidgets.Html)),
  sizeOf { sub := sub, embeds := embeds } = 1 + sizeOf sub + sizeOf embeds
-- Mathlib.AlgebraicGeometry.AffineSpace
_private.Mathlib.AlgebraicGeometry.AffineSpace.0.AlgebraicGeometry.«termℤ[_]» : Lean.ParserDescr
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_map_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : UpperSet α),
  ↑((UpperSet.map f) s) = ⇑f '' ↑s
-- Mathlib.Algebra.Group.Translate
translate_add : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a b : G) (f : G → α),
  translate (a + b) f = translate a (translate b f)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h)
-- Mathlib.Data.Finset.Fin
/-- Given a Finset `s` of `ℕ` contained in `{0,..., n-1}`, the corresponding Finset in `Fin n`
is `s.attachFin h` where `h` is a proof that all elements of `s` are less than `n`.  -/
Finset.attachFin : (s : Finset ℕ) → {n : ℕ} → (∀ m ∈ s, m < n) → Finset (Fin n)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_top_top : ContinuousAt (fun p => p.1 + p.2) (⊤, ⊤)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsTrivial.not_mem_edgeSet : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, H.IsTrivial → e ∉ H.edgeSet
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ), Differentiable 𝕜 ↑z
-- Mathlib.Order.Bounds.Defs
BddAbove.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), BddAbove s = (upperBounds s).Nonempty
-- Init.Data.BitVec.Lemmas
BitVec.umod_eq_of_lt : ∀ {w : ℕ} {x y : BitVec w}, x < y → x % y = x
-- Mathlib.Data.Nat.Factors
/-- If `p` is a prime factor of `a` then `p` is also a prime factor of `a * b` for any `b > 0`  -/
Nat.mem_primeFactorsList_mul_left : ∀ {p a b : ℕ}, p ∈ a.primeFactorsList → b ≠ 0 → p ∈ (a * b).primeFactorsList
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The algebra equiv `A/I ≃ₐ[R] B/J` induced by an algebra equiv `f : A ≃ₐ[R] B`,
where `J = f(I)`.  -/
Ideal.quotientEquivAlg : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Ring B] →
              [inst_4 : Algebra R₁ B] →
                (I : Ideal A) →
                  (J : Ideal B) →
                    [inst_5 : I.IsTwoSided] →
                      [inst_6 : J.IsTwoSided] → (f : A ≃ₐ[R₁] B) → J = Ideal.map (↑f) I → (A ⧸ I) ≃ₐ[R₁] B ⧸ J
-- Aesop.Script.Step
Aesop.Script.LazyStep.mk : Lean.Meta.SavedState →
  Lean.MVarId →
    (tacticBuilders : Array Aesop.Script.TacticBuilder) →
      autoParam (0 < tacticBuilders.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam →
        Lean.Meta.SavedState → Array Lean.MVarId → Aesop.Script.LazyStep
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.congr_simp : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f)
  (x : AdicCompletion.AdicCauchySequence I N) (n : ℕ),
  AdicCompletion.mapPreimage✝ hf x n = AdicCompletion.mapPreimage✝ hf x n
-- Init.Data.List.Basic
List.reverseAux.eq_2 : ∀ {α : Type u} (x : List α) (a : α) (l : List α), (a :: l).reverseAux x = l.reverseAux (a :: x)
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.Limits.IsColimit
              { pt := A, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₁ f g P₁ P₂ }
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsLeftRegular.pow_injective : ∀ {R : Type u_1} [inst : Monoid R] {r : R} [IsMulTorsionFree R],
  IsLeftRegular r → r ≠ 1 → Function.Injective fun n => r ^ n
-- Init.Data.List.Lex
List.instTransLt : {α : Type u_1} →
  [inst : LT α] →
    [Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] →
      Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2