mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.toContinuousLinearMap.congr_simp : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F' : Type x}
  [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [inst_8 : IsTopologicalAddGroup F']
  [inst_9 : ContinuousSMul 𝕜 F'] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E],
  LinearMap.toContinuousLinearMap = LinearMap.toContinuousLinearMap
-- Init.System.IO
/-- Resolves a path to an absolute path that contains no '.', '..', or symbolic links.

This function coincides with the [POSIX `realpath`
function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/realpath.html).
 -/
IO.FS.realPath : System.FilePath → IO System.FilePath
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.biUnion_sdiff_biUnion_subset`. -/
Set.biUnion_diff_biUnion_subset : ∀ {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ s₂ : Set α), (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- A graph is matching free if it has no perfect matching. It does not make much sense to
consider a graph being free of just matchings, because any non-trivial graph has those.
 -/
SimpleGraph.IsMatchingFree : {V : Type u_1} → SimpleGraph V → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negY_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (X Y Z : R),
  W'.negY ![X, Y, Z] = -Y - W'.a₁ * X * Z - W'.a₃ * Z ^ 3
-- Mathlib.Algebra.CharP.Invertible
invertibleSucc : {K : Type u_2} → [inst : DivisionSemiring K] → [CharZero K] → (n : ℕ) → Invertible ↑n.succ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.coconeOpEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op c.unop, map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => (Opposite.unop c).op, map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ })
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.map_vadd_multiples : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommMonoid α],
  Function.Periodic f c → ∀ (a : ↥(AddSubmonoid.multiples c)) (x : α), f (a +ᵥ x) = f x
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgMessageSeverity : Lean.Doc.FromDocArg Lean.MessageSeverity
-- Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
/-- The integral of `log ∘ sin` on `0 … π` equals `-log 2 * π`.
 -/
integral_log_sin_zero_pi : ∫ (x : ℝ) in 0..Real.pi, Real.log (Real.sin x) = -Real.log 2 * Real.pi
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod_inl_inr : ∀ {M : Type u_6} {N : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N],
  (AddMonoidHom.inl M N).coprod (AddMonoidHom.inr M N) = AddMonoidHom.id (M × N)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_one : ∀ (k : ℕ), (ArithmeticFunction.sigma k) 1 = 1
-- Init.Data.List.Attach
List.head_attach : ∀ {α : Type u_1} {xs : List α} (h : xs.attach ≠ []), xs.attach.head h = ⟨xs.head ⋯, ⋯⟩
-- Mathlib.Algebra.Group.AddChar
/-- `AddChar A M` is the type of maps `A → M`, for `A` an additive monoid and `M` a multiplicative
monoid, which intertwine addition in `A` with multiplication in `M`.

We only put the typeclasses needed for the definition, although in practice we are usually
interested in much more specific cases (e.g. when `A` is a group and `M` a commutative ring).
 -/
AddChar : (A : Type u_1) → [AddMonoid A] → (M : Type u_2) → [Monoid M] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  T.rotate.mor₃ = -(CategoryTheory.shiftFunctor C 1).map T.mor₁
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block  -/
MulAction.IsBlock.of_orbit : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {H : Subgroup G} {a : X},
  MulAction.stabilizer G a ≤ H → MulAction.IsBlock G (MulAction.orbit (↥H) a)
-- Mathlib.Algebra.Ring.GeomSum
mul_neg_geom_sum : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), (1 - x) * ∑ i ∈ Finset.range n, x ^ i = 1 - x ^ n
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.coe_pi : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] (s : Set ι) (t : (i : ι) → Subalgebra R (S i)),
  ↑(Subalgebra.pi s t) = (Submodule.pi s fun i => Subalgebra.toSubmodule (t i)).carrier
-- Lean.Meta.Tactic.Grind.Types
/-- E-matching related fields for the `grind` goal.  -/
Lean.Meta.Grind.EMatch.State : Type
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- If `f` assumes values between `0` and `1` and the support is contained in `V`, then
`Λ f ≤ rieszMeasure V`.  -/
RealRMK.le_rieszMeasure_tsupport_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X]
  {f : CompactlySupportedContinuousMap X ℝ},
  (∀ (x : X), 0 ≤ f x ∧ f x ≤ 1) → ∀ {V : Set X}, tsupport ⇑f ⊆ V → ENNReal.ofReal (Λ f) ≤ (RealRMK.rieszMeasure Λ) V
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousOn_primitive_interval_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.uIcc a b) μ → ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) (Set.uIcc a b)
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.surjective_pullbackSnd_of_surjective : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T), Function.Surjective ⇑f → Function.Surjective ⇑(f.pullbackSnd g)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- In a `p`-th cyclotomic extension of `ℚ`, we have that `ζ - 1` divides `p` in `𝓞 K`.  -/
IsPrimitiveRoot.toInteger_sub_one_dvd_prime' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p), hζ.toInteger - 1 ∣ ↑p
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_apply_inl_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : M),
  (MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inl (Monoid.Coprod.inl x)) = Monoid.Coprod.inl x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mono_set : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {s t : Set α},
  s ⊆ t → MeasureTheory.AEStronglyMeasurable f (μ.restrict t) → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr_fin_two : ∀ {R : Type u_1} [inst : CommRing R] (A : Matrix (Fin 2) (Fin 2) R), A.discr = A.trace ^ 2 - 4 * A.det
-- Mathlib.Analysis.Seminorm
Seminorm.comp_smul : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜]
  [inst_1 : SeminormedCommRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E]
  [inst_4 : AddCommGroup E₂] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂)
  (c : 𝕜₂), p.comp (c • f) = ‖c‖₊ • p.comp f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.instNontrivialMixedSpace : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Nontrivial (NumberField.mixedEmbedding.euclidean.mixedSpace K)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_smul_add_adjp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A B : Matrix n n R}, A * B = 1 → Matrix.detp 1 B • A + Matrix.adjp (-1) B = Matrix.detp (-1) B • A + Matrix.adjp 1 B
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ofBijective_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) (a : P₁),
  (AffineEquiv.ofBijective hφ) a = φ a
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_max : ∀ (o₁ o₂ : Ordinal.{u_1}), Ordinal.preOmega (max o₁ o₂) = max (Ordinal.preOmega o₁) (Ordinal.preOmega o₂)
-- Mathlib.Algebra.Polynomial.Identities
/-- `(x + y)^n` can be expressed as `x^n + n*x^(n-1)*y + k * y^2` for some `k` in the ring.
 -/
Polynomial.powAddExpansion : {R : Type u_1} →
  [inst : CommSemiring R] → (x y : R) → (n : ℕ) → { k // (x + y) ^ n = x ^ n + ↑n * x ^ (n - 1) * y + k * y ^ 2 }
-- Mathlib.Topology.FiberBundle.Basic
/-- A fiber bundle constructed from core is indeed a fiber bundle.  -/
FiberBundleCore.fiberBundle : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → FiberBundle F Z.Fiber
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le' : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : One M] {s : Set α} {f g : α → M},
  (∀ a ∈ s, f a ≤ g a) → (∀ a ∉ s, 1 ≤ g a) → s.mulIndicator f ≤ g
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.domRestrict₁₂_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) (x : ↥p) (y : ↥q),
  ((f.domRestrict₁₂ p q) x) y = (f ↑x) ↑y
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A], (F.sheafPushforwardContinuous A J₀ J).EssSurj
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The k-th coefficient of `det (1 + X • M)` equals the sum of all k×k principal minors of M.
This generalizes `coeff_det_one_add_X_smul_one` (the k = 1 case, which gives the trace)
and `det_eq_sign_charpoly_coeff` (the k = n case, which gives the determinant).  -/
Matrix.coeff_det_one_add_X_smul_eq_sum_minors : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (k : ℕ),
  (1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff k =
    ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Promote `HahnEmbedding.Partial.sSupFun` to a `HahnEmbedding.Partial`.  -/
HahnEmbedding.Partial.sSup : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                [IsOrderedAddMonoid R] →
                                  {c : Set (HahnEmbedding.Partial seed)} →
                                    c.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) c → HahnEmbedding.Partial seed
-- Mathlib.Order.Atoms
/-- Every element is either `⊥` or `⊤`  -/
IsSimpleOrder.eq_bot_or_eq_top : ∀ {α : Type u_4} {inst : LE α} {inst_1 : BoundedOrder α} [self : IsSimpleOrder α] (a : α), a = ⊥ ∨ a = ⊤
-- Batteries.Data.List.Basic
/-- Take `n` elements from a list `l`. If `l` has less than `n` elements, append `n - length l`
elements `x`.
 -/
List.takeD : {α : Type u_1} → ℕ → List α → α → List α
-- Lean.KeyedDeclsAttribute
Lean.instNonemptyKeyedDeclsAttribute : ∀ {γ : Type}, Nonempty (Lean.KeyedDeclsAttribute γ)
-- Init.Data.UInt.Lemmas
UInt16.lt_add_one : ∀ {c : UInt16}, c ≠ -1 → c < c + 1
-- Mathlib.Probability.Distributions.Poisson.Basic
_private.Mathlib.Probability.Distributions.Poisson.Basic.0.ProbabilityTheory.map_cast_poissonMeasure_conv_real : ∀ (r₁ r₂ : NNReal),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₁)).conv
      (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₂)) =
    MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure (r₁ + r₂))
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainOfBialgHom_comp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} {I : Type u_7} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : AddGroup G] [inst_3 : AddGroup H] [inst_4 : AddGroup I]
  (f : AddMonoidAlgebra R H →ₐc[R] AddMonoidAlgebra R I) (g : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H),
  AddMonoidAlgebra.mapDomainOfBialgHom (f.comp g) =
    (AddMonoidAlgebra.mapDomainOfBialgHom f).comp (AddMonoidAlgebra.mapDomainOfBialgHom g)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (out' : γ) → motive (some out')),
  (match none with
    | none => h_1 ()
    | some out' => h_2 out') =
    h_1 ()
-- Mathlib.Control.Monad.Cont
instLawfulMonadContOptionT : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadCont m] [LawfulMonadCont m], LawfulMonadCont (OptionT m)
-- Mathlib.Topology.UniformSpace.Equiv
/-- `Equiv.piCongrLeft` as a uniform isomorphism: this is the natural isomorphism
`Π i, β (e i) ≃ᵤ Π j, β j` obtained from a bijection `ι ≃ ι'`.  -/
UniformEquiv.piCongrLeft : {ι : Type u_4} →
  {ι' : Type u_5} →
    {β : ι' → Type u_6} →
      [inst : (j : ι') → UniformSpace (β j)] → (e : ι ≃ ι') → ((i : ι) → β (e i)) ≃ᵤ ((j : ι') → β j)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- If `M` additively acts on `α`, then `DomAddAct M` acts on `α → β` as
well as some bundled maps from `α`. This is a type synonym for `AddOpposite M`, so this corresponds
to a right action of `M`.  -/
«term_ᵈᵃᵃ» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?ₘ'.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE?ₘ' k t =
    Std.DTreeMap.Internal.Impl.explore (compare k) none
      (fun x x_1 =>
        match x, x_1 with
        | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1 => some ⟨k', v⟩
        | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r => (c.inner.or r.head?).or base
        | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 => base)
      t
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.adhoc.sizeOf_spec : ∀ (backend : Lean.Name), sizeOf (Lean.ExternEntry.adhoc backend) = 1 + sizeOf backend
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mulIndicator_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : One R] {U : Set X} (f : LocallyConstant X R)
  (hU : IsClopen U) (x : X), (f.mulIndicator hU) x = U.mulIndicator (⇑f) x
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.map_prod_map : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) {α' : Type u_3} [inst_2 : MeasurableSpace α']
  {β' : Type u_4} [inst_3 : MeasurableSpace β'] {f : α → α'} {g : β → β'},
  Measurable f → Measurable g → (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.isUnaryEntries : {α : Type u_1} →
  {β : Type u_2} →
    Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → ℕ → Option (α × β) → Option (α × β)
-- Init.Data.List.Erase
List.length_eraseIdx : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
coe_setBasisOfLinearIndependentOfCardEqFinrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  [inst_3 : Nonempty ↑s] [inst_4 : Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val)
  (card_eq : s.toFinset.card = Module.finrank K V),
  ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.liftFromUnderComp.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.WithInitial J → Sort u_2)
  (h_1 : Unit → motive CategoryTheory.WithInitial.star) (h_2 : (a : J) → motive (CategoryTheory.WithInitial.of a)),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.star => h_1 ()
    | CategoryTheory.WithInitial.of a => h_2 a) =
    h_1 ()
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isTrivialBottomUp : Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Bool
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `RelUpperSet` is an upper set relative to `P`.

Do NOT use directly. Please use `RelUpperSet.isRelUpperSet` instead.  -/
RelUpperSet.isRelUpperSet' : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} (self : RelUpperSet P), IsRelUpperSet self.carrier P
-- Lean.Environment
/-- Checks whether the given declaration is known on the current branch, in which case `findAsync?` will
not block.
 -/
Lean.Environment.containsOnBranch : Lean.Environment → Lean.Name → Bool
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.one_le : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced → 1 ≤ sz
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.orderIsoRingCon_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (self : TwoSidedIdeal R),
  TwoSidedIdeal.orderIsoRingCon self = self.ringCon
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If a function is meromorphic in normal form at `x`, then it is meromorphic at `x`.  -/
MeromorphicNFAt.meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicNFAt f x → MeromorphicAt f x
-- Mathlib.Data.Matrix.Basis
Matrix.single_apply_of_ne : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (c : α) (i' : m) (j' : n), ¬(i = i' ∧ j = j') → Matrix.single i j c i' j' = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonPrepareRenameParams : Lean.FromJson Lean.Lsp.PrepareRenameParams
-- Mathlib.Algebra.Module.Hom
/-- Scalar multiplication as a biadditive monoid homomorphism. We need `M` to be commutative
to have addition on `M →+ M`.  -/
AddMonoidHom.smul : {R : Type u_1} → {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R →+ M →+ M
-- Mathlib.Data.Finmap
Finmap.sigma_keys_lookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s : Finmap β),
  (s.keys.sigma fun i => (Finmap.lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_mul_eventuallyLE_one : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M}, Filter.Tendsto f l Filter.atBot → g ≤ᶠ[l] 1 → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.isSplittingField_C : ∀ {K : Type v} [inst : Field K] (a : K), Polynomial.IsSplittingField K K (Polynomial.C a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
doublyStochastic.congr_simp : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], doublyStochastic R n = doublyStochastic R n