mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- Given the nondegenerate bilinear form `B`, the linear map `φ` has a unique left adjoint given by
`BilinForm.leftAdjointOfNondegenerate`.  -/
LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (ψ φ : V →ₗ[K] V),
  LinearMap.IsAdjointPair B B ⇑ψ ⇑φ ↔ ψ = B.leftAdjointOfNondegenerate b φ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S : CategoryTheory.ShortComplex C} {r : S.X₂ ⟶ S.X₁} {s : S.X₃ ⟶ S.X₂}
  {f_r :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam}
  {s_g :
    autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam}
  {id :
    autoParam
      (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam}
  {r_1 : S.X₂ ⟶ S.X₁} {s_1 : S.X₃ ⟶ S.X₂}
  {f_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r_1 = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam}
  {s_g_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam}
  {id_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp r_1 S.f + CategoryTheory.CategoryStruct.comp S.g s_1 =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam},
  { r := r, s := s, f_r := f_r, s_g := s_g, id := id } =
      { r := r_1, s := s_1, f_r := f_r_1, s_g := s_g_1, id := id_1 } →
    r = r_1 ∧ s = s_1
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
/-- The *square* of the Gaussian integral `∫ x:ℝ, exp (-b * x^2)` is equal to `π / b`.  -/
integral_gaussian_sq_complex : ∀ {b : ℂ}, 0 < b.re → (∫ (x : ℝ), Complex.exp (-b * ↑x ^ 2)) ^ 2 = ↑Real.pi / b
-- Mathlib.RingTheory.AdjoinRoot
/-- The canonical homomorphism from `AdjoinRoot p` to `AdjoinRoot q` induced by `f : R →+* S`,
where the polynomial `q : S[X]` divides `f(p) : R[X]`.  -/
AdjoinRoot.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) → (p : Polynomial R) → (q : Polynomial S) → q ∣ Polynomial.map f p → AdjoinRoot p →+* AdjoinRoot q
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_X_sub_C_self : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {x : R},
  Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1
-- Mathlib.RingTheory.Flat.Tensor
/-- An `R`-module `M` is flat iff for all ideals `I` of `R`, the tensor product of the
inclusion `I → R` and the identity `M → M` is injective. See `iff_rTensor_injective` to
restrict to finitely generated ideals `I`.  -/
Module.Flat.iff_rTensor_injective' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
-- Lean.Server.Rpc.Basic
/-- Objects that are being kept alive for the RPC client, together with their type names,
mapped to by their RPC reference.
 -/
