mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_mor₂ : ∀ {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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).mor₂ = h.m₃
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff'`. -/
CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff' : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsCardinalPresentable J κ ↔ HasCardinalLT (↑J.obj) κ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.parseWithDate : Std.Time.GenericFormat.DateBuilder✝ →
  Std.Time.FormatConfig → Std.Time.FormatPart → Std.Internal.Parsec.String.Parser Std.Time.GenericFormat.DateBuilder✝
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 2]` which avoids `1`.  -/
SSet.horn₃₂.ι₁ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 2).toSSet
-- Std.Net.Addr
Std.Net.AddressFamily.noConfusionType : Sort v✝ → Std.Net.AddressFamily → Std.Net.AddressFamily → Sort v✝
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_sup_map_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S T : L.Substructure M),
      FirstOrder.Language.Substructure.comap f
          (FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T) =
        S ⊔ T
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Array.filterSepElemsMAux : {m : Type → Type} →
  [Monad m] → Array Lean.Syntax → (Lean.Syntax → m Bool) → ℕ → Array Lean.Syntax → m (Array Lean.Syntax)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundant_iff_sum_divisors : ∀ {n : ℕ}, n.Abundant ↔ 2 * n < ∑ i ∈ n.divisors, i
-- Mathlib.Analysis.Normed.Group.InfiniteSum
HasSum.norm_le_of_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ},
  HasSum f a → HasSum g b → (∀ (i : ι), ‖f i‖ ≤ g i) → ‖a‖ ≤ b
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoAppX M).hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {l : List ((a : α) × β a)},
  Std.DTreeMap.ofList l cmp = ∅.insertMany l
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.self_lt_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a : α}, a < 1 → a < a⁻¹
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderAt f z₀ ≠ 0 ↔ AnalyticAt 𝕜 f z₀ ∧ f z₀ = 0
-- Init.Data.Array.Attach
Array.toList_attach : ∀ {α : Type u_1} {xs : Array α}, xs.attach.toList = xs.toList.attachWith (fun x => x ∈ xs) ⋯
-- Mathlib.Data.EReal.Inv
EReal.lt_div_iff : ∀ {a b c : EReal}, 0 < b → b ≠ ⊤ → (a < c / b ↔ a * b < c)
-- Lean.Elab.DeclModifiers
/-- Ensure the function has not already been declared, and apply the given visibility setting to `declName`.
If `private`, return the updated name using our internal encoding for private names.
If `protected`, register `declName` as protected in the environment.
 -/
Lean.Elab.applyVisibility : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadError m] →
        [MonadFinally m] → [Lean.Elab.MonadInfoTree m] → Lean.Elab.Modifiers → Lean.Name → m Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.strongInnerAnodyneExtensions_ι_iff : ∀ {X : SSet} (A : X.Subcomplex), SSet.strongInnerAnodyneExtensions A.ι ↔ ∃ P, ∃ (x : P.IsRegular), P.IsInner
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsCardinalPresentable X κ]
  [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J] [CategoryTheory.IsCardinalFiltered J κ]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) {i : J}
  (f₁ f₂ : X ⟶ F.obj i),
  CategoryTheory.CategoryStruct.comp f₁ (c.ι.app i) = CategoryTheory.CategoryStruct.comp f₂ (c.ι.app i) →
    ∃ j u, CategoryTheory.CategoryStruct.comp f₁ (F.map u) = CategoryTheory.CategoryStruct.comp f₂ (F.map u)
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ChooseArg.mk.injEq : ∀ (ref : Lean.Syntax) (name : Lean.Name) (expectedType? : Option Lean.Term) (ref_1 : Lean.Syntax) (name_1 : Lean.Name)
  (expectedType?_1 : Option Lean.Term),
  ({ ref := ref, name := name, expectedType? := expectedType? } =
      { ref := ref_1, name := name_1, expectedType? := expectedType?_1 }) =
    (ref = ref_1 ∧ name = name_1 ∧ expectedType? = expectedType?_1)
-- Init.Data.Dyadic.Basic
Int.trailingZeros_two_mul : ∀ {i : ℤ}, i ≠ 0 → (2 * i).trailingZeros = i.trailingZeros + 1
-- Init.Data.Order.Ord
Fin.instOrientedOrd : ∀ (n : ℕ), Std.OrientedOrd (Fin n)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_mono_nnnorm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  0 ≤ q → (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) → MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.induction_on : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop},
  (∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), p (MeasureTheory.AEEqFun.mk f hf)) → p f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.homOfPiHom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X)
  (x : { I := J, obj := f }.I), (CategoryTheory.Limits.FormalCoproduct.homOfPiHom X f φ).f x = PUnit.unit
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- `C` has all (small) conical limits if it has limits of every shape that is as big as its
hom-sets.  -/
CategoryTheory.Enriched.HasConicalLimits : (V : outParam (Type u')) →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [inst_2 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop
-- Lean.Elab.Tactic.Monotonicity
/-- Base case for solveMonoStep: Handles goals of the form
```
monotone (fun f => f.1.2 x y)
```

It's tricky to solve them compositionally from the outside in, so here we construct the proof
from the inside out.
 -/
Lean.Meta.Monotonicity.solveMonoCall : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Parser.Command
Lean.Parser.Term.quot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.Hom.ext_iff : ∀ {R S : CommSemiRingCat} {x y : R.Hom S}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.finZeroElim_eq_zero : ∀ {α : Type u_1} [inst : Zero α], finZeroElim = 0
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.Nodup.le_nsmul_iff_le : ∀ {α : Type u_1} {s t : Multiset α} {n : ℕ}, s.Nodup → n ≠ 0 → (s ≤ n • t ↔ s ≤ t)
-- Mathlib.Algebra.Order.Ring.Abs
Odd.of_dvd_nat : ∀ {m n : ℕ}, Odd n → m ∣ n → Odd m
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_inverse_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Over X)ᵒᵖ} (f : Z ⟶ Y),
  (CategoryTheory.Under.opEquivOpOver X).inverse.map f =
    CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatQuarterShort : Std.Time.DateFormatSymbols → Std.Time.Month.Quarter → String
-- Init.Data.UInt.Lemmas
UInt32.sub_left_inj : ∀ {a b : UInt32} (c : UInt32), a - c = b - c ↔ a = b
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.injective : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.ElementaryEmbedding M N), Function.Injective ⇑φ
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_univ_of_noncompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α], Metric.diam Set.univ = 0
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (a : Std.DHashMap.Internal.AssocList α β) (a_1 : δ),
  Std.DHashMap.Internal.AssocList.forInStep.go✝ f a a_1 =
    match a, a_1 with
    | Std.DHashMap.Internal.AssocList.nil, acc => pure (ForInStep.yield acc)
    | Std.DHashMap.Internal.AssocList.cons k v t, acc => do
      let __do_lift ← f k v acc
      match __do_lift with
        | ForInStep.done d => pure (ForInStep.done d)
        | ForInStep.yield d => Std.DHashMap.Internal.AssocList.forInStep.go✝ f t d
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
ContinuousLinearMap.compFormalMultilinearSeries_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F)
  (n : ℕ), f.compFormalMultilinearSeries p n = f.compContinuousMultilinearMap (p n)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.denote_ite : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : Std.Sat.AIG.RefVec.IfInput aig w} (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.ite aig input).aig, ref := (Std.Sat.AIG.RefVec.ite aig input).vec.get idx hidx }⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧
    else ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Symbols with VSCode extension abbreviation, as of March 17, 2026.
Obtained using `scripts/extract-unique-nonascii.lean` from
https://github.com/leanprover/vscode-lean4/blob/132d329aa8afa3e8508ef77cfdcff112d3b35c88
 -/
_private.Mathlib.Tactic.Linter.TextBased.UnicodeLinter.0.Mathlib.Linter.TextBased.UnicodeLinter.withVSCodeAbbrev : Array Char
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.pretrivialization_mem_atlas : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (self : VectorPrebundle R F E) (x : B), self.pretrivializationAt x ∈ self.pretrivializationAtlas
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.not_isCycle_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, ¬SimpleGraph.Walk.nil.IsCycle
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.q : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Month.Quarter
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.messages : Lean.Lsp.Trace
-- Init.Core
DoResultPRBC.continue.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : σ),
  sizeOf (DoResultPRBC.continue a) = 1 + sizeOf a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_int_mul_pi : ∀ (n : ℤ), Complex.tan (↑n * ↑Real.pi) = 0
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is not included in the range.
   -/
Std.Rco.upper : {α : Type u} → Std.Rco α → α
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_update : ∀ {α : Type u} (f : α → α) (s : Stream'.Seq α) (n m : ℕ),
  (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m
-- Mathlib.Algebra.Order.Ring.Basic
Even.pow_pos_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Even n → n ≠ 0 → (0 < a ^ n ↔ a ≠ 0)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
  CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
-- Init.Data.List.Attach
/-- Maps a partially defined function (defined on those terms of `α` that satisfy a predicate `P`) over
a list `l : List α`, given a proof that every element of `l` in fact satisfies `P`.

`O(|l|)`. `List.pmap`, named for “partial map,” is the equivalent of `List.map` for such partial
functions.
 -/
List.pmap : {α : Type u_1} → {β : Type u_2} → {P : α → Prop} → ((a : α) → P a → β) → (l : List α) → (∀ a ∈ l, P a) → List β
-- Mathlib.Data.List.SplitLengths
List.length_mem_splitLengths : ∀ {α : Type u_2} (l : List α) (sz : List ℕ) (b : ℕ), (∀ n ∈ sz, n ≤ b) → ∀ l₂ ∈ sz.splitLengths l, l₂.length ≤ b
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_sub : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : F.obj X ⟶ Y),
  (adj.homEquiv X Y) (f - f') = (adj.homEquiv X Y) f - (adj.homEquiv X Y) f'
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.free_obj : ∀ (R : Type u) [inst : CommRing R] (S : Type u), (AlgCat.free R).obj S = AlgCat.of R (FreeAlgebra R S)
-- Mathlib.Data.Set.Lattice.Image
Set.InjOn.image_biInter_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {p : ι → Prop} {s : (i : ι) → p i → Set α},
  (∃ i, p i) →
    ∀ {f : α → β},
      Set.InjOn f (⋃ i, ⋃ (hi : p i), s i hi) → f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi
-- Mathlib.Topology.Order.Basic
/-- The set of points which are isolated on the left is countable when the space is
second-countable.  -/
countable_of_isolated_left' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | ∃ y < x, Set.Ioo y x = ∅}.Countable
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {g : N → N'}, MDiff f → MDiff g → MDiff (Prod.map f g)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions_unionProd_ι : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  SSet.anodyneExtensions B.ι → SSet.anodyneExtensions (A.unionProd B).ι
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- A nonempty, bounded below set of real numbers has a greatest lower bound.  -/
Real.exists_isGLB : ∀ {s : Set ℝ}, s.Nonempty → BddBelow s → ∃ x, IsGLB s x
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanAdjunction.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) (H : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  L.lanAdjunction H =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun F G => (L.lan.obj F).homEquivOfIsLeftKanExtension (L.lanUnit.app F) G,
        homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderBaseChange_iff_pullbacks_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  (CategoryTheory.ShortComplex.leftHomologyMapIso e).hom = CategoryTheory.ShortComplex.leftHomologyMap e.hom
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} [inst_1 : SizeOf C]
  (I : Type v) [ℐ : CategoryTheory.SmallCategory I] [hI : CategoryTheory.IsFiltered I] (F : CategoryTheory.Functor I C)
  (ι : F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A)
  (isColimit : CategoryTheory.Limits.IsColimit { pt := A, ι := ι }),
  sizeOf { I := I, ℐ := ℐ, hI := hI, F := F, ι := ι, isColimit := isColimit } =
    1 + sizeOf I + sizeOf ℐ + sizeOf hI + sizeOf F + sizeOf ι + sizeOf isColimit
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Interpret `f : α →ₘ[μ] β` as a germ at `ae μ` forgetting that `f` is almost everywhere
strongly measurable.  -/
MeasureTheory.AEEqFun.toGerm : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → (α →ₘ[μ] β) → (MeasureTheory.ae μ).Germ β
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.Free.addMonoidHom : ∀ (M : Type v) (N : Type w) [inst : AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M] [inst_3 : AddCommGroup N]
  [Module.Free ℤ N], Module.Free ℤ (M →+ N)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.modByMonicHom_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (g : Polynomial R), h.modByMonicHom (h.map g) = g %ₘ f
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_refl : ∀ {R : Type u_5} (K : Type u_7) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K],
  FractionalIdeal.ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingEquiv.refl (FractionalIdeal (nonZeroDivisors R) K)
-- Mathlib.RingTheory.NormalClosure
_private.Mathlib.RingTheory.NormalClosure.0.Ring.termK : Lean.ParserDescr
-- Init.System.IO
IO.FS.DirEntry.mk.inj : ∀ {root : System.FilePath} {fileName : String} {root_1 : System.FilePath} {fileName_1 : String},
  { root := root, fileName := fileName } = { root := root_1, fileName := fileName_1 } →
    root = root_1 ∧ fileName = fileName_1
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.categoryWithCofibrations : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.ModelCategory C] → HomotopicalAlgebra.CategoryWithCofibrations C
-- Init.Data.Array.Lemmas
Array.toList_set! : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {x : α}, (xs.set! i x).toList = xs.toList.set i x
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.zerothHomotopyEquiv_mk : ∀ {X : TopCat} (x : ↑X), TopCat.zerothHomotopyEquiv (ZerothHomotopy.mk x) = SSet.π₀.mk (TopCat.toSSetObj₀Equiv.symm x)
-- Mathlib.CategoryTheory.Galois.Basic
/-- The arbitrarily chosen fiber functor `GaloisCategory.getFiberFunctor` is a fiber functor.  -/
CategoryTheory.PreGaloisCategory.instFiberFunctorGetFiberFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C],
  CategoryTheory.PreGaloisCategory.FiberFunctor (CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor C)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.CharP.dpow_of_prime_le : ∀ (A : Type u_1) [inst : CommRing A] (p : ℕ) [inst_1 : CharP A p] [inst_2 : Fact (Nat.Prime p)] {I : Ideal A}
  [inst_3 : DecidablePred fun x => x ∈ I] (hIp : I ^ p = 0) {n : ℕ},
  p ≤ n → ∀ (a : A), (DividedPowers.CharP.dividedPowers A p hIp).dpow n a = 0
-- Mathlib.Analysis.Normed.Module.Bases
/-- The range of the projection is the span of the basis elements in `A`.  -/
GeneralSchauderBasis.range_proj_eq_span : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β),
  (↑(b.proj A)).range = Submodule.span 𝕜 (↑b '' ↑A)