mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_canonicalEquiv : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'] (P'' : Type u_5) [inst_7 : CommRing P''] [inst_8 : Algebra R P'']
  [inst_9 : IsLocalization S P''] (I : FractionalIdeal S P),
  (FractionalIdeal.canonicalEquiv S P' P'') ((FractionalIdeal.canonicalEquiv S P P') I) =
    (FractionalIdeal.canonicalEquiv S P P'') I
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [inst_3 : Q.RespectsIso]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg : autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Over.mapComp._auto_1)
  (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapComp Q hf hg fg hfg).inv.app X_1).left =
    CategoryTheory.CategoryStruct.id X_1.left
-- Std.Http.Internal.Char
Std.Http.Internal.Char.quotedPairChar.eq_1 : Std.Http.Internal.Char.quotedPairChar '\t' = (true || Std.Http.Internal.Char.vchar '\t')
-- Mathlib.Data.Seq.Defs
Stream'.Seq.terminates_cons_iff : ∀ {α : Type u} {x : α} {s : Stream'.Seq α}, (Stream'.Seq.cons x s).Terminates ↔ s.Terminates
-- Lean.Meta.HaveTelescope
Lean.Meta.ZetaUnusedMode.noConfusionType : Sort v✝ → Lean.Meta.ZetaUnusedMode → Lean.Meta.ZetaUnusedMode → Sort v✝
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.ι_def : ∀ {I : Type u_1} [inst : DecidableEq I] (R : Type u_2) [inst_1 : CommSemiring R] (A : I → Type u_3)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (i : I),
  LinearAlgebra.FreeProduct.ι R A i = AlgHom.ofLinearMap (LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i) ⋯ ⋯
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_head : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [Std.Refl R],
  List.Pairwise R l → ∀ (ha : a ∈ l), R (l.head ⋯) a
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.commutator_subset_ker : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A] (f : G →* A), commutator G ≤ f.ker
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instAdditivePresheafOfModulesObjFunctorOppositeRingCatIsSheafForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.forget R).Additive
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- A uniformizing element for the valuation `v`, as a polynomial in `K[X]`.  -/
RatFunc.uniformizingPolynomial : {K : Type u_1} →
  {Γ : Type u_2} →
    [inst : Field K] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ] →
        {v : Valuation (RatFunc K) Γ} → [v.IsNontrivial] → [Valuation.IsTrivialOn K v] → v RatFunc.X ≤ 1 → Polynomial K
-- Mathlib.Data.List.Sublists
List.sublists'_singleton : ∀ {α : Type u} (a : α), [a].sublists' = [[], [a]]
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_vecMulVec_le : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [StrongRankCondition R]
  (w : m → R) (v : n → R), (Matrix.vecMulVec w v).rank ≤ 1
-- Mathlib.Data.Real.Basic
Real.instSemilatticeInf : SemilatticeInf ℝ
-- Mathlib.Analysis.Complex.JensenFormula
/-- Analogue of the **Poisson Integral Formula** for the circle average function `log ‖· - ρ‖` along the
circle with radius `‖ρ‖`.

- See `InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul` in the file
  `Mathlib/Analysis/Complex/Harmonic/Poisson` for the classic Poisson Integral Formula, for harmonic
  functions without logarithmic poles.

- See `MeromorphicOn.extract_zeros_poles` in the file
  `Mathlib/Analysis/Meromorphic/FactorizedRational` for a construction that splits factors of the
  form `· - ρ` off arbitrary meromorphic functions.
 -/