Lean.Server.RpcObjectStore.aliveRefs : Lean.Server.RpcObjectStore → Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A simple graph has no `card β`-cliques iff it does not contain `⊤ : SimpleGraph β`.  -/
SimpleGraph.cliqueFree_iff_top_free : ∀ {α : Type u_1} {G : SimpleGraph α} {β : Type u_3} [inst : Fintype β], G.CliqueFree (Fintype.card β) ↔ ⊤.Free G
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.toPolyN : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_toReal_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → (MeasureTheory.Integrable (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤)
-- Mathlib.Analysis.Normed.Module.Ball.Action
continuousSMul_sphere_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
-- Init.Data.SInt.Lemmas
Int8.sub_zero : ∀ (a : Int8), a - 0 = a
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj Y ≅ 𝟭 D`, `X : GradedObject J D` and
`p : J × I → J` such that `p ⟨j, 0⟩ = j` for all `j`,
this is the right unitor isomorphism `mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X`.  -/
CategoryTheory.GradedObject.mapBifunctorRightUnitor : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) →
                    (Y : C) →
                      (F.flip.obj Y ≅ CategoryTheory.Functor.id D) →
                        [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] →
                          (p : J × I → J) →
                            (∀ (j : J), p (j, 0) = j) →
                              (X : CategoryTheory.GradedObject J D) →
                                [inst_6 :
                                    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
                                          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
                                      p] →
                                  CategoryTheory.GradedObject.mapBifunctorMapObj F p X
                                      ((CategoryTheory.GradedObject.single₀ I).obj Y) ≅
                                    X
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Context.mk.sizeOf_spec : ∀ («meta» : Lean.Server.DocumentMeta) (cursorPos : Lean.Lsp.Position) (onGoal : Option ℕ)
  (stx : Option (Lean.TSyntax `tactic)) (masterToken statusToken solvedToken : ProofWidgets.RefreshToken)
  (goal : Lean.MVarId) (hyp? : Option Lean.FVarId) (pos : Lean.SubExpr.Pos),
  sizeOf
      { «meta» := «meta», cursorPos := cursorPos, onGoal := onGoal, stx := stx, masterToken := masterToken,
        statusToken := statusToken, solvedToken := solvedToken, goal := goal, hyp? := hyp?, pos := pos } =
    1 + sizeOf «meta» + sizeOf cursorPos + sizeOf onGoal + sizeOf stx + sizeOf masterToken + sizeOf statusToken +
            sizeOf solvedToken +
          sizeOf goal +
        sizeOf hyp? +
      sizeOf pos
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ φ_1 : F ⟶ G) (e_φ : φ = φ_1) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone φ = CochainComplex.mappingCone φ_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.getKey! (Std.Internal.List.maxKey! l) l = Std.Internal.List.maxKey! l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
      (CategoryTheory.Limits.pullback.snd f g) =
    CategoryTheory.Limits.pullback.fst g f
-- Init.Data.List.Perm
List.foldl.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → β → α) (x : α) (b : β) (l : List β),
  List.foldl f x (b :: l) = List.foldl f (f x b) l
-- Mathlib.Algebra.Group.Defs
AddZero.mk : {M : Type u_2} → [toZero : Zero M] → [toAdd : Add M] → AddZero M
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrRight_refl : ∀ {α : Sort u_1} {β : α → Sort u_9}, (Equiv.piCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) → β a)
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_antitone : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  Antitone fun x => IsMulFreimanHom x A B f
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.eq_zero_iff_forall_dual_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] (x : V),
  x = 0 ↔ ∀ (g : StrongDual R V), g x = 0
-- Std.Time.Date.Unit.Day
Std.Time.Day.instReprOffset : Repr Std.Time.Day.Offset
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → m.getKeyD a fallback = m_1.getKeyD a_1 fallback_1
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.mk : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R],
  (∀ {s : Set R} {x : R}, s ∈ nhds x ↔ ∃ γ, (fun x_1 => x + x_1) '' {z | (ValuativeRel.valuation R) z < ↑γ} ⊆ s) →
    IsValuativeTopology R
