mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lex
instUniqueColex : (α : Type u_2) → [Unique α] → Unique (Colex α)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT!_eq_get!_getEntryLT? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α}
  [inst_1 : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.getEntryLT! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t).get!
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.getKey? km = some km
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.eraseIdxIfInBounds.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ), xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i h else xs
-- Mathlib.RingTheory.Algebraic.Cardinality
Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial : ∀ (R : Type u) [inst : CommRing R] [IsDomain R] (L : Type u) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L],
  Cardinal.mk L ≤ Cardinal.mk ((p : Polynomial R) × { x // x ∈ p.aroots L })
-- Init.Data.UInt.Basic
/-- Adds two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.add : UInt16 → UInt16 → UInt16
-- Mathlib.Order.WithBot
WithBot.semilatticeSup : {α : Type u_1} → [SemilatticeSup α] → SemilatticeSup (WithBot α)
-- Mathlib.Order.Hom.CompleteLattice
sSupHomClass.mk : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : FunLike F α β],
  (∀ (f : F) (s : Set α), f (sSup s) = sSup (⇑f '' s)) → sSupHomClass F α β
-- Mathlib.Tactic.Push.Attr
/-- Converts a `Head` to a string.  -/
Mathlib.Tactic.Push.Head.toString : Mathlib.Tactic.Push.Head → String
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_eq_or_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b < a ↔ b = a ∨ b < a
-- Aesop.RuleTac.GoalDiff
/-- A representation of the differences between two goals. Each Aesop rule produces
a `GoalDiff` between the goal on which the rule was run (the 'old goal') and
each of the subgoals produced by the rule (the 'new goals').

We use the produced `GoalDiff`s to update stateful data structures which cache
information about Aesop goals and for which it is more efficient to update the
cached information than to recompute it for each goal.

Hypotheses are identified by their `FVarId` *and* type and value (if any).
This means that when a hypothesis `h : T` with `FVarId` `i` appears in the old
goal and `h : T'` with `FVarId` `i` appears in the new goal, but `T` is not
defeq to `T'`, then `h` is treated as both added (with the new type) and
removed (with the old type). This can happen when the type of a hyp changes to
another type that is definitionally equal at `default`, but not at `reducible`
transparency.

The target is identified up to defeq. All defeq comparisons are made at
reducible transparency and metavariables are treated as rigid.
 -/
Aesop.GoalDiff : Type
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_iSup : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {ι : Sort u_1}
  (s : ι → X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (⨆ i, s i) =
    ⨆ i, (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (s i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- **Alias** of `SSet.chainComplexFunctorAdjunction`.

---

The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `R : C` and `F : SSet ⥤ C`.  -/
SSet.singularChainComplexFunctorAdjunction : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (n : ℕ) →
          (CategoryTheory.Functor.postcompose₂.obj (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).obj
              (SSet.chainComplexFunctor C) ⊣
            (CategoryTheory.evaluation SSet C).obj (SSet.stdSimplex.obj { len := n })
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k},
  (t.insertIfNew k v).getD a fallback = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.getD a fallback
-- Mathlib.Data.ENat.Basic
/-- A version of `WithTop.map` for `AddMonoidHom`s.  -/
AddMonoidHom.ENatMap : {N : Type u_2} → [inst : AddZeroClass N] → (ℕ →+ N) → ℕ∞ →+ WithTop N
-- Lean.AuxRecursor
Lean.markNoConfusion : Lean.Environment → Lean.Name → Lean.NoConfusionInfo → Lean.Environment
-- Mathlib.Algebra.Module.Hom
AddMonoidHom.instDomMulActModule : {S : Type u_6} →
  {M : Type u_7} →
    {M₂ : Type u_8} →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid M₂] → [Module S M] → Module Sᵈᵐᵃ (M →+ M₂)
-- Lean.Meta.KExprMap
Lean.Meta.KExprMap.map : {α : Type} → Lean.Meta.KExprMap α → Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.apply_symm_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂), e (e.symm x) = x
-- Mathlib.Tactic.UnsetOption
/-- Unset a user option  -/
Lean.Elab.Command.unsetOption : Lean.ParserDescr
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedDBuilderName.default : Aesop.Frontend.DBuilderName
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_top : ∀ {M : Type u_2} [inst : AddZeroClass M], ⊤.unop = ⊤
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instAdd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → {P Q : CategoryTheory.Idempotents.Karoubi C} → Add (P ⟶ Q)
-- Mathlib.Algebra.Homology.ShortComplex.Linear
/-- Given a right homology map data for morphism `φ`, this is the induced right homology
map data for `a • φ`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.smul : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.RightHomologyData} →
                  {h₂ : S₂.RightHomologyData} →
                    CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ →
                      (a : R) → CategoryTheory.ShortComplex.RightHomologyMapData (a • φ) h₁ h₂
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
divisorsAntidiagonalFactors.eq_1 : ∀ (n : ℕ+) (x : ↥(↑n).divisorsAntidiagonal), divisorsAntidiagonalFactors n x = (⟨(↑x).1, ⋯⟩, ⟨↑⟨(↑x).2, ⋯⟩, ⋯⟩)
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalNPow : ∀ {a : Ordinal.{u}} {b an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an ^ bn = rn → Mathlib.Meta.NormNum.IsNat (a ^ b) rn
-- Mathlib.Algebra.Order.Module.Defs
inv_smul_lt_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β], 0 < a → (a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂)
-- Mathlib.Tactic.Abel
/-- The default form  -/
Mathlib.Tactic.Abel.AbelMode.term : Mathlib.Tactic.Abel.AbelMode
-- Init.Data.BitVec.Lemmas
BitVec.toNat_add_of_not_uaddOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.uaddOverflow y = true → (x + y).toNat = x.toNat + y.toNat
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.mk.injEq : ∀ {α₁ : Type w} {m : Type w → Type w'} {β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w}
  (left : Std.IterM m β₁) (memoizedLeft : Option { out // ∃ it, it.IsPlausibleOutput out }) (right : Std.IterM m β₂)
  (left_1 : Std.IterM m β₁) (memoizedLeft_1 : Option { out // ∃ it, it.IsPlausibleOutput out })
  (right_1 : Std.IterM m β₂),
  ({ left := left, memoizedLeft := memoizedLeft, right := right } =
      { left := left_1, memoizedLeft := memoizedLeft_1, right := right_1 }) =
    (left = left_1 ∧ memoizedLeft = memoizedLeft_1 ∧ right = right_1)
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_sdiff : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α →
      (MeasureTheory.projectiveFamilyContent hP) s - (MeasureTheory.projectiveFamilyContent hP) t ≤
        (MeasureTheory.projectiveFamilyContent hP) (s \ t)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 g s → DifferentiableOn 𝕜 (f + g) s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c) (CategoryTheory.Limits.limit.π F j) =
    c.π.app j
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given a distinguished triangle `T` such that `T.mor₃ = 0` and the datum of morphisms
`inr : T.obj₃ ⟶ T.obj₂` and `fst : T.obj₂ ⟶ T.obj₁` satisfying suitable relations, this
is the binary biproduct data expressing that `T.obj₂` identifies to the binary
biproduct of `T.obj₁` and `T.obj₃`.
See also `exists_iso_binaryBiproduct_of_distTriang`.  -/
CategoryTheory.Pretriangulated.binaryBiproductData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              (T : CategoryTheory.Pretriangulated.Triangle C) →
                T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                  T.mor₃ = 0 →
                    (inr : T.obj₃ ⟶ T.obj₂) →
                      CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃ →
                        (fst : T.obj₂ ⟶ T.obj₁) →
                          CategoryTheory.CategoryStruct.comp fst T.mor₁ +
                                CategoryTheory.CategoryStruct.comp T.mor₂ inr =
                              CategoryTheory.CategoryStruct.id T.obj₂ →
                            CategoryTheory.Limits.BinaryBiproductData T.obj₁ T.obj₃
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.coe_range : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x → AlgebraicIndependent R Subtype.val
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.f₁.eq_1 : ∀ {ι : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] (s : Finset ι) (_a : ι → ZMod p),
  f₁✝ s _a = ∑ i, MvPolynomial.X i ^ (p - 1)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.eqToHom_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (h : X = Y),
  CategoryTheory.Arrow.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.one_le_toENat : ∀ {c : Cardinal.{u}}, 1 ≤ Cardinal.toENat c ↔ 1 ≤ c
-- Lean.Meta.Basic
/-- Return `some decl` if `fvarId` is declared in the current local context.
 -/
Lean.FVarId.findDecl? : Lean.FVarId → Lean.MetaM (Option Lean.LocalDecl)
-- Mathlib.Data.FinEnum
FinEnum.prod : {α : Type u} → {β : Type u_1} → [FinEnum α] → [FinEnum β] → FinEnum (α × β)
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.del.sizeOf_spec : ∀ (ids : Array ℕ), sizeOf (Mathlib.Tactic.Sat.LRATStep.del ids) = 1 + sizeOf ids
-- Mathlib.Algebra.Group.Units.Defs
divp_assoc : ∀ {α : Type u} [inst : Monoid α] (a b : α) (u : αˣ), a * b /ₚ u = a * (b /ₚ u)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.forall : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {P : Subgroup ↥H → Prop},
  (∀ (H' : Subgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.subgroupOf H)
-- Init.Data.Rat.Lemmas
Rat.mul_le_mul_of_nonneg_left : ∀ {a b c : ℚ}, a ≤ b → 0 ≤ c → c * a ≤ c * b
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_eq_ofNat : ∀ n < USize.size, USize.ofNatClamp n = USize.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_subset_of_subgraph : ∀ {V : Type u} {G : SimpleGraph V} {x y : G.Subgraph}, x ≤ y → ∀ (v : V), x.neighborSet v ⊆ y.neighborSet v
-- Mathlib.RingTheory.Nilpotent.Defs
pow_nilpotencyClass : ∀ {R : Type u_1} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ], IsNilpotent x → x ^ nilpotencyClass x = 0
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.expandGoal.doUnsafe : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.GoalRef → Array Aesop.PostponedSafeRule → Aesop.SearchM Q Aesop.RuleResult
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.mvfunctor : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → MvFunctor (MvQPF.Fix F)
-- Init.Data.UInt.Lemmas
UInt16.add_def : ∀ (a b : UInt16), a + b = { toBitVec := a.toBitVec + b.toBitVec }
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.instIsMulCommutative_iSup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Type u_1} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o NonUnitalSubring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_le_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (t : Multiset α), s.Nodup → s.ndinter t ≤ t
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of the function `z ↦ z - z₀` at `z₀` is `1`.  -/
MeromorphicOn.divisor_sub_const_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z₀ : 𝕜} {U : Set 𝕜},
  z₀ ∈ U → (MeromorphicOn.divisor (fun x => x - z₀) U) z₀ = 1
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnityEquivNthRoots_symm_apply : ∀ {R : Type u_4} {k : ℕ} [inst : NeZero k] [inst_1 : CommRing R] [inst_2 : IsDomain R]
  (x : { x // x ∈ Polynomial.nthRoots k 1 }), ↑↑((rootsOfUnityEquivNthRoots R k).symm x) = ↑x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.mk.injEq : ∀ (p : Lean.Grind.Linarith.Poly) (h : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) (p_1 : Lean.Grind.Linarith.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof), ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The currying operation `Sigma.curry` as a measurable equivalence.
See `MeasurableEquiv.piCurry` for the dependent version.  -/
MeasurableEquiv.curry : (ι : Type u_6) → (κ : Type u_7) → (X : Type u_8) → [inst : MeasurableSpace X] → (ι × κ → X) ≃ᵐ (ι → κ → X)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.ofArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : Array ((a : α) × β a)},
  (Std.DTreeMap.Raw.ofArray a cmp).WF
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.countRestricted_two : ∀ (n : ℕ), Nat.Partition.countRestricted n 2 = Nat.Partition.distincts n
-- Mathlib.AlgebraicGeometry.Over
AlgebraicGeometry.Scheme.Hom.isOver_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S] {f : X ⟶ Y},
  AlgebraicGeometry.Scheme.Hom.IsOver f S ↔ CategoryTheory.CategoryStruct.comp f (Y ↘ S) = X ↘ S
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_span_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (s : Set M), Module.rank R ↥(Submodule.span R s) ≤ Cardinal.mk ↑s
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.hom_comp : ∀ {X Y Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z},
  CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g) = MonoidWithZeroHom.comp g f
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.mk.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} {app : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y}
  {naturality :
    autoParam
      (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
        CategoryTheory.CategoryStruct.comp (P.map f g) (app X' Y) =
          CategoryTheory.CategoryStruct.comp (app X Y') (Q.map f g))
      CategoryTheory.ProfunctorCore.Hom.naturality._autoParam}
  {app_1 : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y}
  {naturality_1 :
    autoParam
      (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
        CategoryTheory.CategoryStruct.comp (P.map f g) (app_1 X' Y) =
          CategoryTheory.CategoryStruct.comp (app_1 X Y') (Q.map f g))
      CategoryTheory.ProfunctorCore.Hom.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.ediam_eq_two : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ} [Nontrivial V],
  G.IsSRGWith n k ℓ μ → G ≠ ⊤ → μ ≠ 0 → G.ediam = 2
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.lift.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [inst_2 : Nonempty J] {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)),
  CategoryTheory.Limits.wideEqualizer.lift k h = CategoryTheory.Limits.wideEqualizer.lift k_1 ⋯
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.epi_map : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₃' : ι}
  (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₃' : i₂ ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃') (n₀ n₁ n₂ n₃ : ℤ),
  autoParam (α.app 0 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 0))
      CategoryTheory.Abelian.SpectralObject.epi_map._auto_1 →
    autoParam (α.app 1 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 1))
        CategoryTheory.Abelian.SpectralObject.epi_map._auto_3 →
      autoParam (α.app 2 = CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 2))
          CategoryTheory.Abelian.SpectralObject.epi_map._auto_5 →
        ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.epi_map._auto_7)
          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.epi_map._auto_9),
          autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.epi_map._auto_11 →
            CategoryTheory.Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃' α n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Data.Set.Basic
Set.sep_eq_self_iff_mem_true : ∀ {α : Type u} {s : Set α} {p : α → Prop}, {x | x ∈ s ∧ p x} = s ↔ ∀ x ∈ s, p x
-- Std.Internal.Do.PredTrans
/-- `MonadReaderOf` instance: `read` provides the state without consuming it.  -/
Std.Internal.Do.instMonadReaderOfPredTransForall : {σ : Type u} → {Pred : Type v} → {EPred : Type w} → MonadReaderOf σ (Std.Internal.Do.PredTrans (σ → Pred) EPred)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The affine span of the orthocenter and a vertex is contained in
the altitude.  -/
Affine.Triangle.affineSpan_orthocenter_point_le_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (i : Fin 3),
  line[ℝ, t.orthocenter, t.points i] ≤ Affine.Simplex.altitude t i
-- Mathlib.RingTheory.TensorProduct.Basic
/-- If `M` is an `R`-module and `N` is an `A`-module, then `A`-linear maps `A ⊗[R] M →ₗ[A] N`
correspond to `R` linear maps `M →ₗ[R] N` by composing with `M → A ⊗ M`, `x ↦ 1 ⊗ x`.
 -/
LinearMap.liftBaseChangeEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      (A : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module A N] →
                        [inst_8 : IsScalarTower R A N] → (M →ₗ[R] N) ≃ₗ[A] TensorProduct R A M →ₗ[A] N
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.mkAppRevRangeAux : Array Lean.Expr → ℕ → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A subrepresentation is a representation.  -/
Subrepresentation.toRepresentation : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] →
              {ρ : Representation A G W} → (ρ' : Subrepresentation ρ) → Representation A G ↥ρ'.toSubmodule
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.coe_zero : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), { toCompletion := ↑(WithAbs.toAbs (↑v) 0) } = 0
-- Mathlib.Order.Filter.Defs
/-- Override `sets` field of a filter to provide better definitional equality.  -/
Filter.copy : {α : Type u_1} → (f : Filter α) → (S : Set (Set α)) → (∀ (s : Set α), s ∈ S ↔ s ∈ f) → Filter α
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_sum_mul_range_of_summable_mul : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α]
  [IsTopologicalSemiring α],
  (Summable fun x => f x.1 * g x.2) → Summable fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
-- Mathlib.Data.Sym.Sym2
Sym2.fromRelNdrec.congr_simp : ∀ {α : Type u_1} {r : α → α → Prop} {motive : Sort u_4} {sym : Std.Symm r} (z z_1 : Sym2 α) (e_z : z = z_1)
  (hz : z ∈ Sym2.fromRel sym) (f f_1 : (a b : α) → r a b → motive) (e_f : f = f_1)
  (h : ∀ (a b : α) (h : r a b), f a b h = f b a ⋯), Sym2.fromRelNdrec z hz f h = Sym2.fromRelNdrec z_1 ⋯ f_1 ⋯
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- Type synonym, introduced to put a different `SMul` action on `C^n⟮I, M; 𝕜⟯`
which is defined as `f • r = f(x) * r`.
Denoted as `C^n⟮I, M; 𝕜⟯⟨x⟩` within the `Derivation` namespace.  -/
PointedContMDiffMap : (𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                (M : Type u_4) →
                  [inst : TopologicalSpace M] → [ChartedSpace H M] → WithTop ℕ∞ → M → Type (max 0 u_4 u_1)