mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- The Frobenius morphism for an adjunction `L ⊣ F` at `A` is given by the morphism

    L(FA ⨯ B) ⟶ LFA ⨯ LB ⟶ A ⨯ LB

natural in `B`, where the first morphism is the product comparison and the latter uses the counit
of the adjunction.

We will show that if `C` and `D` are Cartesian closed, then this morphism is an isomorphism for all
`A` iff `F` is a Cartesian closed functor, i.e. it preserves exponentials.
 -/
CategoryTheory.frobeniusMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} D] →
        [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              {L : CategoryTheory.Functor D C} →
                (L ⊣ F) →
                  (A : C) →
                    CategoryTheory.TwoSquare (CategoryTheory.MonoidalCategory.tensorLeft (F.obj A)) L L
                      (CategoryTheory.MonoidalCategory.tensorLeft A)
-- Mathlib.Data.PFun
PFun.core_inter : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : Set β), f.core (s ∩ t) = f.core s ∩ f.core t
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} [inst_3 : Inhabited (β a)] {v : β k},
      (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub_left' : ∀ {n a b c : ℕ}, (b ≤ a ↔ c ≤ a) → b ≡ c [MOD n] → a - b ≡ a - c [MOD n]
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesMonomorphisms_π₃ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C],
  CategoryTheory.ShortComplex.π₃.PreservesMonomorphisms
-- Lean.Data.PersistentArray
Lean.PersistentArray.mk : {α : Type u} → Lean.PersistentArrayNode α → Array α → ℕ → USize → ℕ → Lean.PersistentArray α
-- Lean.Parser.Basic
Lean.Parser.takeWhileFn : (Char → Bool) → Lean.Parser.ParserFn
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_injective : ∀ {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 : EuclideanGeometry.Sphere P), Function.Injective s.orthRadius
-- Std.Internal.UV.TCP
/-- Returns an `IO.Promise` that resolves to `true` once `socket` has data available for reading,
or to `false` if `socket` is closed before that. Calling this function twice on the same `Socket`
or in parallel with `recv?` is not supported.
 -/
Std.Internal.UV.TCP.Socket.waitReadable : Std.Internal.UV.TCP.Socket → IO (IO.Promise (Except IO.Error Bool))
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_inj : ∀ {a b : UpperHalfPlane}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.below.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} (x : α),
  CategoryTheory.IsCofiltered.cofilteredClosure.below ⋯
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.instIsDenseSubsiteOverLeftOverInverseIteratedSliceEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (f : CategoryTheory.Over X),
  CategoryTheory.Functor.IsDenseSubsite (J.over f.left) ((J.over X).over f) f.iteratedSliceEquiv.inverse
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.neg : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α}, Summable f L → Summable (fun b => -f b) L
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdUnique_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique β] (a : α), (LinearIsometryEquiv.withLpProdUnique p 𝕜 α β).symm a = WithLp.toLp p (a, default)
-- Lean.Elab.Do.Switch
_private.Lean.Elab.Do.Switch.0.Lean.Elab.Term.toDoElem : Lean.SyntaxNodeKind → Lean.Macro
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.add_congr.wl : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Add α] [Lean.Grind.ToInt.Add α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = i.wrap a' → ↑b = b' → ↑(a + b) = i.wrap (a' + b')
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_sq_inner_left : ∀ {ι : Type u_7} {E : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fintype ι]
  (b : OrthonormalBasis ι ℝ E) (x : E), ∑ i, inner ℝ x (b i) ^ 2 = ‖x‖ ^ 2
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The recurrence relation for the `Γ` integral.  -/
Complex.GammaIntegral_add_one : ∀ {s : ℂ}, 0 < s.re → (s + 1).GammaIntegral = s * s.GammaIntegral
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.subset_closure_sdiff_singleton : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → ∀ (e : α), C ⊆ M.closure (C \ {e})
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.instIsRootSystemFlip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsRootSystem],
  P.flip.IsRootSystem