circleAverage_re_herglotzRieszKernel_mul_log : ∀ {w ρ c : ℂ} {R : ℝ},
  ρ ∈ Metric.sphere c R →
    w ∈ Metric.ball c R →
      Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun x => Real.log ‖x - ρ‖) c R = Real.log ‖w - ρ‖
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- Exactness of `Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)`.  -/
groupHomology.mapShortComplex₃_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i), (groupHomology.mapShortComplex₃ hX hij).Exact
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.intro' : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {K : Set α},
  IsCompact K → IsClosed K → (∀ x ∉ K, f x = 0) → HasCompactSupport f
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) [inst_2 : CategoryTheory.IsAddMonHom f],
  CategoryTheory.AddGrp.homMk f = CategoryTheory.AddGrp.homMk' { hom := f, isAddMonHom_hom := inst_2 }
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  SupBotHom.instOrderBot = { bot := { toSupHom := ⊥, map_bot' := ⋯ }, bot_le := ⋯ }
-- Mathlib.RingTheory.Ideal.Operations
Submodule.map_smul'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M) {M' : Type w} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Submodule.map f (I • N) = I • Submodule.map f N
-- Init.Data.Option.Lemmas
Option.map_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {x : Option α},
  Option.map g (x.bind f) = x.bind (Option.map g ∘ f)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.π_def : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns] (x : I × I),
  TotalComplexShape.π c c c x =
    match x with
    | (p, q) => p + q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → m.get? a = none
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.coe_comp : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} {Z : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  [inst_5 : Convexity.ConvexSpace R Z] (g : Convexity.ConvexSpace.AffineMap R Y Z)
  (f : Convexity.ConvexSpace.AffineMap R X Y), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.disjoint_coe_of_mem : ∀ {ι : Type u_1} {I J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
  J₁ ∈ π → J₂ ∈ π → J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂
-- Mathlib.RingTheory.Multiplicity
multiplicity_of_unit_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, ¬IsUnit a → ∀ (u : αˣ), multiplicity a ↑u = 0
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.of_comp : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {A' : Type u_6} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  AlgebraicIndependent R (⇑f ∘ x) → AlgebraicIndependent R x
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mapₐ_surjective_of_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_6}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] {Aₚ : Type u_7} [inst_5 : CommSemiring Aₚ] [inst_6 : Algebra A Aₚ]
  [inst_7 : Algebra R Aₚ] [inst_8 : IsScalarTower R A Aₚ] {Bₚ : Type u_8} [inst_9 : CommSemiring Bₚ]
  [inst_10 : Algebra B Bₚ] [inst_11 : Algebra R Bₚ] [inst_12 : IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A)
  [inst_13 : IsLocalization.Away a Aₚ] [inst_14 : IsLocalization.Away (f a) Bₚ],
  Function.Surjective ⇑f → Function.Surjective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizePersistentExtensions.loop : Array Lean.ModuleData → Lean.Options → ℕ → Lean.Environment → IO Lean.Environment
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.categoryForgetEnrichment : {C : Type u₁} →
  (W : Type v) →
    [inst : CategoryTheory.Category.{w, v} W] →
      [inst_1 : CategoryTheory.MonoidalCategory W] →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          CategoryTheory.Category.{w, u₁} (CategoryTheory.ForgetEnrichment W C)
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.coe_range : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S), ↑f.range = Set.range ⇑f
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalizedModule.lift_rank_eq : ∀ {R : Type uR} {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
-- Mathlib.Data.List.Sort
OrderIso.sortedGT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {l : List α},
  (List.map (⇑e) l).SortedGT ↔ l.SortedGT
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.isAlgebraic_def : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.IsAlgebraic R A ↔ ∀ (x : A), IsAlgebraic R x
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.down_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : ι → ULift.{v, u_1} α), (⨅ i, f i).down = ⨅ i, (f i).down
-- Init.ShareCommon
ShareCommon.State.shareCommon : {α : Type u_1} → {σ : ShareCommon.StateFactory} → ShareCommon.State σ → α → α × ShareCommon.State σ
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of the forward direction of `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`. -/
LE.le.absolutelyContinuous_of_ae : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.ae μ ≤ MeasureTheory.ae ν → μ.AbsolutelyContinuous ν
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm_image_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → ↑e.symm '' (e.target ∩ t) = e.source ∩ s
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The residue of `Λ` at `s = 0` is equal to `-f₀`.  -/
WeakFEPair.Λ_residue_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  Filter.Tendsto (fun s => s • P.Λ s) (nhdsWithin 0 {0}ᶜ) (nhds (-P.f₀))
-- Mathlib.Data.ENat.Defs
ENat.instNatCast : NatCast ℕ∞
-- Mathlib.RingTheory.Congruence.Basic
RingCon.mkₐ_apply : ∀ (α : Type u_1) {R : Type u_3} [inst : CommSemiring α] [inst_1 : Semiring R] [inst_2 : Algebra α R] (c : RingCon R)
  (r : R), (RingCon.mkₐ α c) r = ↑r
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Poly.mulMonC k m p c =
    bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0
    else
      bif m == Lean.Grind.CommRing.Mon.unit then Lean.Grind.CommRing.Poly.mulConstC (k % ↑c) p c
      else Lean.Grind.CommRing.Poly.mulMonC.go k m c p
