mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- The property that a full subcategory of a pretriangulated category
equipped with a t-structure can be endowed with an induced t-structure.  -/
CategoryTheory.ObjectProperty.HasInducedTStructure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (P : CategoryTheory.ObjectProperty C) →
                CategoryTheory.Triangulated.TStructure C → [P.IsTriangulated] → Prop
-- Mathlib.Algebra.Group.Prod
Prod.instRightCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : RightCancelMonoid M] [inst_1 : RightCancelMonoid N],
  Prod.instRightCancelMonoid = { toMonoid := Prod.instMonoid, toIsRightCancelMul := ⋯ }
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The affine space over an affine base is isomorphic to the spectrum of the polynomial ring.
Also see `AffineSpace.SpecIso`.
 -/
AlgebraicGeometry.AffineSpace.isoOfIsAffine : (n : Type u) →
  (S : AlgebraicGeometry.Scheme) →
    [AlgebraicGeometry.IsAffine S] →
      AlgebraicGeometry.AffineSpace n S ≅
        AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))
-- Mathlib.Analysis.Analytic.Constructions
/-- **Alias** of `AnalyticAt.curry_left`.

---

Analytic functions on products are analytic in the first coordinate  -/
AnalyticAt.along_fst : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F},
  AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun x => f (x, p.2)) p.1
-- Mathlib.Dynamics.Ergodic.Extreme
/-- Given a constant `c ≠ ∞`, an extreme point of the set of measures that are invariant under `f`
and have total mass `c` is an ergodic measure.  -/
Ergodic.of_mem_extremePoints_measure_univ_eq : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} {c : ENNReal},
  c ≠ ⊤ → μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = c} → Ergodic f μ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_comm : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
  [inst_2 : AddCommMonoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N),
  (f.sum fun x v => g.sum fun x' v' => h x v x' v') = g.sum fun x' v' => f.sum fun x v => h x v x' v'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constInsertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] (l : List (α × β)),
  m₁.Equiv m₂ → (Std.DHashMap.Const.insertMany m₁ l).Equiv (Std.DHashMap.Const.insertMany m₂ l)
-- Mathlib.Tactic.Ring.Basic
/-- Converts `ExProd sα` to `ExProd sβ`, assuming `sα` and `sβ` are defeq.  -/
Mathlib.Tactic.Ring.ExProd.cast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          {sβ : Q(CommSemiring «$β»)} →
            {a : Q(«$α»)} → Mathlib.Tactic.Ring.ExProd sα a → (a : Q(«$β»)) × Mathlib.Tactic.Ring.ExProd sβ a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The homeomorphism between the `realMixedSpace` and the `polarSpace`.
 -/
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace : (K : Type u_1) →
  [inst : Field K] → NumberField.mixedEmbedding.realMixedSpace K ≃ₜ NumberField.mixedEmbedding.polarSpace K
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.whiskerLeft_def : ∀ {R : Type u} [inst : CommRing R] (M x x_1 : ModuleCat R) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = ModuleCat.ofHom (LinearMap.lTensor (↑M) (ModuleCat.Hom.hom f))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), t.contains a = false)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.IsSeparated (f ∣_ V)
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.mk : Lean.MVarIdMap Lean.MVarId → Lean.Meta.MVarRenaming
-- Mathlib.NumberTheory.NumberField.Basic
Module.Basis.localizationLocalization.congr_simp : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1)
  [inst_1 : CommSemiring Rₛ] [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {A : Type u_3}
  [inst_4 : CommSemiring A] [inst_5 : Algebra R A] (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ]
  [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ] [inst_10 : IsScalarTower R Rₛ Aₛ] [inst_11 : IsScalarTower R A Aₛ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b b_1 : Module.Basis ι R A),
  b = b_1 → Module.Basis.localizationLocalization Rₛ S Aₛ b = Module.Basis.localizationLocalization Rₛ S_1 Aₛ b_1
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.le_vanishingIdeal_zeroLocus : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (I : Ideal (MvPolynomial σ k)), I ≤ MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I)
-- Mathlib.Algebra.Star.StarAlgHom
/-- Construct a star algebra equivalence from a pair of non-unital star algebra homomorphisms.  -/
StarAlgEquiv.ofNonUnitalStarAlgHom : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A₁] →
          [inst_2 : DistribMulAction R A₁] →
            [inst_3 : Star A₁] →
              [inst_4 : NonUnitalNonAssocSemiring A₂] →
                [inst_5 : DistribMulAction R A₂] →
                  [inst_6 : Star A₂] →
                    (f : A₁ →⋆ₙₐ[R] A₂) →
                      (g : A₂ →⋆ₙₐ[R] A₁) →
                        g.comp f = NonUnitalStarAlgHom.id R A₁ → f.comp g = NonUnitalStarAlgHom.id R A₂ → A₁ ≃⋆ₐ[R] A₂