-- Lean.Attributes
/-- `getNumBuiltinAttributes` implementation  -/
Lean.getNumBuiltinAttributesImpl : IO ℕ
-- Batteries.Recycling.RBTree.Basic
/-- Fold a function on the values from left to right (in increasing order).  -/
RBTree.RBNode.foldl : {σ : Sort u_1} → {α : Type u_2} → (σ → α → σ) → σ → RBTree.RBNode α → σ
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.Result.map.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_1 a s'
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.type_eq_of_isCofinal : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α},
  IsCofinal s → (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instTopologicalSpace : {G : Type u_1} → [TopologicalSpace G] → [inst : AddGroup G] → (N : AddSubgroup G) → TopologicalSpace (G ⧸ N)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.cocyclesMkOfCompEqD.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} {y y_1 : (Fin i → G) → ↑X.X₂} (e_y : y = y_1) {x x_1 : (Fin j → G) → ↑X.X₁}
  (e_x : x = x_1)
  (hx :
    ⇑(Rep.Hom.hom X.f) ∘ x =
      (CategoryTheory.ConcreteCategory.hom ((groupCohomology.inhomogeneousCochains X.X₂).d i j)) y),
  groupCohomology.cocyclesMkOfCompEqD hX hx = groupCohomology.cocyclesMkOfCompEqD hX ⋯
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.HasLimits.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections],
  MonCat.HasLimits.limitCone F =
    { pt := MonCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt,
      π := { app := fun j => MonCat.ofHom (MonCat.limitπMonoidHom F j), naturality := ⋯ } }
-- Mathlib.Data.Finset.Basic
Finset.range_inter_range : ∀ (m n : ℕ), Finset.range m ∩ Finset.range n = Finset.range (min m n)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
cexp_neg_quadratic_isLittleO_abs_rpow_cocompact : ∀ {a : ℂ},
  a.re < 0 → ∀ (b : ℂ) (s : ℝ), (fun x => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.cocompact ℝ] fun x => |x| ^ s
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.det_mapGL : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (g : Matrix.SpecialLinearGroup n R),
  Matrix.GeneralLinearGroup.det ((Matrix.SpecialLinearGroup.mapGL S) g) = 1
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_entry_le_entrywise_sup_nnnorm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α) {i : m} {j : n}, ‖A i j‖₊ ≤ ‖A‖₊
-- Std.Time.Zoned.RecurringRule
/-- DST UTC offset (east-positive).
 -/
Std.Time.TimeZone.DaylightSavingRule.offset : Std.Time.TimeZone.DaylightSavingRule → Std.Time.TimeZone.Offset
-- Mathlib.Analysis.Seminorm
Seminorm.ball_zero_eq_preimage_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interLift_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S}
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F)
  (i : G.I₀),
  (CategoryTheory.PreZeroHypercover.interLift f g).h₀ i = CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_inv_app : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C),
  (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).inv.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
/-- Bundle `WithLp.unitization_addEquiv_prod` as a `UniformEquiv`.  -/
WithLp.uniformEquiv_unitization_addEquiv_prod : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] → [inst_2 : NormedSpace 𝕜 A] → WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instNonUnitalRingHomClass : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B], NonUnitalRingHomClass (A →⋆ₙ+* B) A B
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C)
  (X_1 : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj X_1))
-- Init.Data.Bool
Bool.le_total : ∀ (x y : Bool), x ≤ y ∨ y ≤ x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.LeftAdjoint.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {right : b ⟶ a} →
        (left : a ⟶ b) → CategoryTheory.Bicategory.Adjunction left right → CategoryTheory.Bicategory.LeftAdjoint right
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.inv_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant], (MeasureTheory.ae μ)⁻¹ = MeasureTheory.ae μ
-- Mathlib.Algebra.Ring.Defs
Distrib.mk : {R : Type u_1} →
  [toMul : Mul R] →
    [toAdd : Add R] →
      (∀ (a b c : R), a * (b + c) = a * b + a * c) → (∀ (a b c : R), (a + b) * c = a * c + b * c) → Distrib R
