mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι)
  {Z : D} (h : F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.π (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i) h) =
    CategoryTheory.CategoryStruct.comp
      (F.map
        (CategoryTheory.CategoryStruct.comp M.isoBiproductEmbedding.hom
          (CategoryTheory.Limits.biproduct.π (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i)))
      h
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Error.other.injEq : ∀ (s s_1 : String), (Std.Internal.Parsec.Error.other s = Std.Internal.Parsec.Error.other s_1) = (s = s_1)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integrable_exp_mul_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (t : ℝ),
  MeasureTheory.Integrable (fun x => Real.exp (t * x)) (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.Data.Int.Cast.Lemmas
/-- If two `MonoidHom`s agree on `-1` and the naturals then they are equal.  -/
MonoidHom.ext_int : ∀ {M : Type u_5} [inst : Monoid M] {f g : ℤ →* M}, f (-1) = g (-1) → f.comp ↑Int.ofNatHom = g.comp ↑Int.ofNatHom → f = g
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app._auto_1),
  (CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app
          (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X))))
        ((CategoryTheory.shiftFunctor Cᵒᵖ m).map
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X)))
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.IsAssociatedPrime.eq_radical_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R}, N.IsAssociatedPrime I → ∃ x, I = (N.colon {x}).radical
-- Mathlib.Topology.Separation.Regular
/-- **Alias** of the reverse direction of `completelyNormalSpace_iff_forall_normalSpace`.

---

A space is completely normal iff it is hereditarily normal.
 -/
CompletelyNormalSpace.of_forall_normalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), NormalSpace ↑s) → CompletelyNormalSpace X
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from monoids to types preserves all limits.  -/
MonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)
-- Mathlib.Data.Set.Image
Set.range_inl_union_range_inr : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inl ∪ Set.range Sum.inr = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCone_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F),
  B.toCone.pt = B.pt
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- Uniqueness (up to a natural isomorphism) of the left derived functor.  -/
CategoryTheory.Functor.leftDerivedUnique : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (LF' LF : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : L.comp LF ⟶ F) →
                    (α'₂ : L.comp LF' ⟶ F) →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] →
                          [LF.IsLeftDerivedFunctor α W] → [LF'.IsLeftDerivedFunctor α'₂ W] → LF ≅ LF'
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- Some basic API lemmas  -/
quadraticCharFun_eq_zero_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  quadraticCharFun F a = 0 ↔ a = 0
-- Mathlib.RingTheory.Valuation.Integers
Valuation.mem_integer_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (r : R),
  r ∈ v.integer ↔ v r ≤ 1
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The given arrow is contained in the given sieve.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.hf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (self : S.Arrow), (↑S).arrows self.f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod_zero : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A], H.mod 0 = 0
-- Mathlib.Data.Finsupp.Ext
/-- **Alias** of `Finsupp.add_closure_setOfPred_eq_single`. -/
Finsupp.add_closure_setOf_eq_single : ∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M], AddSubmonoid.closure {f | ∃ a b, f = fun₀ | a => b} = ⊤
-- Batteries.Data.HashMap.Basic
/-- The number of elements in the hash map.
```
(ofList [("one", 1), ("two", 2)]).size = 2
```
 -/
Batteries.HashMap.size : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → ℕ
-- Init.Data.Nat.Bitwise.Basic
/-- Returns `true` if the `(n+1)`th least significant bit is `1`, or `false` if it is `0`.
 -/
Nat.testBit : ℕ → ℕ → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
PartialEquiv.prod.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  e.prod e' =
    { toFun := fun p => (↑e p.1, ↑e' p.2), invFun := fun p => (↑e.symm p.1, ↑e'.symm p.2),
      source := e.source ×ˢ e'.source, target := e.target ×ˢ e'.target, map_source' := ⋯, map_target' := ⋯,
      left_inv' := ⋯, right_inv' := ⋯ }
-- Mathlib.Algebra.Group.Pi.Units
/-- **Alias** of the forward direction of `Pi.isUnit_iff`. -/
IsUnit.apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {x : (i : ι) → M i},
  IsUnit x → ∀ (i : ι), IsUnit (x i)
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro'.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionTriggerKind.noConfusionType : Sort v✝ → Lean.Lsp.CodeActionTriggerKind → Lean.Lsp.CodeActionTriggerKind → Sort v✝
-- Mathlib.Algebra.Ring.Defs
Ring.toNeg : {R : Type u} → [self : Ring R] → Neg R
-- Mathlib.LinearAlgebra.Projection
/-- Equivalence between submodules `q` such that `IsCompl p q` and linear maps `f : E →ₗ[R] p`
such that `∀ x : p, f x = x`.  -/
Submodule.isComplEquivProj : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] → (p : Submodule R E) → { q // IsCompl p q } ≃ { f // ∀ (x : ↥p), f ↑x = x }
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.induced_of_isLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit c),
  c.pt.str = ⨅ j, TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (c.π.app j))) (F.obj j).str
-- Mathlib.Data.List.Sigma
List.nodupKeys_nil : ∀ {α : Type u} {β : α → Type v}, [].NodupKeys
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `minToLeft j j'` is an arbitrary choice of morphism from `min j j'` to `j`,
whose existence is ensured by `IsCofiltered`.
 -/
