mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.map_ofComp_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [Nontrivial S],
  (Algebra.Extension.Cotangent.map
        ((Algebra.Generators.localizationAway S (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D)).ofComp
            (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toGenerators).toExtensionHom)
      (Algebra.Extension.Cotangent.mk
        ⟨(Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D).relation (Sum.inl ()), ⋯⟩) =
    Algebra.Generators.cMulXSubOneCotangent S (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.comm 𝕜 E F) x‖ = ‖x‖
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ofList_cons : ∀ {α : Type u} (a : α) (l : List α), ↑(a :: l) = Stream'.Seq.cons a ↑l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The functions from a monoid `M` to itself equivariant with respect to the right `M`-action
are exactly left multiplications by elements of `M`. See also `RingEquiv.moduleEndSelfOp`.  -/
MulActionHom.End.mulOppositeEquiv : {M : Type u_2} → [inst : Monoid M] → (M →ₑ[id] M) ≃* M
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.const.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : ℕ), sizeOf (Lean.Meta.DiscrTree.Key.const a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f : M → G} {s : Set M}, ContMDiffOn I' I n f s → ContMDiffOn I' I n (fun x => (f x)⁻¹) s
-- Mathlib.Order.Max
/-- Order without bottom elements.  -/
NoBotOrder : (α : Type u_3) → [LE α] → Prop
-- Mathlib.Order.Hom.Basic
/-- Identity order isomorphism.  -/
OrderIso.refl : (α : Type u_6) → [inst : LE α] → α ≃o α
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_le : ∀ {a b : UInt32}, a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The topology of the Lévy-Prokhorov metric is at least as fine as the topology of convergence in
distribution.  -/
MeasureTheory.LevyProkhorov.le_convergenceInDistribution : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  TopologicalSpace.coinduced MeasureTheory.LevyProkhorov.toMeasure inferInstance ≤ inferInstance
-- Mathlib.Analysis.Complex.Basic
RCLike.summable_ofReal : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ},
  Summable (fun x => ↑(f x)) L ↔ Summable f L
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_add_two : ∀ (n : ℕ), (n + 2).doubleFactorial = (n + 2) * n.doubleFactorial
-- Mathlib.Order.PrimeIdeal
Order.Ideal.isPrime_iff : ∀ {P : Type u_1} [inst : Preorder P] (I : Order.Ideal P), I.IsPrime ↔ I.IsProper ∧ Order.IsPFilter (↑I)ᶜ
-- Mathlib.Data.List.Chain
List.IsChain.imp_head : ∀ {α : Type u_1} {R : α → α → Prop} {x y : α},
  (∀ {z : α}, R x z → R y z) → ∀ {l : List α}, List.IsChain R (x :: l) → List.IsChain R (y :: l)
-- Mathlib.Tactic.Widget.StringDiagram
/-- Given an expression, return the kind of the context.  -/
Mathlib.Tactic.Widget.StringDiagram.mkKind : Lean.Expr → Lean.MetaM Mathlib.Tactic.Widget.StringDiagram.Kind
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.is_homogeneous' : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  (self : HomogeneousSubmodule 𝒜 ℳ), self.IsHomogeneous ℳ
-- Std.Sat.AIG.CNF
/-- Produce a Tseitin style CNF for a `Decl.gate`, using `output` as the tree node variable.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.gateToCNF : {α : Type u_1} → α → α → α → Bool → Bool → Std.Sat.CNF α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.decidableMemMker : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : AddMonoidHomClass F M N] → [DecidableEq N] → (f : F) → DecidablePred fun x => x ∈ AddMonoidHom.mker f
-- Init.Internal.Order.While
/-- One-step unfolding of `Lean.Loop.forIn` for any `MonadTail m`.  -/
Lean.Loop.forIn_eq_of_monadTail : ∀ {m : Type u → Type v} [inst : Monad m] {β : Type u} [LawfulMonad m] [Lean.Order.MonadTail m] {l : Lean.Loop} {b : β}
  {f : Unit → β → m (ForInStep β)},
  l.forIn b f = do
    let __do_lift ← f () b
    match __do_lift with
      | ForInStep.done val => pure val
      | ForInStep.yield val => l.forIn val f
