mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.Request
/-- Sets the request target/URI for the request being built.
 -/
Std.Http.Request.Builder.uri : Std.Http.Request.Builder → Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Algebra.Group.AddChar
/-- An additive character maps sums to products.  -/
AddChar.map_add_eq_mul : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (x y : A),
  ψ (x + y) = ψ x * ψ y
-- Batteries.Data.HashMap.Basic
/-- Looks up an element in the map with key `a`. Panics if the element is not found.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find! "one" = 1
hashMap.find! "three" => panic!
```
 -/
Batteries.HashMap.find! : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → [Inhabited β] → Batteries.HashMap α β → α → β
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ), p.coeff n = p.coeff (Multiplicative.ofAdd n)
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.part.sizeOf_spec : sizeOf Mathlib.Tactic.Order.OrderType.part = 1
-- Init.Guard
/-- Default-reducibility defeq matching for `guard_hyp` types  -/
Lean.Parser.colonD : Lean.ParserDescr
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A `PreconnectedSpace` version of `isPreconnected.constant`  -/
PreconnectedSpace.constant : ∀ {α : Type u} [inst : TopologicalSpace α] {Y : Type u_3} [inst_1 : TopologicalSpace Y] [DiscreteTopology Y],
  PreconnectedSpace α → ∀ {f : α → Y}, Continuous f → ∀ {x y : α}, f x = f y
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- If `z` is a non-real complex root of a real polynomial,
then `p` is divisible by a quadratic polynomial.  -/
Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero : ∀ (p : Polynomial ℝ) {z : ℂ},
  (Polynomial.aeval z) p = 0 →
    z.im ≠ 0 → Polynomial.X ^ 2 - Polynomial.C (2 * z.re) * Polynomial.X + Polynomial.C (‖z‖ ^ 2) ∣ p
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalWithImplicit : Lean.Elab.Tactic.Tactic
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : AddMonoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : AddMonoid G'] (toAddMonoidHom : G →+ G')
  (contMDiff_toFun : ContMDiff I I' n (↑toAddMonoidHom).toFun) (toAddMonoidHom_1 : G →+ G')
  (contMDiff_toFun_1 : ContMDiff I I' n (↑toAddMonoidHom_1).toFun),
  ({ toAddMonoidHom := toAddMonoidHom, contMDiff_toFun := contMDiff_toFun } =
      { toAddMonoidHom := toAddMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 }) =
    (toAddMonoidHom = toAddMonoidHom_1)
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformlyOn.inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
-- Mathlib.Topology.Bases
TopologicalSpace.isOpen_sUnion_countable : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] (S : Set (Set α)),
  (∀ s ∈ S, IsOpen s) → ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientKerEquivOfSurjective.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (hφ : Function.Surjective ⇑φ),
  QuotientGroup.quotientKerEquivOfSurjective φ hφ = QuotientGroup.quotientKerEquivOfRightInverse φ (Exists.choose ⋯) ⋯
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.StrictMono.liftRingHom.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f f_1 : (n : ℕ) → R →+* S ⧸ I ^ a n) (e_f : f = f_1)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S],
  IsAdicComplete.StrictMono.liftRingHom I ha f hf = IsAdicComplete.StrictMono.liftRingHom I ha f_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_ι : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).ι = F.map h.ι
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.subst_add : ∀ {M : Type u_1} [inst : Semiring M] {x₁ x₂ X₁ X₂ Y y a : M},
  x₁ = a * X₁ → x₂ = a * X₂ → X₁ + X₂ = Y → a * Y = y → x₁ + x₂ = y
-- Mathlib.Order.Lex
ofColex_symm_eq : ∀ {α : Type u_1}, ofColex.symm = toColex
-- Lean.Namespace
/-- Register a new namespace in the environment.  -/
Lean.Environment.registerNamespace : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.RingTheory.Localization.Algebra
/-- Less linear version of `mapExtendScalars_eq_toLinearMap_mapₐ`.
For a version where `R = A`, see `map_linearMap_eq_toLinearMap_mapₐ`.  -/
IsLocalization.map_eq_toLinearMap_mapₐ : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B),
  (IsLocalizedModule.map M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap (IsScalarTower.toAlgHom R B Bₚ).toLinearMap)
      f.toLinearMap =
    ↑R (IsLocalization.mapₐ M Rₚ Aₚ Bₚ f).toLinearMap
-- Aesop.Builder.Forward
Aesop.RuleBuilder.getImmediatePremises : Lean.Expr →
  Option Aesop.RulePattern → Option (Array Lean.Name) → Lean.MetaM (Aesop.UnorderedArraySet Aesop.PremiseIndex)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.smul_cons : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ g₂ : G)
  (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  g₁ • HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_strict_mono : ∀ {α : Type u_1} {f g : α → NNReal}, Summable g → f < g → ∑' (n : α), f n < ∑' (n : α), g n
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft (HomotopicalAlgebra.LeftHomotopyClass.mk f) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.BifibrantObject.homMk f)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.of_comp_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ}, IsUniformInducing g → ∀ {f : α → β}, IsUniformInducing (g ∘ f) ↔ IsUniformInducing f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_insert!_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).toArray.Perm
        ((Array.filter (fun x => decide ¬(k == x.fst) = true) t.toArray).push ⟨k, v⟩)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.mk.sizeOf_spec : ∀ (toTopCat : TopCat) [is_alexandrovDiscrete : AlexandrovDiscrete ↑toTopCat],
  sizeOf { toTopCat := toTopCat, is_alexandrovDiscrete := is_alexandrovDiscrete } =
    1 + sizeOf toTopCat + sizeOf is_alexandrovDiscrete
-- Lean.Parser.Term
Lean.Parser.Term.letOptUsedOnly.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Star.StarProjection
/-- The product of star projections is a star projection if they commute.  -/
IsStarProjection.mul : ∀ {R : Type u_1} {p q : R} [inst : NonUnitalSemiring R] [inst_1 : StarRing R],
  IsStarProjection p → IsStarProjection q → Commute p q → IsStarProjection (p * q)
-- Std.Http.Test.Helpers
/-- Respond 200 with the request URI as the body.
 -/
Std.Http.Internal.Test.uriHandler : Std.Http.Internal.Test.TestHandler
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).π = CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.Order.Hom.Basic
OrderIso.lt_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {x : α} {y : β},
  x < e.symm y ↔ e x < y
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series is differentiable on the set and its derivative is the sum of the
derivatives.  -/
hasDerivAt_tsum_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F}
  {t : Set 𝕜} {y₀ y : 𝕜},
  Summable u →
    IsOpen t →
      IsPreconnected t →
        (∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) →
          (∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) →
            y₀ ∈ t → (Summable fun n => g n y₀) → y ∈ t → HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
-- Mathlib.Logic.Relation
Relation.symmGen_of_total : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α), Relation.SymmGen r a b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], (m₁ ∪ m₂)[k]! = m₂.getD k m₁[k]!
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_bot_eq : ∀ {V : Type u} {u v : V}, ⊥.commonNeighbors u v = ∅
-- Mathlib.Topology.Algebra.GroupCompletion
instSubCompletion : {α : Type u_3} → [inst : UniformSpace α] → [Sub α] → Sub (UniformSpace.Completion α)
-- Mathlib.Order.Category.Preord
Preord.hom_comp : ∀ {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z),
  Preord.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Preord.Hom.hom g).comp (Preord.Hom.hom f)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ} [inst_3 : Group X]
  [IsIsometricSMul Xᵐᵒᵖ X], (MeasureTheory.Measure.hausdorffMeasure d).IsMulRightInvariant
-- Mathlib.CategoryTheory.CommSq
/-- A choice of a diagonal morphism that is part of a `LiftStruct` when
the square has a lift.  -/
CategoryTheory.CommSq.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → (sq : CategoryTheory.CommSq f i p g) → [hsq : sq.HasLift] → B ⟶ X
-- Mathlib.Algebra.Quaternion
Quaternion.algebra : {S : Type u_1} →
  {R : Type u_3} → [inst : CommRing R] → [inst_1 : CommSemiring S] → [Algebra S R] → Algebra S (Quaternion R)
-- Mathlib.Algebra.Star.Pointwise
Set.star_empty : ∀ {α : Type u_1} [inst : Star α], star ∅ = ∅
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.of_simple_quotient : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  [IsSimpleModule R (M ⧸ N)], IsFiniteLength R ↥N → IsFiniteLength R M
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.coe_addEquiv : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V], ⇑(WithLp.addEquiv p V) = WithLp.ofLp
-- Init.Core
/-- Heterogeneous equality with an `Eq.rec` application on the right is equivalent to a heterogeneous
equality on the original term.
 -/
heq_eqRec_iff : ∀ {β : Sort v} {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v} {b : α} {refl : motive a ⋯} {h : a = b} {c : β},
  c ≍ h ▸ refl ↔ c ≍ refl
-- Lean.Meta.Tactic.Grind.EMatch
/-- Maximum term generation found so far.  -/
Lean.Meta.Grind.EMatch.Choice.gen : Lean.Meta.Grind.EMatch.Choice → ℕ
-- Std.Sat.AIG.CNF
/-- Cache extension is a reflexive relation.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy_rfl : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} {idx : ℕ} {omega : idx < aig.decls.size}
  (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf) {h : idx < (Std.Sat.AIG.toCNF.Cache.marks✝ cache).size},
  (Std.Sat.AIG.toCNF.Cache.marks✝ cache)[idx] = true → Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache cache idx ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.brecOn.eq : ∀ {motive : (a : ℕ) → Std.Tactic.BVDecide.BVExpr a → Sort u} {a : ℕ} (t : Std.Tactic.BVDecide.BVExpr a)
  (F_1 : (a : ℕ) → (t : Std.Tactic.BVDecide.BVExpr a) → Std.Tactic.BVDecide.BVExpr.below t → motive a t),
  Std.Tactic.BVDecide.BVExpr.brecOn t F_1 = F_1 a t (Std.Tactic.BVDecide.BVExpr.brecOn.go t F_1).2
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.IterM.take.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (n : ℕ) (it : Std.IterM m β),
  Std.IterM.take n it = { internalState := { countdown := n + 1, inner := it, finite := ⋯ } }
-- Mathlib.FieldTheory.SeparableDegree
/-- **Alias** of `Field.finSepDegree_eq_finrank_of_isSeparable`.

---

If `E / F` is a separable extension, then its separable degree is equal to its degree.
When `E / F` is infinite, it means that `Field.Emb F E` has infinitely many elements.
(But the cardinality of `Field.Emb F E` is not equal to `Module.rank F E` in general!)  -/
Field.Algebra.IsSeparable.finSepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Field.finSepDegree F E = Module.finrank F E
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.universally_isZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
      TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f) →
    AlgebraicGeometry.IsZariskiLocalAtTarget P.universally
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey! =
        t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_surjective : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (X.residue x))
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneraciesVanishPInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.DoldKan.DegeneraciesVanish (AlgebraicTopology.DoldKan.PInfty.f n)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of 0-morphism we can define an inclusion morphism into any product.  -/
CategoryTheory.Limits.Pi.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      {β : Type w} →
        [DecidableEq β] → (f : β → C) → [inst_3 : CategoryTheory.Limits.HasProduct f] → (b : β) → f b ⟶ ∏ᶜ f
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic'_source : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), (stereographic' n v).source = {v}ᶜ
-- Mathlib.RingTheory.DedekindDomain.Instances
FractionRing.isSeparable_of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_5 : CommRing Rₘ] [inst_6 : CommRing Sₘ]
  [inst_7 : Algebra R Rₘ] [inst_8 : Module.IsTorsionFree R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
  {M : Submonoid R} [IsLocalization M Rₘ] [inst_11 : Algebra Rₘ Sₘ] [inst_12 : Algebra S Sₘ] [inst_13 : Algebra R Sₘ]
  [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  [inst_17 : Algebra (FractionRing Rₘ) (FractionRing Sₘ)] [IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)],
  M ≤ nonZeroDivisors R → Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
-- Mathlib.Analysis.Analytic.Constructions
alternatingGeometricSeries_eq_formalMultilinearSeries_geometric_comp_neg : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A],
  alternatingGeometricSeries 𝕜 A =
    (formalMultilinearSeries_geometric 𝕜 A).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 A)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.NatTrans.IsMonoidal.of_cartesianMonoidalCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F G : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] [inst_5 : G.Monoidal] (α : F ⟶ G),
  CategoryTheory.NatTrans.IsMonoidal α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.map f it)).toArray = (Std.IterM.mapM (fun b => g (f b)) it).toArray
-- Aesop.Util.Basic
Aesop.compareArrayLex : {α : Type u_1} → (α → α → Ordering) → Array α → Array α → Ordering
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : CategoryTheory.Bicategory.Adj B),
  CategoryTheory.Bicategory.Adj.forget₁.obj a = a.obj
-- Mathlib.Data.Finset.Basic
/-- The type of dependent functions on the disjoint union of finsets `s ∪ t` is equivalent to the
type of pairs of functions on `s` and on `t`. This is similar to `Equiv.sumPiEquivProdPi`.  -/
Equiv.piFinsetUnion : {ι : Type u_5} →
  [inst : DecidableEq ι] →
    (α : ι → Type u_4) →
      {s t : Finset ι} → Disjoint s t → ((i : ↥s) → α ↑i) × ((i : ↥t) → α ↑i) ≃ ((i : ↥(s ∪ t)) → α ↑i)
-- Mathlib.Data.Set.Card
Set.encard_eq_four : ∀ {α : Type u_1} {s : Set α}, s.encard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
-- Mathlib.Data.List.Sort
/-- The list obtained from a monotone tuple is sorted.  -/
List.SortedLE.monotone : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedLE → Monotone f
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_self_neg : ∀ (n : ℕ), (ascPochhammer ℕ n).smeval (-↑n) = (-1) ^ n * ↑n.factorial
-- Mathlib.GroupTheory.IsSubnormal
/-- A proper subnormal subgroup is contained in a proper normal subgroup.  -/
Subgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsSubnormal → H ≠ ⊤ → ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instHomeomorphClass : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N], HomeomorphClass (M ≃ₜ* N) M N
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ : ∀ {Ω : Type u_1} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : CommMonoid β] [MeasurableMul₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.CondIndepFun m' hm' (∏ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Interpreting the legs of a cone as a structured arrow and then forgetting the arrow again does
nothing.  -/
CategoryTheory.Limits.Cone.toStructuredArrowCompProj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) ≅ CategoryTheory.Functor.id J
-- Mathlib.Data.Nat.ModEq
/-- A natural number is odd iff it has residue `1` or `3` mod `4`.  -/
Nat.odd_mod_four_iff : ∀ {n : ℕ}, n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3
-- Mathlib.Data.Finset.DenselyOrdered
Set.Finite.exists_between' : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] [NoMaxOrder α] [NoMinOrder α] [Nonempty α] {s t : Set α},
  s.Finite → t.Finite → (∀ x ∈ s, ∀ y ∈ t, x < y) → ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.mk.inj : ∀ {J : Type u} {inst : CategoryTheory.Category.{v, u} J} {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  {desc : (c' : F.CoconeTypes) → c.pt → c'.pt}
  {fac :
    autoParam (∀ (c' : F.CoconeTypes) (j : J), desc c' ∘ c.ι j = c'.ι j)
      CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam}
  {funext : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g}
  {desc_1 : (c' : F.CoconeTypes) → c.pt → c'.pt}
  {fac_1 :
    autoParam (∀ (c' : F.CoconeTypes) (j : J), desc_1 c' ∘ c.ι j = c'.ι j)
      CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam}
  {funext_1 : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g},
  { desc := desc, fac := fac, funext := funext } = { desc := desc_1, fac := fac_1, funext := funext_1 } → desc = desc_1