CategoryTheory.IsCofiltered.minToLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] → (j j' : C) → CategoryTheory.IsCofiltered.min j j' ⟶ j
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.le_boundedBy : ∀ {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α},
  μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G : C)
  {X Y : C} (f : X ⟶ Y) (j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C).obj G).map f).app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator G j X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f))
        (CategoryTheory.MonoidalCategoryStruct.associator G j Y).inv)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).isEmpty = false →
        ((t.alter k f).maxKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors_dvd_iff_dvd_coe : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {a b : ↥(nonZeroDivisors M₀)}, a ∣ b ↔ ↑a ∣ ↑b
-- Mathlib.Order.Filter.IsBounded
Monotone.isCoboundedUnder_le_of_isCobounded : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Monotone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
-- Batteries.Linter.UnnecessarySeqFocus
/-- Gets the value of the `linter.unnecessarySeqFocus` option.  -/
Batteries.Linter.UnnecessarySeqFocus.getLinterUnnecessarySeqFocus : Lean.Linter.LinterOptions → Bool
-- Init.Data.SInt.Bitwise
Int64.toBitVec_abs : ∀ (a : Int64), a.abs.toBitVec = a.toBitVec.abs
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
/-- Simplification procedure for `#[...][n]?` for `n` a `Nat` literal.  -/
Array.reduceGetElem? : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The inclusion of polynomials into power series has dense image  -/
MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : CommSemiring R],
  DenseRange MvPolynomial.toMvPowerSeries
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The stitched together cones each project down to the original given cones (up to iso).  -/
CategoryTheory.Limits.evaluateCombinedCones : {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.LimitCone (F.flip.obj k)) →
                (k : K) →
                  ((CategoryTheory.evaluation K C).obj k).mapCone (CategoryTheory.Limits.combineCones F c) ≅ (c k).cone
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- The bilinear form bundled inside an `InvariantForm`.  -/
RootPairing.InvariantForm.form : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [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} → P.InvariantForm → LinearMap.BilinForm R M
-- Std.Http.Server.Connection
Std.Http.Server.instTypeNameRemoteAddr : TypeName Std.Http.Server.RemoteAddr
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.mem_baseSet_trivializationAt : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] (b : B), b ∈ (trivializationAt F E b).baseSet
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.equiv_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C),
  (CategoryTheory.WalkingIso.equiv F).fst = F.obj CategoryTheory.WalkingIso.zero
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their forward images.

See also `MulEquiv.comapSubgroup` which maps subgroups to their inverse images.
 -/
MulEquiv.mapSubgroup : {G : Type u_1} → [inst : Group G] → {H : Type u_6} → [inst_1 : Group H] → G ≃* H → Subgroup G ≃o Subgroup H
-- Lean.Parser.Extra
Lean.Parser.withOpen.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.iInf_adj : ∀ {ι : Sort u_1} {V : Type u_2} {a b : V} {f : ι → Digraph V}, (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toAddMonoidHom : {α : Type u_6} → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α → α →+ α
-- Init.Data.BitVec.Basic
BitVec.instPowNat : {n : ℕ} → Pow (BitVec n) ℕ
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.measurePreserving_subtype_coe : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μa : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    MeasureTheory.MeasurePreserving Subtype.val (MeasureTheory.Measure.comap Subtype.val μa) (μa.restrict s)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_div_left : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a / x) '' t = (fun x => x⁻¹ * a) ⁻¹' t
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.toPiLocalization_not_surjective_of_infinite : ∀ {ι : Type u_5} (R : ι → Type u_4) [inst : (i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] [Infinite ι],
  ¬Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))
-- Mathlib.Algebra.QuaternionBasis
/-- Two `R`-algebra morphisms from a quaternion algebra are equal if they agree on `i` and `j`.  -/
QuaternionAlgebra.hom_ext : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  ⦃f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A⦄,
  f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i →
    f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j → f = g
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_inter_ground : ∀ {α : Type u} (M : Matroid α) (X : Set α), M.cRk (X ∩ M.E) = M.cRk X
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X.eq_1 : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.X = MvPowerSeries.X ()
-- Mathlib.Algebra.QuadraticDiscriminant
/-- Roots of a quadratic equation.  -/
quadratic_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [NeZero 2] {a b c : K},
  a ≠ 0 →
    ∀ {s : K},
      discrim a b c = s * s → ∀ (x : K), a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