-- Lean.Meta.Tactic.Grind.Util
/-- Throws an exception if target of the given goal contains metavariables.
 -/
Lean.MVarId.ensureNoMVar : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Data.List.Lattice
List.forall_mem_inter_of_forall_left : ∀ {α : Type u_1} {l₁ : List α} {p : α → Prop} [inst : DecidableEq α],
  (∀ x ∈ l₁, p x) → ∀ (l₂ : List α), ∀ x ∈ l₁ ∩ l₂, p x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, ∅.getKey! a = default
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_trans' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n),
  (h₁.trans h₂).symm = h₂.symm.trans h₁.symm
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.mk.injEq : ∀ {σ : Type} (idx : ℕ) (mkInitial : IO σ) (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (Lean.ReplayFn σ))
  (idx_1 : ℕ) (mkInitial_1 : IO σ) (asyncMode_1 : Lean.EnvExtension.AsyncMode) (replay?_1 : Option (Lean.ReplayFn σ)),
  ({ idx := idx, mkInitial := mkInitial, asyncMode := asyncMode, replay? := replay? } =
      { idx := idx_1, mkInitial := mkInitial_1, asyncMode := asyncMode_1, replay? := replay?_1 }) =
    (idx = idx_1 ∧ mkInitial = mkInitial_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1)
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of the forward direction of `AffineSubspace.wSameSide_comm`. -/
AffineSubspace.WSameSide.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WSameSide x y → s.WSameSide y x
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_1 : ∀ (x x_1 : ℕ), hyperoperation 0 x x_1 = x_1 + 1
-- Mathlib.Data.Nat.Choose.Factorization
/-- A lower bound on the factorization of `p` in `choose n k`.  -/
Nat.factorization_le_factorization_choose_add : ∀ {p n k : ℕ}, k ≤ n → k ≠ 0 → n.factorization p ≤ (n.choose k).factorization p + k.factorization p
-- Mathlib.SetTheory.Lists
Lists'.cons_subset : ∀ {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true}, Lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesWithinOnBall_insert_self : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p (insert x s) x r ↔ HasFPowerSeriesWithinOnBall f p s x r
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.eq_homEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B)
  (g : A ⟶ G.obj B), g = (adj.homEquiv A B) f ↔ (adj.homEquiv A B).symm g = f
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.andthen.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant.congr_simp : ∀ {n : ℕ} (original_assignments original_assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (e_original_assignments : original_assignments = original_assignments_1)
  (original_assignments_size : original_assignments.size = n)
  (units units_1 : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
  units = units_1 →
    ∀ (assignments assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
      (e_assignments : assignments = assignments_1) (assignments_size : assignments.size = n),
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant original_assignments
          original_assignments_size units assignments assignments_size =
        Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant original_assignments_1 ⋯ units_1
          assignments_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  LinearMap.toMatrixAlgEquiv v₁ = AlgEquiv.ofLinearEquiv (LinearMap.toMatrix v₁ v₁) ⋯ ⋯
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ioo_mul_eq_prod_Ioc : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → (∏ x ∈ Finset.Ioo a b, f x) * f b = ∏ x ∈ Finset.Ioc a b, f x
-- Init.System.Promise
_private.Init.System.Promise.0.IO.PromisePointed : NonemptyType
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMonadMor₁BicategoryM : Mathlib.Tactic.BicategoryLike.MonadMor₁ Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.comp_assoc : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {Y : Type u_4} {G : SimpleGraph V} {G' : SimpleGraph W}
  {G'' : SimpleGraph X} {G''' : SimpleGraph Y} (f : G'' ≃g G''') (g : G' ≃g G'') (h : G ≃g G'),
  f.comp (g.comp h) = (f.comp g).comp h
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.map_subgraphOfAdj : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v w : V} (hvw : G.Adj v w),
  SimpleGraph.Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯
-- Mathlib.Data.FunLike.Graded
GradedEquivLike.map_mem_iff : ∀ {E : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {σ : outParam (Type u_4)} {τ : outParam (Type u_5)}
  {ι : outParam (Type u_6)} {inst : SetLike σ A} {inst_1 : SetLike τ B} {𝒜 : outParam (ι → σ)} {ℬ : outParam (ι → τ)}
  {inst_2 : EquivLike E A B} [self : GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι} {x : A}, e x ∈ ℬ i ↔ x ∈ 𝒜 i
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.normedAddCommGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F],
  Prod.normedAddCommGroup =
    { toNorm := Prod.seminormedAddGroup.toNorm, toAddGroup := Prod.seminormedAddGroup.toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := Prod.seminormedAddGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Given a box `I` in `ℝⁿ` and a function `r : ℝⁿ → (0, ∞)`, there exists a tagged partition `π` of
`I` such that

* `π` is a Henstock partition;
* `π` is subordinate to `r`;
* each box in `π` is homothetic to `I` with coefficient of the form `1 / 2 ^ m`.

This lemma implies that the Henstock filter is nontrivial, hence the Henstock integral is
well-defined.  -/
BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J ∈ π, ∃ m, ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) ∧
            π.distortion = I.distortion
-- Mathlib.RingTheory.FractionalIdeal.Basic
IsFractional.nsmul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : Submodule R P} (n : ℕ), IsFractional S I → IsFractional S (n • I)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_rightUnshift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {a n' : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn' : n' + a = n), (γ.rightUnshift n hn').rightShift a n' hn' = γ
-- Init.Data.List.TakeDrop
List.splitAt_eq : ∀ {α : Type u_1} {i : ℕ} {l : List α}, List.splitAt i l = (List.take i l, List.drop i l)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.add_smul : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (a b : R) (f : M →ₚₗ[R] N), (a + b) • f = a • f + b • f
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} {d₀ : K.X 0 ⟶ L.X 0}
  {comp_d₀ : CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀ = 0}
  {d₀_comp : CategoryTheory.CategoryStruct.comp d₀ (L.d 0 1) = 0} {d₀_1 : K.X 0 ⟶ L.X 0}
  {comp_d₀_1 : CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀_1 = 0}
  {d₀_comp_1 : CategoryTheory.CategoryStruct.comp d₀_1 (L.d 0 1) = 0},
  { d₀ := d₀, comp_d₀ := comp_d₀, d₀_comp := d₀_comp } = { d₀ := d₀_1, comp_d₀ := comp_d₀_1, d₀_comp := d₀_comp_1 } →
    d₀ = d₀_1
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.transpose_apply : ∀ {R : Type u_1} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_4}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (u : M →ₗ[R] M') (l : Module.Dual R M'),
  (Module.Dual.transpose u) l = l ∘ₗ u
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_top_iff : ∀ {ι : Type u_5} {α : Type u_7} [inst : LinearOrder α] [inst_1 : BoundedOrder α] [Nontrivial α] {s : Finset ι}
  {f : ι → α}, s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a cone `c` over `F`, we can interpret the legs of `c` as structured arrows
