mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.extendScalars_commRing : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.extendScalars.commRing = P.commRing
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  curveIntegralFun (fun x => 0) γ = 0
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_map_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] {f : M →ₗ[R] M₁},
  Function.Injective ⇑f → ∀ (p : Submodule R M), Module.rank R ↥(Submodule.map f p) = Module.rank R ↥p
-- Mathlib.Computability.Primrec.List
/-- A helper lemma for proofs about bounded quantifiers on decidable relations.  -/
PrimrecPred.listFilter_listRange : ∀ {R : ℕ → ℕ → Prop} (s : ℕ) [inst : DecidableRel R],
  PrimrecRel R → Primrec fun n => List.filter (fun y => decide (R y n)) (List.range s)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ =
    (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app X.obj₃
-- Mathlib.Data.PFun
/-- `α →. β` is notation for the type `PFun α β` of partial functions from `α` to `β`.  -/
«term_→._» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Ideal.Prime
Ideal.eq_bot_of_prime : ∀ {K : Type u} [inst : DivisionSemiring K] (I : Ideal K) [h : I.IsPrime], I = ⊥
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.ιMultiDual_apply_ιMulti : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) (v : Fin n → M),
  (exteriorPower.ιMultiDual R n b s) ((exteriorPower.ιMulti R n) v) =
    (Matrix.of fun i j => (b.coord ((Set.powersetCard.ofFinEmbEquiv.symm s) j)) (v i)).det
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The product of subsemigroups is isomorphic to their product as semigroups.  -/
Subsemigroup.prodEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (s : Subsemigroup M) → (t : Subsemigroup N) → ↥(s.prod t) ≃* ↥s × ↥t
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightIso_hom_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 : Cᴹᵒᵖ),
  (X.tensorRightIso.hom.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop X_1.unmop)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t u : Finset β},
  s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_snd_of_isMulCocycle₂ : ∀ {G : Type u_1} {M : Type u_2} [inst : Monoid G] [inst_1 : CommGroup M] [inst_2 : MulAction G M] {f : G × G → M},
  groupCohomology.IsMulCocycle₂ f → ∀ (g : G), f (g, 1) = g • f (1, 1)
-- Mathlib.Analysis.Calculus.Deriv.Mul
ContinuousLinearMap.derivWithin_of_bilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {G : Type u_1}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : 𝕜} {s : Set 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E}
  {v : 𝕜 → F},
  DifferentiableWithinAt 𝕜 u s x →
    DifferentiableWithinAt 𝕜 v s x →
      derivWithin (fun y => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
IsGroupLikeElem.antipode_antipode : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {a : A},
  IsGroupLikeElem R a → (HopfAlgebraStruct.antipode R) ((HopfAlgebraStruct.antipode R) a) = a
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instGroup : {G : Type u_3} → [Group G] → Group (ConjAct G)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormedSpaceComplexForall : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [inst_2 : Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [inst_6 : (i : ι) → CStarModule A (E i)] →
                    [inst_7 : StarOrderedRing A] → NormedSpace ℂ (WithCStarModule A ((i : ι) → E i))
-- Mathlib.Topology.Connected.Clopen
/-- Preconnected sets are either contained in or disjoint to any given clopen set.  -/
IsPreconnected.subset_isClopen : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsPreconnected s → IsClopen t → (s ∩ t).Nonempty → s ⊆ t
-- Mathlib.Tactic.FastInstance
/-- Core algorithm for normalizing instances.
* Ideally, the term is replaced with a synthesized instance.
* If not, it is reduced to a constructor
  and each instance implicit field is given the same treatment.

Many reductions for typeclasses are done with reducible transparency, so the entire body
is `withReducible` with some exceptions.
 -/
_private.Mathlib.Tactic.FastInstance.0.Mathlib.Elab.FastInstance.makeFastInstance : Lean.Expr → Lean.Expr → optParam Bool true → optParam (Array Lean.Name) #[] → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are
equal  -/
CategoryTheory.Limits.pushout.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {W : C} {k l : CategoryTheory.Limits.pushout f g ⟶ W},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) k =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l →
      k = l
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Makes the `NeBot` instance visible to the typeclass machinery.  -/
SummationFilter.instNeBotFinsetFilterOfNeBot : ∀ {β : Type u_2} (L : SummationFilter β) [L.NeBot], L.filter.NeBot
-- Mathlib.GroupTheory.Congruence.Defs
Con.monoid.eq_1 : ∀ {M : Type u_4} [inst : Monoid M] (c : Con M),
  c.monoid =
    { toSemigroup := c.semigroup, toOne := c.one, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow, npow_zero := ⋯,
      npow_succ := ⋯ }
-- Mathlib.Data.List.Monad
List.pure_def : ∀ {α : Type u} (a : α), pure a = [a]
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → Std.DTreeMap.Raw α β cmp → (a : α) → β a → Option (β a) × Std.DTreeMap.Raw α β cmp
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_id : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : AddZeroClass α], ⇑(OrderAddMonoidHom.id α) = id
-- Init.Data.List.Lemmas
List.eq_replicate_iff : ∀ {α : Type u_1} {a : α} {n : ℕ} {l : List α}, l = List.replicate n a ↔ l.length = n ∧ ∀ b ∈ l, b = a
-- Mathlib.Algebra.Free
FreeSemigroup.of.eq_1 : ∀ {α : Type u} (x : α), FreeSemigroup.of x = { head := x, tail := [] }
-- Init.SimpLemmas
instAssociativeBoolAnd : Std.Associative fun x1 x2 => x1 && x2
-- Init.Data.List.Nat.Sum
List.sum_le_max_mul_length_nat : ∀ {xs : List ℕ} (h : xs ≠ []), xs.sum ≤ xs.max h * xs.length
-- Mathlib.Order.Booleanisation
Booleanisation.lift_sdiff_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a \ Booleanisation.comp b = Booleanisation.lift (a ⊓ b)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_translation_number₀' : ∀ (f : CircleDeg1Lift), Filter.Tendsto (fun n => (f ^ (n + 1)) 0 / (↑n + 1)) Filter.atTop (nhds f.translationNumber)
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.range_eq_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S},
  f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Order.Filter.Prod