-- Mathlib.RingTheory.Ideal.Maps
Ideal.orderEmbeddingOfSurjective.congr_simp : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  (f f_1 : F) (e_f : f = f_1) [inst_3 : RingHomClass F R S] (hf : Function.Surjective ⇑f),
  Ideal.orderEmbeddingOfSurjective f hf = Ideal.orderEmbeddingOfSurjective f_1 ⋯
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instField : {K : Type u} → [inst : DivisionRing K] → Field ↥(Subring.center K)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Only the empty graph has empty support.  -/
SimpleGraph.support_eq_bot_iff : ∀ {V : Type u} (G : SimpleGraph V), G.support = ∅ ↔ G = ⊥
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder β] (f : LatticeHom α β)
  (a : WithBot (WithTop α)), f.withBotWithTop' a = Option.elim a ⊥ ⇑f.withTop'
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.coeff_list_prod_of_natDegree_le : ∀ {S : Type u_1} [inst : Semiring S] (l : List (Polynomial S)) (n : ℕ),
  (∀ p ∈ l, p.natDegree ≤ n) → l.prod.coeff (l.length * n) = (List.map (fun p => p.coeff n) l).prod
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.forget₂Comon_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  {X Y : CategoryTheory.InducedCategory (CategoryTheory.Comon C) CategoryTheory.CommComon.toComon} (f : X ⟶ Y),
  (CategoryTheory.CommComon.forget₂Comon C).map f = f.hom
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_inl' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.inl M N) = Submonoid.comap (MonoidHom.snd M N) ⊥
-- Mathlib.Order.Fin.Basic
Fin.predAboveOrderHom_coe : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)), p.predAboveOrderHom i = p.predAbove i
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_i_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.symm.i h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i) h
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.trans_assoc : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄),
  (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.analyticOnNhd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  CPolynomialOn 𝕜 f s → AnalyticOnNhd 𝕜 f s
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.integral_circleTransform : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E),
  ∫ (θ : ℝ) in 0..2 * Real.pi, Complex.circleTransform R z w f θ =
    (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natSucc : ∀ {a a' c : ℕ}, Mathlib.Meta.NormNum.IsNat a a' → a'.succ = c → Mathlib.Meta.NormNum.IsNat a.succ c
-- Mathlib.Topology.UniformSpace.Basic
comap_uniformity_mulOpposite : ∀ {α : Type ua} [inst : UniformSpace α],
  Filter.comap (fun p => (MulOpposite.op p.1, MulOpposite.op p.2)) (uniformity αᵐᵒᵖ) = uniformity α
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r.inj : ∀ {n : ℕ} {a a_1 : ZMod n}, DihedralGroup.r a = DihedralGroup.r a_1 → a = a_1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_toAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U : OpenAddSubgroup G}, ↑↑U = ↑U
-- Mathlib.RingTheory.Etale.Weakly
/-- [Stacks Tag 092J](https://stacks.math.columbia.edu/tag/092J) ((2)) -/
Algebra.WeaklyEtale.trans : ∀ (R : Type u₁) (S : Type u₂) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u₃)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.WeaklyEtale R S]
  [Algebra.WeaklyEtale S T], Algebra.WeaklyEtale R T
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (B : LinearMap.BilinForm K V) (W : Subspace K V),
  Submodule.map (Submodule.subtype W) (LinearMap.domRestrict B W).ker = W ⊓ LinearMap.ker B