`c.pt ⟶ F.obj -`.  -/
CategoryTheory.Limits.Cone.toStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) → CategoryTheory.Functor J (CategoryTheory.StructuredArrow c.pt F)
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq : ∀ (k G : Type u) [inst : CommRing k] (n : ℕ) [inst_1 : Group G],
  CategoryTheory.CategoryStruct.comp (Rep.barComplex.d k G n) (Rep.diagonalSuccIsoFree k G n).inv =
    CategoryTheory.CategoryStruct.comp (Rep.diagonalSuccIsoFree k G (n + 1)).inv ((Rep.standardComplex k G).d (n + 1) n)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extends `PolynomialLaw.isCompat_apply'` to all universes.  -/
PolynomialLaw.isCompat_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) {T : Type w} [inst_7 : CommSemiring T] [inst_8 : Algebra R T] (h : S →ₐ[R] T)
  (t : TensorProduct R S M),
  (LinearMap.rTensor N h.toLinearMap) (PolynomialLaw.toFun S f t) =
    PolynomialLaw.toFun T f ((LinearMap.rTensor M h.toLinearMap) t)
-- Mathlib.ModelTheory.PartialEquiv
/-- Maps to the symmetric partial equivalence.  -/
FirstOrder.Language.PartialEquiv.symm : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.PartialEquiv M N → L.PartialEquiv N M
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsSStronglyConnected.exists_pos_path : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsSStronglyConnected V → ∀ (i j : V), ∃ p, 0 < p.length
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_closure : ∀ {G : Type u_2} [inst : Group G] (s : Set G), (Subgroup.closure s).op = Subgroup.closure (MulOpposite.unop ⁻¹' s)
-- Init.Data.Int.Gcd
Int.lcm_mul_left_right : ∀ (a b : ℤ), a.lcm (b * a) = b.natAbs * a.natAbs
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingSurjectiveEquiv_symm_apply_coe_apply : ∀ {α : Sort u_1} {β : Type u_2} (f : α ≃ β) (a : α), ↑(Equiv.embeddingSurjectiveEquiv.symm f) a = f a
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The inclusion `S ⊗ Y ⟶ S.unionProd T` as simplicial sets  -/
SSet.Subcomplex.unionProd.ι₂ : {X Y : SSet} →
  (S : X.Subcomplex) →
    (T : Y.Subcomplex) → CategoryTheory.MonoidalCategoryStruct.tensorObj S.toSSet Y ⟶ (S.unionProd T).toSSet
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the first left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction₂.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₂ X Y) → X ⟶ self.Y'
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instFinite_countablePartition : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  Finite ↑(MeasurableSpace.countablePartition α n)
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `supClosure_eq_self`. -/
SupClosed.supClosure_eq : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, SupClosed s → supClosure s = s
-- Aesop.Rule.Name
Aesop.RuleName.phase : Aesop.RuleName → Aesop.PhaseName
-- Mathlib.Order.Bounds.Basic
not_bddBelow_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoBotOrder α], ¬BddBelow Set.univ
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.asteriskForm.sizeOf_spec : sizeOf Std.Http.RequestTarget.asteriskForm = 1
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_filter : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → Bool}
  {p : β → m Bool},
  Std.Iter.allM p (Std.Iter.filter f it) = Std.Iter.allM (fun x => if f x = true then p x else pure true) it
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.measurable_ofLp : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], Measurable WithLp.ofLp
-- Mathlib.ModelTheory.Syntax
/-- Applies a unary relation to a term as a bounded formula.  -/
FirstOrder.Language.Relations.boundedFormula₁ : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Relations 1 → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.getObjValAs? : Lean.Json → (α : Type u) → [Lean.FromJson α] → String → Except String α
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_pow_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (n : ℕ), UniformContinuous fun x => x ^ n
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Sigma.mk i` as a bundled continuous map.  -/
ContinuousMap.sigmaMk : {I : Type u_5} → {X : I → Type u_7} → [inst : (i : I) → TopologicalSpace (X i)] → (i : I) → C(X i, (i : I) × X i)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.MonadicRightAdjoint R],
  (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)).IsEquivalence
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.CoverPreserving.overPost : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} (X : C),
  CategoryTheory.CoverPreserving J K F →
    CategoryTheory.CoverPreserving (J.over X) (K.over (F.obj X)) (CategoryTheory.Over.post F)
-- Init.Data.Int.DivMod.Basic
Int.ofNat_ediv_ofNat : ∀ {a b : ℕ}, ↑a / ↑b = ↑(a / b)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instAddCommGroup : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → AddCommGroup (M →ₗ⁅R,L⁆ N)