-- Mathlib.Geometry.Manifold.Immersion
/-- Being an immersion w.r.t. `F` is stable under replacing `F` by an isomorphic copy.  -/
Manifold.IsImmersionOfComplement.congr_F : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F]
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {G : Type u_9} [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {M : Type u_11} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] {N : Type u_13}
  [inst_13 : TopologicalSpace N] [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (e : F ≃L[𝕜] F'),
  Manifold.IsImmersionOfComplement F I J n f ↔ Manifold.IsImmersionOfComplement F' I J n f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, (Std.ExtDTreeMap.filter f t).contains k = true → t.contains k = true
-- Mathlib.Data.Int.Log
Int.zpow_pred_clog_lt_self : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ} {r : R}, 1 < b → 0 < r → ↑b ^ (Int.clog b r - 1) < r
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNRealOrderEmbedding_apply : ⇑ENat.toENNRealOrderEmbedding = WithTop.map Nat.cast
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.equivTreesOfNumNodesEq_apply_coe : ∀ (n : ℕ) (a : { a // (fun p => p.semilength = n) a }), ↑((DyckWord.equivTreesOfNumNodesEq n) a) = (↑a).toTree
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.brecOn.go : {B : Type u} →
  [inst : Quiver B] →
    {motive : (a a_1 : B) → CategoryTheory.FreeBicategory.Hom a a_1 → Sort u_1} →
      {a a_1 : B} →
        (t : CategoryTheory.FreeBicategory.Hom a a_1) →
          ((a a_2 : B) →
              (t : CategoryTheory.FreeBicategory.Hom a a_2) →
                CategoryTheory.FreeBicategory.Hom.below t → motive a a_2 t) →
            motive a a_1 t ×' CategoryTheory.FreeBicategory.Hom.below t
-- Lean.Data.Position
Lean.FileMap.mk.injEq : ∀ (source : String) (positions : Array String.Pos.Raw) (source_1 : String) (positions_1 : Array String.Pos.Raw),
  ({ source := source, positions := positions } = { source := source_1, positions := positions_1 }) =
    (source = source_1 ∧ positions = positions_1)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_natCast : ∀ (n : ℕ), (↑n).toNNReal = ↑n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_iff : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
-- Mathlib.InformationTheory.Hamming
Hamming.instAdd : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → Add (β i)] → Add (Hamming β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [inst_4 : Nonempty ↥s] (a : ↥s.direction) (b : ↥s),
  ↑(a +ᵥ b) = ↑a +ᵥ ↑b
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_ι_terminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C),
  CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊤_ J))
-- Mathlib.RingTheory.Coalgebra.Basic
/-- the second coordinate of a representation of `comul a`  -/
Coalgebra.Repr.right : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → {a : A} → {ι : Type u_1} → Coalgebra.Repr R a ι → ι → A
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f f' : α → β},
  MeasureTheory.MeasurePreserving f μa μb → Measurable f' → f =ᵐ[μa] f' → MeasureTheory.MeasurePreserving f' μa μb
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCallHierarchyItem : BEq Lean.Lsp.CallHierarchyItem
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mulLeftMono : MulLeftMono Ordinal.{u}
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingHom_comp : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : AddMonoid M] (f : S →+* T) (g : R →+* S),
  AddMonoidAlgebra.mapRingHom M (f.comp g) = (AddMonoidAlgebra.mapRingHom M f).comp (AddMonoidAlgebra.mapRingHom M g)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.coind : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)}
  (motive : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl) → Prop),
  motive ms →
    (∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)),
        motive ms →
          ms.seq = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil ∧ ms.toFun =ᶠ[Filter.atTop] 0 ∨
            ∃ exp coef tl,
              ms.seq = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl ∧
                coef.Approximates ∧
                  Tactic.ComputeAsymptotics.Majorized ms.toFun basis_hd exp ∧
                    motive
                      (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) →
      ms.Approximates
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd : ∀ {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m]
  [hK : IsCyclotomicExtension {m} ℚ K], ¬p ∣ m → P.ramificationIdx ℤ = 1
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithBot.instRepr.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithBot α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_iff_of_le_aleph0 : ∀ {c c' : Cardinal.{u}}, c ≤ Cardinal.aleph0 → c' ≤ Cardinal.aleph0 → (Cardinal.toENat c = Cardinal.toENat c' ↔ c = c')
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- (Implementation) We construct the map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V)` for each `V` in the gluing
diagram. We will lift these maps into `ιInvApp`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        {i : D.J} →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (j : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J)) →
              (D.U i).presheaf.obj (Opposite.op U) ⟶ (D.diagramOverOpen U).obj (Opposite.op j)
-- Mathlib.NumberTheory.Niven
Complex.exp_rat_mul_pi_mul_I_pow_two_mul_den : ∀ (q : ℚ), Complex.exp (↑q * ↑Real.pi * Complex.I) ^ (2 * q.den) = 1
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink : Type
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_id : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R], MvPolynomial.rename id = AlgHom.id R (MvPolynomial σ R)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- An equality of the form `c = 0`. It is used to simplify polynomial coefficients.
 -/
Lean.Meta.Grind.Arith.CommRing.CommRing.numEq0? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option Lean.Meta.Grind.Arith.CommRing.EqCnstr
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.lid_comp_map : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] (f : M →ₗ[R] R) (g : N →ₗ[R] M'),
  ↑(TensorProduct.lid R M') ∘ₗ TensorProduct.map f g = g ∘ₗ ↑(TensorProduct.lid R N) ∘ₗ TensorProduct.map f LinearMap.id
-- Aesop.Forward.State
/-- Insert the raw hyps from `slot`'s queue into the variable map.  -/
Aesop.ClusterState.addQueuedRawHyps : Aesop.Slot → Aesop.ClusterState → Aesop.ClusterState.AddM Aesop.ClusterState
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- Composition of morphisms in `SimplicialThickening J`, as a functor `(i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k)`
 -/
CategoryTheory.SimplicialThickening.compFunctor : {J : Type u_1} →
  [inst : LinearOrder J] →
    (i j k : CategoryTheory.SimplicialThickening J) → CategoryTheory.Functor ((i ⟶ j) × (j ⟶ k)) (i ⟶ k)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_iff_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V ↔ U ≤ Vᗮ
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)),
  (CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence F sq sq₃).functor =
    CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor F sq sq₃
-- Init.Data.Float.Float32
/-- Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not
reflexive since `NaN != NaN`, and it is not a congruence because `0.0 == -0.0`, but
`1.0 / 0.0 != 1.0 / -0.0`.

This function does not reduce in the kernel. It is compiled to the C equality operator.
 -/
Float32.beq : Float32 → Float32 → Bool
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.isOpenImmersion_eq_inf : AlgebraicGeometry.IsOpenImmersion =
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
    AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Bijective ⇑x
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.AddMon C → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C
-- Mathlib.Topology.Bases
/-- A countable open cover induces a second-countable topology if all open covers
are themselves second countable.  -/
TopologicalSpace.secondCountableTopology_of_countable_cover : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_1} [Countable ι] {U : ι → Set α}
  [∀ (i : ι), SecondCountableTopology ↑(U i)],
  (∀ (i : ι), IsOpen (U i)) → ⋃ i, U i = Set.univ → SecondCountableTopology α