mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.add_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α},
  ν₁.MutuallySingular μ → ν₂.MutuallySingular μ → (ν₁ + ν₂).MutuallySingular μ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.Quotient.group.eq_1 : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal],
  QuotientGroup.Quotient.group N =
    { mul := Quotient.map₂ (fun x1 x2 => x1 * x2) ⋯, mul_assoc := ⋯, one := Quotient.mk'' 1, one_mul := ⋯, mul_one := ⋯,
      npow := QuotientGroup.Quotient.group._aux_4 N, npow_zero := ⋯, npow_succ := ⋯, inv := Quotient.map' Inv.inv ⋯,
      div := Quotient.map₂ (fun x1 x2 => x1 / x2) ⋯, zpow := QuotientGroup.Quotient.group._aux_8 N, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {km : α}, t.max? = some km → t.get! km = km
-- Mathlib.Analysis.Convex.Basic
convex_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E], Convex 𝕜 Set.univ
-- Mathlib.Analysis.Analytic.Basic
analyticOnNhd_congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  f =ᶠ[nhdsSet s] g → (AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  IsZLattice ℝ (NumberField.mixedEmbedding.idealLattice K I)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} → (toFun : G → E) → Function.RightInverse toFun ⇑S.rightHom → S.Section
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectBottomUps : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.equivRange_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (x : M), ↑(f.equivRange x) = f x
-- Init.Data.String.Basic
String.sliceTo.eq_1 : ∀ (s : String) (p : s.Pos), s.sliceTo p = s.toSlice.sliceTo p.toSlice
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
isInvertible_mfderiv_extChartAt : ∀ {𝕜 : 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] [IsManifold I 1 M] {x y : M},
  y ∈ (extChartAt I x).source → (mfderiv% ↑(extChartAt I x) y).IsInvertible
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.noConfusionType : Sort v✝ → Lean.Compiler.InlineAttributeKind → Lean.Compiler.InlineAttributeKind → Sort v✝
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n` is integrable for all `n : ℕ`.  -/
ProbabilityTheory.integrable_pow_abs_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) → ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => |X ω| ^ n) μ
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.linearIndependentEmpty : ∀ {I : Type u_1} [inst : LinearOrder I], LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval ∅)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M),
  (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source
-- Lean.Parser.Term
/-- `have` is used to declare local hypotheses and opaque local definitions.

It has the same syntax as `let`, and it is equivalent to `let +nondep`,
creating a *nondependent* let expression.
 -/
Lean.Parser.Term.have : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.mk.inj : ∀ {id structId : ℕ} {type : Lean.Expr} {u : Lean.Level} {natModuleInst : Lean.Expr}
  {leInst? ltInst? lawfulOrderLTInst? isPreorderInst? orderedAddInst? isLinearInst? addRightCancelInst? :
    Option Lean.Expr}
  {rfl_q zero toQFn addFn smulFn : Lean.Expr} {termMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)}
  {id_1 structId_1 : ℕ} {type_1 : Lean.Expr} {u_1 : Lean.Level} {natModuleInst_1 : Lean.Expr}
  {leInst?_1 ltInst?_1 lawfulOrderLTInst?_1 isPreorderInst?_1 orderedAddInst?_1 isLinearInst?_1 addRightCancelInst?_1 :
    Option Lean.Expr}
  {rfl_q_1 zero_1 toQFn_1 addFn_1 smulFn_1 : Lean.Expr}
  {termMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)},
  { id := id, structId := structId, type := type, u := u, natModuleInst := natModuleInst, leInst? := leInst?,
        ltInst? := ltInst?, lawfulOrderLTInst? := lawfulOrderLTInst?, isPreorderInst? := isPreorderInst?,
        orderedAddInst? := orderedAddInst?, isLinearInst? := isLinearInst?, addRightCancelInst? := addRightCancelInst?,
        rfl_q := rfl_q, zero := zero, toQFn := toQFn, addFn := addFn, smulFn := smulFn, termMap := termMap } =
      { id := id_1, structId := structId_1, type := type_1, u := u_1, natModuleInst := natModuleInst_1,
        leInst? := leInst?_1, ltInst? := ltInst?_1, lawfulOrderLTInst? := lawfulOrderLTInst?_1,
        isPreorderInst? := isPreorderInst?_1, orderedAddInst? := orderedAddInst?_1, isLinearInst? := isLinearInst?_1,
        addRightCancelInst? := addRightCancelInst?_1, rfl_q := rfl_q_1, zero := zero_1, toQFn := toQFn_1,
        addFn := addFn_1, smulFn := smulFn_1, termMap := termMap_1 } →
    id = id_1 ∧
      structId = structId_1 ∧
        type = type_1 ∧
          u = u_1 ∧
            natModuleInst = natModuleInst_1 ∧
              leInst? = leInst?_1 ∧
                ltInst? = ltInst?_1 ∧
                  lawfulOrderLTInst? = lawfulOrderLTInst?_1 ∧
                    isPreorderInst? = isPreorderInst?_1 ∧
                      orderedAddInst? = orderedAddInst?_1 ∧
                        isLinearInst? = isLinearInst?_1 ∧
                          addRightCancelInst? = addRightCancelInst?_1 ∧
                            rfl_q = rfl_q_1 ∧
                              zero = zero_1 ∧
                                toQFn = toQFn_1 ∧ addFn = addFn_1 ∧ smulFn = smulFn_1 ∧ termMap = termMap_1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- An Eisenstein series of weight `k` and level `Γ(N)`, with congruence condition `a`.  -/
eisensteinSeries : {N : ℕ} → (Fin 2 → ZMod N) → ℤ → UpperHalfPlane → ℂ
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_pow : ∀ {p : ℝ}, 0 ≤ p → ∀ (n : ℕ), ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mem_univ_Ioc : ∀ {ι : Type u_1} {x : ι → ℝ} {I : BoxIntegral.Box ι}, (x ∈ Set.univ.pi fun i => Set.Ioc (I.lower i) (I.upper i)) ↔ x ∈ I
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.instIsIsoPullbackObjUnitToUnitOfFinal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [F.Final],
  CategoryTheory.IsIso (SheafOfModules.pullbackObjUnitToUnit φ)
-- Mathlib.Order.InitialSeg
InitialSeg.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : InitialSeg r s) (g : InitialSeg s t) (a : α), (f.trans g) a = g (f a)
-- Mathlib.Topology.MetricSpace.Cauchy
/-- If the distance between `s n` and `s m`, `n ≤ m` is bounded above by `b n`
and `b` converges to zero, then `s` is a Cauchy sequence.  -/
cauchySeq_of_le_tendsto_0' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {s : β → α}
  (b : β → ℝ), (∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n) → Filter.Tendsto b Filter.atTop (nhds 0) → CauchySeq s
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.cancelBaseChange.congr_simp : ∀ (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : Algebra A B] [inst_15 : IsScalarTower A B M],
  TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N =
    TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t) \ s = t \ s
-- Mathlib.Data.Stream.Defs
/-- Append a stream to a list.  -/
Stream'.appendStream' : {α : Type u} → List α → Stream' α → Stream' α
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCocones_pt_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂),
  (CategoryTheory.Limits.combineCocones F c).pt.map f =
    (c k₁).isColimit.desc
      { pt := (c k₂).cocone.pt, ι := CategoryTheory.CategoryStruct.comp (F.flip.map f) (c k₂).cocone.ι }
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_sSup : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] (s : Set G.Finsubgraph), ↑(sSup s) = ⨆ G_1 ∈ s, ↑G_1
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coe_id : ∀ {M : Type u_10} [inst : AddZero M], ⇑(AddMonoidHom.id M) = id
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.fst R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom) h
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.forall_coeff_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), (∀ (n : ℕ), (PowerSeries.coeff n) φ = 0) ↔ φ = 0
-- Mathlib.Data.Nat.Factors
Nat.replicate_subperm_primeFactorsList_iff : ∀ {a b n : ℕ}, Nat.Prime a → b ≠ 0 → ((List.replicate n a).Subperm b.primeFactorsList ↔ a ^ n ∣ b)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.of.eq_1 : ∀ {α : Type u} (x : α), FreeGroup.of x = FreeGroup.mk [(x, true)]
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The target of the equalizer diagram for `f`.  -/
CategoryTheory.IsRegularMono.Z : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsRegularMono f] → C
-- Mathlib.Analysis.Quaternion
/-- Coercion from `ℂ` to `ℍ`.  -/
Quaternion.coeComplex : ℂ → Quaternion ℝ
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`.
Then `f` can be written in the form `(∏ i ∈ s, g i) * (q + ∑ i ∈ s, r i / g i)`, where
`degree (r i) < degree (g i)` and the denominator cancels formally.
See `quo_mul_prod_add_sum_rem_mul_prod_unique` for the uniqueness of this representation.  -/
Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prod : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R] {ι : Type u_2} [inst_2 : DecidableEq ι] {s : Finset ι}
  (f : Polynomial R) {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The interchange law for horizontal and vertical composition of 2-cells in a bicategory.  -/
CategoryTheory.CatEnrichedOrdinary.hComp_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃) (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.hComp η θ)
      (CategoryTheory.CatEnrichedOrdinary.hComp η' θ') =
    CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CategoryStruct.comp η η')
      (CategoryTheory.CategoryStruct.comp θ θ')
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkTailWs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.GDelta.MetrizableSpace
instT4SpaceOfMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.MetrizableSpace X], T4Space X
-- Std.Data.TreeSet.Raw.Basic
/-- Well-formedness predicate for tree sets. Users of `TreeSet` will not need to interact with
this. Users of `TreeSet.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas
like `WF.empty` and `WF.insert` (which are always named exactly like the operations they are about)
to show that set operations preserve well-formedness. The constructors of this type are internal
implementation details and should not be accessed by users.
 -/
Std.TreeSet.Raw.WF : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Prop
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.mk.injEq : ∀ (lhs rhs : Lean.Expr) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (lhs_1 rhs_1 : Lean.Expr)
  (lctx_1 : Lean.LocalContext) (localInstances_1 : Lean.LocalInstances),
  ({ lhs := lhs, rhs := rhs, lctx := lctx, localInstances := localInstances } =
      { lhs := lhs_1, rhs := rhs_1, lctx := lctx_1, localInstances := localInstances_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ lctx = lctx_1 ∧ localInstances = localInstances_1)
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.mk_div_mk : ∀ {M : Type u_1} [inst : CommMonoid M] (m₁ m₂ : M) (s₁ s₂ : ↥⊤),
  Localization.mk m₁ s₁ / Localization.mk m₂ s₂ = Localization.mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  RootPairing.EmbeddedG2.threeShortAddTwoLongRoot P =
    3 • RootPairing.EmbeddedG2.shortRoot P + 2 • RootPairing.EmbeddedG2.longRoot P
-- Mathlib.Algebra.Group.Basic
mul_zpow_neg_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instContainsZeroIsInjectiveOfHasZeroMorphismsOfHasZeroObject : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C], (CategoryTheory.isInjective C).ContainsZero
-- Mathlib.CategoryTheory.Filtered.Final
/-- Any under category on a filtered or empty category is filtered.
(Note that under categories are always cofiltered since they have an initial object.)  -/
CategoryTheory.IsFiltered.under : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C),
  CategoryTheory.IsFiltered (CategoryTheory.Under c)
-- Mathlib.Data.Sym.Sym2
Sym2.lift_comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }),
  Sym2.lift f ∘ Sym2.map g = Sym2.lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩
-- Mathlib.Order.NonemptyFiniteChains
/-- The functor `PartOrd ⥤ PartOrd` which sends a partially ordered type `X`
to `NonemptyFiniteChains X`.  -/
PartOrd.nonemptyFiniteChainsFunctor : CategoryTheory.Functor PartOrd PartOrd
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_one : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ), Polynomial.homogenize 1 n = MvPolynomial.X 1 ^ n
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) (X : C), F.leftOpRightOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Combinatorics.SimpleGraph.Clique
_private.Mathlib.Combinatorics.SimpleGraph.Clique.0.SimpleGraph.finite_cliqueNum_bddAbove : ∀ {α : Type u_3} {G : SimpleGraph α} [Finite α], BddAbove {n | ∃ s, G.IsNClique n s}
-- Mathlib.LinearAlgebra.LinearPMap
/-- Define a `LinearMap` from its graph.

Helper definition for `LinearPMap`.  -/
Submodule.toLinearPMapAux : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module R F] →
                (g : Submodule R (E × F)) →
                  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → ↥(Submodule.map (LinearMap.fst R E F) g) →ₗ[R] F
-- Mathlib.Order.CompleteLattice.Lemmas
/-- This is a weaker version of `sInf_sup_eq`  -/
sInf_sup_le_iInf_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.coeffs = Finset.image (fun n => p.coeff n) p.support
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprAuthority.repr : Std.Http.URI.Authority → ℕ → Std.Format
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffWithinAt_extChartAt_symm_range : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (x : M) {y : E},
  y ∈ (extChartAt I x).target →
    ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (Set.range ↑I) y
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sieve₀_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀),
  E.sieve₀.arrows (E.f i)
-- Mathlib.Algebra.Group.Defs
DivisionMonoid.mul_inv_rev : ∀ {G : Type u} [self : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct a morphism between categorical coproducts (indexed by the same type)
from a family of morphisms between the factors.
 -/
CategoryTheory.Limits.Sigma.map : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : β → C} →
        [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct g] → ((b : β) → f b ⟶ g b) → (∐ f ⟶ ∐ g)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasCokernel f]
  [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_12 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_13 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))]
  [inst_14 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom
      (CategoryTheory.Abelian.coimageImageComparison (F.map f)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimageImageComparison f))
      (CategoryTheory.Abelian.PreservesImage.iso F f).hom
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_apply₀ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    ∀ {s : Set β},
      MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ) →
        (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPushout_of_right_factors_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (h : W ⟶ X) [CategoryTheory.Epi h],
  CategoryTheory.Limits.HasPushout h (CategoryTheory.CategoryStruct.comp h f)
-- Mathlib.Topology.Algebra.AffineSubspace
/-- A continuous affine equivalence restricts to a continuous affine equivalence between an affine
subspace and its image.

This is the continuous affine version of `AffineEquiv.affineSubspaceMap`.  -/
ContinuousAffineEquiv.affineSubspaceMap : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      {W : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] →
                          [inst_8 : AddTorsor W Q] →
                            (e : P ≃ᴬ[R] Q) →
                              (s : AffineSubspace R P) → [inst_9 : Nonempty ↥s] → ↥s ≃ᴬ[R] ↥(AffineSubspace.map (↑↑e) s)