Filter.tendsto_swap4_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter α} {g : Filter β} {h : Filter γ}
  {k : Filter δ}, Filter.Tendsto (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) ((f ×ˢ h) ×ˢ g ×ˢ k)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f g : α →ᵈ β},
  f = g ↔ ∀ (x : α), f x = g x
-- Std.Time.Format
/-- The DateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ`
for representing date, time, and time zone.
 -/
Std.Time.Formats.dateTimeWithZone : Std.Time.GenericFormat Std.Time.Awareness.any
-- Init.Prelude
/-- Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.

The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨`
operator.

The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `true` then `y` is not evaluated at runtime.
 -/
Bool.or : Bool → Bool → Bool
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_lt_mul_left : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LT α] [DenselyOrdered α] [MulRightStrictMono α] {a b c : α},
  c < a * b → ∃ a' < a, c < a' * b
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.coe_sInf : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Submonoid M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Logic.Equiv.Finset
/-- Makes `raise' l n` into a finset. Elements are distinct thanks to `raise'_sorted`.  -/
Denumerable.raise'Finset : List ℕ → ℕ → Finset ℕ
-- Init.ShareCommon
ShareCommon.State : ShareCommon.StateFactory → Type u
-- Mathlib.Order.SuccPred.Tree
/-- The root of a `SubRootedTree`.
 -/
SubRootedTree.root : {t : RootedTree} → SubRootedTree t → ↑t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.keyword.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.keyword = 1
-- Lean.Attributes
Lean.AttributeKind.scoped.sizeOf_spec : sizeOf Lean.AttributeKind.scoped = 1
-- Mathlib.RepresentationTheory.Tannaka
/-- The `rightFDRep` component of `η : Aut (forget k G)` preserves multiplication  -/
TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G]
  (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)) (f g : G → k),
  have α := ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep).hom;
  α (f * g) = α f * α g
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inr_comp_pushoutObjIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inr f g).app d)
      (CategoryTheory.Limits.pushoutObjIso f g d).hom =
    CategoryTheory.Limits.pushout.inr (f.app d) (g.app d)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_functor_obj_toProd : ∀ (X : Bipointed), (Bipointed.swapEquiv.functor.obj X).toProd = X.toProd.swap
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
-- Batteries.Data.List.Basic
/-- `extractP p l` returns a pair of an element `a` of `l` satisfying the predicate
`p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`.
 -/