-- Batteries.Data.List.Lemmas
List.swap_comm : ∀ {α : Type u_1} {xs : List α} {i j : ℕ}, xs.swap i j = xs.swap j i
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_counitIso_hom_app_app : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (X_1 : CategoryTheory.Functor X Y) (X_2 : X),
  (OrderHom.equivalenceFunctor.counitIso.hom.app X_1).app X_2 = CategoryTheory.CategoryStruct.id (X_1.obj X_2)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.π_ofπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y P : C}
  (f : X ⟶ Y) (π : Y ⟶ P) (w : CategoryTheory.CategoryStruct.comp f π = 0),
  CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.CokernelCofork.ofπ π w) = π
-- Lean.Level
Lean.Level.Data.depth : Lean.Level.Data → UInt32
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.Pairwise.isChain`. -/
List.Pairwise.chain : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l → List.IsChain R l
-- Mathlib.Order.Atoms
/-- A simple partial ordered `BoundedOrder` induces a linear order.
This is not an instance to prevent loops.  -/
IsSimpleOrder.linearOrder : {α : Type u_2} →
  [inst : PartialOrder α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → [DecidableEq α] → LinearOrder α
-- Init.Data.String.TakeDrop
String.nextWhile : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Order.Interval.Finset.Nat
/-- Note that while this lemma cannot be easily generalized to a type class, it holds for ℤ as
well. See `Int.image_Ico_emod` for the ℤ version.  -/
Nat.image_Ico_mod : ∀ (n a : ℕ), Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.range a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] [inst_3 : Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKey! k = ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).get!
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (Φ₁ Φ₂ : S₁.Hom S₂), (∀ (n : ℕ), Φ₁.f n = Φ₂.f n) → Φ₁ = Φ₂
-- Mathlib.Topology.Category.Compactum
Compactum.str_incl : ∀ (X : Compactum) (x : X.A), X.str (X.incl x) = x
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.CategoryStruct.comp.hcongr_7 : ∀ (obj obj' : Type u),
  obj = obj' →
    ∀ (self : CategoryTheory.CategoryStruct.{v, u} obj) (self' : CategoryTheory.CategoryStruct.{v, u} obj'),
      self ≍ self' →
        ∀ (X : obj) (X' : obj'),
          X ≍ X' →
            ∀ (Y : obj) (Y' : obj'),
              Y ≍ Y' →
                ∀ (Z : obj) (Z' : obj'),
                  Z ≍ Z' →
                    ∀ (a : X ⟶ Y) (a' : X' ⟶ Y'),
                      a ≍ a' →
                        ∀ (a_1 : Y ⟶ Z) (a'_1 : Y' ⟶ Z'),
                          a_1 ≍ a'_1 →
                            CategoryTheory.CategoryStruct.comp a a_1 ≍ CategoryTheory.CategoryStruct.comp a' a'_1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → x ≤ᵥ y
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center_eq_top : ∀ (R : Type u_1) [inst : CommRing R], Subring.center R = ⊤
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_zero_eq_singleton : (*...=0).toArray = #[0]
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_eq_get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h : k ∈ m}, m.get k h = (m.get? k).get ⋯
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.lt_of_parseLowerHex?_eq_some : ∀ {k : ℕ} {s : String} {p q : s.Pos} {acc r : ℕ}, 0 < k → Lean.parseLowerHex?✝ k s p acc = some (q, r) → p < q
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.forall_mem_sup : ∀ {C : Type u_2} [inst : CommGroup C] {s t : Subgroup C} {P : C → Prop},
  (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
-- Lean.Util.CollectFVars
Lean.CollectFVars.State : Type
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsAddApply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂],
  IsAddApply (M₁ →SL[σ₁₂] M₂) M₁ M₂
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.eq_1 : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  IsStronglyTranscendental R x =
    ∀ (u : S) (p : Polynomial R),
      (Polynomial.aeval x) p * u = 0 → Polynomial.map (algebraMap R S) p * Polynomial.C u = 0
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G ⧸ S`-representation on
the coinvariants of `ρ|_S`.  -/
Representation.quotientToCoinvariants : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [inst_4 : S.Normal] →
                    Representation k (G ⧸ S) (Representation.Coinvariants (MonoidHom.comp ρ S.subtype))
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeContainsMVar : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `filterMap` which can be used in the absence of balance
information but still assumes the preconditions of `filterMap`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.filterMap! : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      [Ord α] → ((a : α) → β a → Option (γ a)) → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α γ
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasurableEmbedding.integrableOn_iff_comap : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] {e : α → β},
  MeasurableEmbedding e →
    ∀ {f : β → ε} {μ : MeasureTheory.Measure β} {s : Set β},
      s ⊆ Set.range e →
        (MeasureTheory.IntegrableOn f s μ ↔
          MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) (MeasureTheory.Measure.comap e μ))