-- Mathlib.Order.DirectedInverseSystem
/-- An inverse system indexed by a preorder is a contravariant functor from the preorder
to another category. It is dual to `DirectedSystem`.  -/
InverseSystem : {ι : Type u_1} → [inst : Preorder ι] → {F : ι → Type u_4} → (⦃i j : ι⦄ → i ≤ j → F j → F i) → Prop
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.surjective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), Function.Surjective ⇑e
-- Init.Data.Slice.Lemmas
_private.Init.Data.Slice.Lemmas.0.Std.Slice.toArray.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toArray = (Std.Slice.Internal.iter s).toArray
-- Init.Data.Vector.Lemmas
Vector.reverse_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (Vector.replicate n a).reverse = Vector.replicate n a
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  ∑ w, (NumberField.Units.logEmbedding K) (Additive.ofMul x) w =
    -↑NumberField.Units.dirichletUnitTheorem.w₀.mult *
      Real.log (NumberField.Units.dirichletUnitTheorem.w₀ ((algebraMap (NumberField.RingOfIntegers K) K) ↑x))
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_inf_comap_of_surjective : ∀ {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.Surjective ⇑f →
    ∀ (S T : L.Substructure N),
      FirstOrder.Language.Substructure.map f
          (FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T) =
        S ⊓ T
-- Lean.Parser.Term
Lean.Parser.Termination.terminationBy?.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Function.Basic
Function.instAntisymmSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Antisymm r], Std.Antisymm (Function.swap r)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_toMultiplicative_symm_apply : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Add M] (x : MonoidAlgebra R (Multiplicative M)),
  ((AddMonoidAlgebra.toMultiplicative R M).symm x).coeff = Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  (Std.ExtDTreeMap.map f t).getD k fallback = (Option.map (f k) (t.get? k)).getD fallback
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuous_toENNReal : Continuous EReal.toENNReal
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.eq_3 : ∀ (n : ℕ), sinPoly✝ n.succ.succ = (2 * (2 * ↑n + 3)) • sinPoly✝ (n + 1) + (Polynomial.monomial 2) (-4) * sinPoly✝ n
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given `F : CofFibFactorizationQuasiIsoLE f n₀`, this is term in
`CofFibFactorizationQuasiIsoLE f n₁` with `n₀ + 1 = n₁` that is given
by the lemma `exists_next`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.next : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {f : K ⟶ L} →
          [CategoryTheory.EnoughInjectives C] →
            {n₀ : ℤ} →
              CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f n₀ →
                (n₁ : ℤ) →
                  n₀ + 1 = n₁ → CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f n₁
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Copying an image factorisation to another image factorisation with propositionally equal
`m` and `e` fields.
 -/
CategoryTheory.Limits.ImageFactorisation.copy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.ImageFactorisation f) →
          (m : F.F.I ⟶ Y) →
            (e : X ⟶ F.F.I) →
              autoParam (m = F.F.m) CategoryTheory.Limits.ImageFactorisation.copy._auto_1 →
                autoParam (e = F.F.e) CategoryTheory.Limits.ImageFactorisation.copy._auto_3 →
                  CategoryTheory.Limits.ImageFactorisation f
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.mk : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (s : Set X)
  (F : ↑s → Type u_3) [inst_2 : (x : ↑s) → TopologicalSpace (F x)] [hF : ∀ (x : ↑s), DiscreteTopology (F x)]
  (e : (x : ↑s) → Bundle.Trivialization (F x) f), (∀ (x : ↑s), ↑x ∈ (e x).baseSet) → IsCoveringMapOn f s
-- Mathlib.Data.Sum.Order
/-- `toLex` promoted to a `RelIso` between `<` relations.  -/
Sum.Lex.toLexRelIsoLT : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LT α] → [inst_1 : LT β] → (Sum.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instTopologicalSpaceSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXLaurentSeriesPkg : (K : Type u_2) → [inst : Field K] → TopologicalSpace (LaurentSeries.LaurentSeriesPkg K).space
-- Mathlib.CategoryTheory.Category.Cat
/-- The identity in the category of categories equals the identity functor.  -/
CategoryTheory.Cat.id_eq_id : ∀ (X : CategoryTheory.Cat), (CategoryTheory.CategoryStruct.id X).toFunctor = CategoryTheory.Functor.id ↑X
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.precylinder_i₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  K.precylinder.i₁ = HomologicalComplex.cylinder.ι₁ K
-- Mathlib.Data.Finset.Powerset
Finset.pairwise_disjoint_powersetCard : ∀ {α : Type u_1} (s : Finset α), Pairwise fun i j => Disjoint (Finset.powersetCard i s) (Finset.powersetCard j s)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.KernelFork f), s.π.app CategoryTheory.Limits.WalkingParallelPair.one = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_π : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.π =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Init.GrindInstances.Ring.BitVec
Lean.Grind.instIsCharPBitVecHPowNatOfNat : ∀ {w : ℕ}, Lean.Grind.IsCharP (BitVec w) (2 ^ w)
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_quotient_of_le : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided],
  I ≤ Ring.jacobson R → Ring.jacobson (R ⧸ I) = Submodule.map (Ideal.Quotient.mk I).toSemilinearMap (Ring.jacobson R)
-- Lean.Message
/-- Start time in seconds; 0 if unknown to avoid `Option` allocation.  -/
Lean.TraceData.startTime : Lean.TraceData → Float
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalAddTorsor.continuous_vsub : ∀ {V : Type u_1} {inst : AddGroup V} {inst_1 : TopologicalSpace V} {P : Type u_2} {inst_2 : AddTorsor V P}
  {inst_3 : TopologicalSpace P} [self : IsTopologicalAddTorsor P], Continuous fun x => x.1 -ᵥ x.2