List.extractP : {α : Type u_1} → (α → Bool) → List α → Option α × List α
-- Mathlib.GroupTheory.FinitelyPresentedGroup
AddGroup.IsFinitelyPresented.mk : ∀ {G : Type u_5} [inst : AddGroup G],
  (∃ n φ, Function.Surjective ⇑φ ∧ φ.ker.IsFinitelyNormallyGenerated) → AddGroup.IsFinitelyPresented G
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_inv_apply : ∀ {X Y Z : TopCat} {x : ↑X} {y : ↑Y} {z : ↑Z},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) (x, y, z) =
    ((x, y), z)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sq_add_sin_sq : ∀ (x : ℂ), Complex.cos x ^ 2 + Complex.sin x ^ 2 = 1
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M},
  TensorialAt I F Φ x → ∀ {f : M → 𝕜} {σ : (x : M) → V x}, MDiffAt f x → MDiffAt (T% σ) x → Φ (f • σ) = f x • Φ σ
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_lt_two : Real.goldenRatio < 2
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.ιK_mor₁ : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
  CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ {K : A} (α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [inst_7 : ι.Full]
      [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful],
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α) f₁ = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- If `F : C ⥤ D` if a functor and `R : Dᵒᵖ ⥤ CommRingCat` is a presheaf
of commutative rings, this is the pushforward functor from the category
of presheaves of modules on `R` to the category of presheaves of
modules on `F.op ⋙ R`.  -/
PresheafOfModules.pushforward₀OfCommRingCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (R : CategoryTheory.Functor Dᵒᵖ CommRingCat) →
            CategoryTheory.Functor (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))
              (PresheafOfModules ((F.op.comp R).comp (CategoryTheory.forget₂ CommRingCat RingCat)))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientQuotientEquivQuotient.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (c d : Con M) (h : c ≤ d),
  c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_mul' := ⋯ }
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toLinearEquiv_eq_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (f : A ≃ₗc[R] B), f.toLinearEquiv = f.toLinearEquiv
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, t.contains a = false → Std.ExtDTreeMap.Const.get? t a = none
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] {f : (a : α) → β a → γ a} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = true},
  (Std.DTreeMap.Internal.Impl.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_one_iff`. -/
Ordinal.principal_one_iff : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}}, Ordinal.IsPrincipal op 1 ↔ op 0 0 = 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rcc : ∀ {m n k : ℕ}, Array.map (fun x => x + k) (m...=n).toArray = ((m + k)...=n + k).toArray
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.η.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F G : CategoryTheory.MonoidalCategory.DayFunctor C V),
  F.η G = CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V F G
-- Mathlib.CategoryTheory.Join.Opposites
/-- Characterize (up to a rightOp) the action of the right inclusion on `Join.opEquivFunctor`.  -/
CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Join.inclRight C D).comp (CategoryTheory.Join.opEquiv C D).functor.rightOp ≅
          (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.single_injective : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ),
  Function.Injective ⇑(HahnSeries.single a)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.one_right : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q], RegularWreathProduct.right 1 = 1
-- Mathlib.Algebra.Polynomial.Smeval
RingHom.smulOneHom.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Module R S]
  [inst_3 : IsScalarTower R S S], RingHom.smulOneHom = RingHom.smulOneHom
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
trdeg_ne_zero_iff : ∀ {R : Type u_3} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.trdeg R A ≠ 0 ↔ Algebra.Transcendental R A
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_lt_succ : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b → Std.PRange.UpwardEnumerable.LT (Std.PRange.succ a) (Std.PRange.succ b)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.kind? : LeanSearchClient.SearchResult → Option String
-- Mathlib.Analysis.Convex.Function
/-- A strictly convex function admits at most one global minimum.  -/
StrictConvexOn.eq_of_isMinOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : AddCommMonoid E]
  [inst_7 : SMul 𝕜 E] [inst_8 : Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} {s : Set E} {x y : E},
  StrictConvexOn 𝕜 s f → IsMinOn f s x → IsMinOn f s y → x ∈ s → y ∈ s → x = y
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.alphaEqv : Lean.IR.IndexRenaming → Lean.IR.VarId → Lean.IR.VarId → Bool
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A B : Rep.{w, u, v} k G) (f : A ⟶ B),
  Rep.ofHom (Rep.Hom.hom f) = f
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_intCast_add : ∀ {x : ℝ} (m : ℤ), Irrational (↑m + x) → Irrational x
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instOne : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → [One β] → One (α →ₘ[μ] β)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one_lt_coe : ∀ {α : Type u} [inst : One α] {a : α} [inst_1 : LT α], 1 < ↑a ↔ 1 < a