-- Mathlib.Algebra.Homology.Single
CochainComplex.fromSingle₀Equiv.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V),
  C.fromSingle₀Equiv X =
    { toFun := fun φ => ⟨φ.f 0, ⋯⟩, invFun := fun f => HomologicalComplex.mkHomFromSingle ↑f ⋯, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Logic.Lemmas
iff_assoc : ∀ {a b c : Prop}, ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
-- Init.Data.SInt.Lemmas
Int32.toUInt32_add : ∀ (a b : Int32), (a + b).toUInt32 = a.toUInt32 + b.toUInt32
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Any isomorphism between objects of `P.Comma L R Q W` in `Comma L R` is also an isomorphism
in `P.Comma L R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.isoFromComma : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                                (X.toComma ≅ Y.toComma) → (X ≅ Y)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Nested monoid algebras can be taken in an arbitrary order.  -/
AddMonoidAlgebra.commAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddMonoid M] →
                [inst_4 : AddMonoid N] →
                  AddMonoidAlgebra (AddMonoidAlgebra A M) N ≃ₐ[R] AddMonoidAlgebra (AddMonoidAlgebra A N) M
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_zero_right : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G), SkewMonoidAlgebra.single a 0 = 0
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β} {s : Set α} {t : Set β},
  s ∈ f → t ∈ g → s +ᵥ t ∈ f +ᵥ g
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.eq_conj_prod_map' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] E} (h : LinearMap.IsProj p f),
  f = ↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ LinearMap.id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯).symm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α}
  {k : α}, k ∈ t → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey? k = t.getKey? k
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow' : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ),
  h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.rank_eq_of_surjective : ∀ {R : Type u_1} {M M₁ : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
  [inst_3 : Module R M] [inst_4 : Module R M₁] [HasRankNullity.{u, u_1} R] {f : M →ₗ[R] M₁},
  Function.Surjective ⇑f → Module.rank R M = Module.rank R M₁ + Module.rank R ↥f.ker
-- Mathlib.Analysis.LConvolution
/-- Convolution is associative.  -/
MeasureTheory.mlconvolution_assoc : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {f g k : G → ENNReal},
  Measurable f →
    Measurable g →
      Measurable k →
        MeasureTheory.mlconvolution f (MeasureTheory.mlconvolution g k μ) μ =
          MeasureTheory.mlconvolution (MeasureTheory.mlconvolution f g μ) k μ
-- Mathlib.Topology.Maps.Proper.Basic
/-- The identity is proper.  -/
isProperMap_id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsProperMap id
-- Mathlib.Order.Category.BddOrd
BddOrd.ext_iff : ∀ {X Y : BddOrd} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Data.Sym.Sym2.Order
/-- In a linear order, two symmetric squares are equal if and only if
they have the same infimum and supremum.  -/
Sym2.inf_eq_inf_and_sup_eq_sup : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Sym2 α}, s.inf = t.inf ∧ s.sup = t.sup ↔ s = t