-- Mathlib.Data.List.TakeDrop
List.take_eq_left_iff : ∀ {α : Type u} {x y : List α} {n : ℕ}, List.take n (x ++ y) = List.take n x ↔ y = [] ∨ n ≤ x.length
-- Mathlib.Probability.Independence.Basic
/-- Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`.
We use the notation `f ⟂ᵢ[μ] g` for `IndepFun f g μ` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.«term_⟂ᵢ_» : Lean.TrailingParserDescr
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.mono : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α}, ProbabilityTheory.IsRatStieltjesPoint f a → Monotone (f a)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Bounded.eq_2 : ∀ {α : Type u_1} [inst : Preorder α] (x : WithBot α) (x_1 : WithTop α),
  (∀ (a b : α), x = some a → x_1 = some b → False) → Ordnode.nil.Bounded x x_1 = True
-- Mathlib.Order.Hom.Bounded
BoundedOrderHomClass.toRelHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : LE α} {inst_1 : LE β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedOrderHomClass F α β],
  RelHomClass F (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.RingTheory.HopfAlgebra.Quotient
/-- Pre-composition by a coalgebra homomorphism preserves the convolution unit.  -/
LinearMap.convOne_comp_coalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : HopfAlgebra R A] [inst_4 : HopfAlgebraStruct R B] (g : A →ₗc[R] B),
  WithConv.ofConv 1 ∘ₗ g.toLinearMap = WithConv.ofConv 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {lo hi a : α}, (a ∈ (Std.PRange.succ lo)...=Std.PRange.succ hi) ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo...=hi
-- Mathlib.Tactic.Widget.StringDiagram
/-- Penrose sty file for string diagrams.  -/
Mathlib.Tactic.Widget.StringDiagram.sty : String
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGT? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian distribution pdf integrates to 1 when the variance is not zero.  -/
ProbabilityTheory.lintegral_gaussianPDFReal_eq_one : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∫⁻ (x : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x) = 1
-- Mathlib.Order.Closure
LowerAdjoint.mem_closed_iff : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  x ∈ l.closed ↔ u (l.toFun x) = x
-- Init.Data.Array.Lemmas
List.foldr_push_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {xs : Array β},
  List.foldr (fun x xs => xs.push (f x)) xs l = xs ++ (List.map f l.reverse).toArray
-- Init.Data.Array.Lemmas
Array.foldr_map' : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Array α₁} {init : β} {start : ℕ},
  start = xs.size → Array.foldr g init (Array.map f xs) start = Array.foldr (fun x y => g (f x) y) init xs
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The sum of `f` over `insert a s` is the same as
the sum over `s`, as long as `a` is in `s` or `f a = 0`.  -/
Finset.sum_insert_of_eq_zero_if_notMem : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (a ∉ s → f a = 0) → ∑ x ∈ insert a s, f x = ∑ x ∈ s, f x
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.finitenessRelation : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {s : String.Slice} →
            [Std.Iterators.Finite (σ s) Id] →
              Std.Iterators.FinitenessRelation (String.Slice.SplitInclusiveIterator pat s) Id
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_lt_mul'`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul'`.  -/
one_lt_mul'' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 < a → 1 < b → 1 < a * b
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeHexDigit : String → String.Pos.Raw → Option (ℕ × String.Pos.Raw)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.conjTranspose_comp : ∀ {α : Type u_1} [inst : Star α] {I : Type u_5} {J : Type u_6} {K : Type u_7} {L : Type u_8}
  (M : Matrix I J (Matrix K L α)),
  ((Matrix.comp I J K L α) M).conjTranspose = (Matrix.comp J I L K α) (M.transpose.map fun x => x.conjTranspose)
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.whiskerRight_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] {X₁ X₂ : CategoryTheory.WideSubcategory P}
  (f : X₁ ⟶ X₂) (c' : CategoryTheory.WideSubcategory P),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c').hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom c'.obj
-- Batteries.Tactic.OpenPrivate
/-- Get the list of declarations in a module (referenced by index).  -/
Lean.Environment.declsInModuleIdx : Lean.Environment → Lean.ModuleIdx → List Lean.Name
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldRedeclInfo : Lean.Elab.FieldRedeclInfo → Lean.Elab.Info
-- Mathlib.Data.Nat.Cast.NeZero
NeZero.of_neZero_natCast : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] {n : ℕ} [h : NeZero ↑n], NeZero n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.max?_mem : ∀ {α : Type u_1} {a : α} {t : RBTree.RBNode α}, t.max? = some a → a ∈ t
-- Mathlib.Data.List.Sort
List.cons_sublist_orderedInsert : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] {l c : List α} {a : α},
  c.Sublist l → (∀ a' ∈ c, r a a') → (a :: c).Sublist (List.orderedInsert r a l)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Subobject X), P.Factors P.arrow
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Swapping elements in `σ` with equal values in `v` results in an addition that cancels  -/
AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb},
  v i = v j →
    i ≠ j →
      (AlternatingMap.domCoprod.summand a b σ) v + (AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) v = 0
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_def : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (a : α) (g : Γ), (s.coeff g) a = (s a).coeff g
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
algebraicIndependent_singleton_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [Subsingleton ι] (i : ι), AlgebraicIndependent R x ↔ Transcendental R (x i)
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaForget_hom_app_app_hom_apply_hom : ∀ (X : CommGrpCatᵒᵖ) (X_1 : CommGrpCat) (f : ↑(Opposite.unop X) →* ↑X_1),
  CommGrpCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((CommGrpCat.coyonedaForget.hom.app X).app X_1)) f) = f
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.pair.inj : ∀ {a a_1 a_2 a_3 : Nat.Partrec.Code}, a.pair a_1 = a_2.pair a_3 → a = a_2 ∧ a_1 = a_3