-- Mathlib.Topology.Algebra.Group.Basic
nhdsMulHom_apply : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (x : G),
  nhdsMulHom x = nhds x
-- Mathlib.CategoryTheory.LiftingProperties.Basic
/-- Given morphisms `i : A ⟶ B`, `p : X ⟶ Y`, `b : B ⟶ Y`,
this is the property that a lifting exists for all squares
with `i` on left, `p` on the right and `b` on the bottom.  -/
CategoryTheory.HasLiftingPropertyFixedBot : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {Y X B A : C} → (A ⟶ B) → (X ⟶ Y) → (B ⟶ Y) → Prop
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instInhabitedDeclMod : Inhabited Lean.Meta.LibrarySearch.DeclMod
-- Lean.Meta.Basic
/-- Auxiliary structure for representing postponed universe constraints.
Remark: the fields `ref` and `rootDefEq?` are used for error message generation only.
Remark: we may consider improving the error message generation in the future.
 -/
Lean.Meta.PostponedEntry : Type
-- Init.Data.Vector.Basic
/-- Finds the first index of a given value in a vector using a predicate. Returns `none` if the
no element of the index matches the given value.  -/
Vector.findFinIdx? : {α : Type u_1} → {n : ℕ} → (α → Bool) → Vector α n → Option (Fin n)
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric_sUnion : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {c : Set (Set α)},
  IsCompact s → (∀ t ∈ c, IsOpen t) → s ⊆ ⋃₀ c → ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.eball x δ ⊆ t
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidOpenTextDocumentParams : Lean.ToJson Lean.Lsp.DidOpenTextDocumentParams
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber.eq_1 : ∀ (n : ℕ), n.fermatNumber = 2 ^ 2 ^ n + 1
-- Mathlib.Computability.Primrec.Basic
Primrec.primrecPred : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  (Primrec fun a => decide (p a)) → PrimrecPred p
-- Mathlib.Analysis.Convex.Body
ConvexBody.instSMulReal : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → [ContinuousSMul ℝ V] → SMul ℝ (ConvexBody V)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `Ω n` is the number of prime factors of `n`.  -/
ArithmeticFunction.cardFactors : ArithmeticFunction ℕ
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.minus.sizeOf_spec : ∀ {v : Lean.Level} {M : Q(Type v)} (iM : Q(Field «$M»)), sizeOf (Mathlib.Tactic.FieldSimp.Sign.minus iM) = 1 + sizeOf iM
-- Init.Data.Int.Order
Int.min_def : ∀ (n m : ℤ), min n m = if n ≤ m then n else m
-- Mathlib.Data.PSigma.Order
PSigma.Lex.noMinOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), NoMinOrder (α i)], NoMinOrder (Σₗ' (i : ι), α i)
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.mul_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsLowerSet t → IsLowerSet (s * t)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Day.Offset
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.sdiff_singleton_indep`. -/
Matroid.IsCircuit.diff_singleton_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → M.Indep (C \ {e})
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- `R^n/I^n` is a `R/I`-module.  -/
Ideal.modulePi : {ι : Type u_1} →
  {R : Type u_3} →
    [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → Module (R ⧸ I) ((ι → R) ⧸ Ideal.pi fun x => I)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMax.eq_def : ∀ {α : Type u_1} (x : Ordnode α),
  x.eraseMax =
    match x with
    | Ordnode.nil => Ordnode.nil
    | Ordnode.node size l x Ordnode.nil => l
    | Ordnode.node size l x (Ordnode.node sz l' y r') => l.balanceL x (Ordnode.node sz l' y r').eraseMax
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.mul_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N)
  [CategoryTheory.IsMonHom g],
  CategoryTheory.CategoryStruct.comp (f₁ * f₂) g =
    CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₁.eq_1 : ∀ (w : UInt8) (h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done),
  ByteArray.utf8DecodeChar?.assemble₁ w h = some { val := w.toUInt32, valid := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the first morphism in the factorization  -/
CategoryTheory.MorphismProperty.MapFactorizationData.i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {X Y : C} → {f : X ⟶ Y} → (self : W₁.MapFactorizationData W₂ f) → X ⟶ self.Z
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.modifyₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (f : β → β),
  Std.DHashMap.Internal.Raw₀.Const.modifyₘ m a f =
    Std.DHashMap.Internal.Raw₀.Const.alterₘ m a fun option => Option.map f option
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.hom_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y),
  f = g ↔ f.left = g.left
-- Mathlib.RingTheory.Congruence.Basic
RingCon.ringConGen_sSup : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (rs : Set (R → R → Prop)),
  ringConGen (sSup rs) = ⨆ r ∈ rs, ringConGen r
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_le_iff : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a + b ≤ c ↔ ∀ d < b, a + d < c)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_destruct_iff : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s t ↔
    Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.quotToDoubleCoset.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (q : DoubleCoset.Quotient ↑H ↑K),
  DoubleCoset.quotToDoubleCoset H K q = DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K
-- Mathlib.Algebra.Ring.Pi
/-- Ring homomorphism between the function spaces `I → α` and `I → β`, induced by a ring
homomorphism `f` between `α` and `β`.  -/
RingHom.compLeft : {α : Type u_1} →
  {β : Type u_2} →
    [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → (I : Type u_3) → (I → α) →+* I → β
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangentAt.mem_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P}, s₁.IsIntTangentAt s₂ p → p ∈ s₂
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Orientation.oangle.congr_simp : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o o_1 : Orientation ℝ V (Fin 2)),
  o = o_1 → ∀ (x x_1 : V), x = x_1 → ∀ (y y_1 : V), y = y_1 → o.oangle x y = o_1.oangle x_1 y_1
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLen_eq_card : ∀ (μ : YoungDiagram) {i : ℕ}, μ.rowLen i = (μ.row i).card
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instBot : {X : Type u_1} → {R : Type u_2} → [inst : AddZeroClass R] → [inst_1 : Preorder R] → Bot (PseudoMetric X R)
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalExprCastMode : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasFDerivWithinAt.norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {G : Type u_4}
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {s : Set G} {x : G} {f : G → F} {f' : G →L[ℝ] F},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 • (innerSL ℝ) (f x) ∘SL f') s x
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.countPBefore.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (x s : ℕ)
  (h_1 : (head : α) → (tail : List α) → (s : ℕ) → motive (head :: tail) 0 s)
  (h_2 : (a : α) → (xs : List α) → (i s : ℕ) → motive (a :: xs) i.succ s) (h_3 : (x s : ℕ) → motive [] x s),
  (match [], x, s with
    | head :: tail, 0, s => h_1 head tail s
    | a :: xs, i.succ, s => h_2 a xs i s
    | [], x, s => h_3 x s) =
    h_3 x s
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.Γ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Preadditive.DoldKan.Γ = AlgebraicTopology.DoldKan.Γ₂
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c))
  (s : CategoryTheory.Limits.Cone F.rightOp),
  (CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sep_mem : ∀ (x y : ZFSet.{u}), ZFSet.sep (fun x => x ∈ y) x = x ∩ y
-- Init.Data.List.Erase
List.erase_comm : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a b : α) {l : List α}, (l.erase a).erase b = (l.erase b).erase a
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.coeff_domCongrBialgEquiv_apply : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (a : AddMonoidAlgebra A M),
  ((AddMonoidAlgebra.domCongrBialgEquiv R A e) a).coeff = Finsupp.mapDomain (⇑e) a.coeff
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Naturality lemma for `ΓHomEquiv` analogous to `Adjunction.homEquiv_naturality_right_symm`.  -/
CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] {X : A} {F F' : CategoryTheory.Sheaf J A}
  (f : X ⟶ (CategoryTheory.Sheaf.Γ J A).obj F) (g : F ⟶ F'),
  CategoryTheory.Sheaf.ΓHomEquiv.symm (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Sheaf.Γ J A).map g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.ΓHomEquiv.symm f) g.hom
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves finite limits, then `F : Cᵒᵖ ⥤ D` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F.rightOp],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a category `C` has 0-morphisms, there is a canonical projection from a coproduct `X ⨿ Y` to
its first component `X`.  -/
CategoryTheory.Limits.coprod.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → X ⨿ Y ⟶ X
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv_tmul : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (a : A) (p : MvPolynomial σ R),
  (MvPolynomial.algebraTensorAlgEquiv R A) (a ⊗ₜ[R] p) = a • (MvPolynomial.map (algebraMap R A)) p
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.contains_char_eq_contains_beq : ∀ {c : Char} {s : String}, s.contains c = s.contains fun x => x == c
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_rii : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α] {xs : Std.Rii α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Std.Time.Format.Modifier
Std.Time.OffsetZ.hourMinute.sizeOf_spec : sizeOf Std.Time.OffsetZ.hourMinute = 1
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.subset_span_finite_of_subset_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {t : Finset M}, ↑t ⊆ ↑(Submodule.span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(Submodule.span R ↑T)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.diag_σ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) CategoryTheory.NonPreadditiveAbelian.σ = 0
-- Mathlib.Data.Finset.Filter
/-- Return `true` if `expectedType?` is `some (Finset ?α)`, throws `throwUnsupportedSyntax` if it is
`some (Set ?α)`, and returns `false` otherwise.  -/
Mathlib.Meta.knownToBeFinsetNotSet : Option Lean.Expr → Lean.Elab.TermElabM Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  Std.DTreeMap.Raw.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty`. -/
AddAction.IsBlock.vadd_eq_vadd_of_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B → ∀ ⦃g₁ g₂ : G⦄, ((g₁ +ᵥ B) ∩ (g₂ +ᵥ B)).Nonempty → g₁ +ᵥ B = g₂ +ᵥ B
-- Mathlib.AlgebraicGeometry.Scheme
/-- Given a morphism of schemes `f : X ⟶ Y`, this is the induced map `Γ(Y, ⊤) ⟶ Γ(X, ⊤)`.
This is treated as a suffix in lemma names.  -/
AlgebraicGeometry.Scheme.Hom.appTop : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → (Y.presheaf.obj (Opposite.op ⊤) ⟶ X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.eq_1 : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  IntermediateField.adjoin F S =
    { toSubsemiring := (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)).toSubsemiring, algebraMap_mem' := ⋯,
      inv_mem' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- `ContinuousLinearMap.restrictScalars` as a `ContinuousLinearMap`.  -/
ContinuousLinearMap.restrictScalarsL : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜 E] →
            [ContinuousSMul 𝕜 E] →
              (F : Type u_3) →
                [inst_5 : AddCommGroup F] →
                  [inst_6 : TopologicalSpace F] →
                    [inst_7 : IsTopologicalAddGroup F] →
                      [inst_8 : Module 𝕜 F] →
                        (𝕜' : Type u_4) →
                          [inst_9 : NontriviallyNormedField 𝕜'] →
                            [inst_10 : NormedAlgebra 𝕜' 𝕜] →
                              [inst_11 : Module 𝕜' E] →
                                [IsScalarTower 𝕜' 𝕜 E] →
                                  [inst_13 : Module 𝕜' F] →
                                    [IsScalarTower 𝕜' 𝕜 F] →
                                      (𝕜'' : Type u_5) →
                                        [inst_15 : Ring 𝕜''] →
                                          [inst_16 : Module 𝕜'' F] →
                                            [inst_17 : ContinuousConstSMul 𝕜'' F] →
                                              [inst_18 : SMulCommClass 𝕜 𝕜'' F] →
                                                [inst_19 : SMulCommClass 𝕜' 𝕜'' F] → (E →L[𝕜] F) →L[𝕜''] E →L[𝕜'] F
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csInf_of_not_bddBelow : ∀ {s : Set ℤ}, ¬BddBelow s → sInf s = 0
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → Inhabited (CategoryTheory.CommMon C)