mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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}
  (self : P.InvariantForm), LinearMap.IsSymm self.form
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_div_subset : ∀ {α : Type u_2} [inst : Div α] (S : Set (Set α)) (t : Set α), ⋂₀ S / t ⊆ ⋂ s ∈ S, s / t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p p_1 : G.Walk v w),
  p = p_1 → SimpleGraph.Walk.cons h p = SimpleGraph.Walk.cons h p_1
-- Mathlib.Data.EReal.Operations
EReal.mul_pos_iff : ∀ {a b : EReal}, 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.Data.Finset.Sum
Finset.Injective2_disjSum : ∀ {α : Type u_4} {β : Type u_5}, Function.Injective2 Finset.disjSum
-- Mathlib.Analysis.CStarAlgebra.Basic
IsSelfAdjoint.norm_pow_two_pow : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E},
  IsSelfAdjoint x → ∀ (n : ℕ), ‖x ^ 2 ^ n‖ = ‖x‖ ^ 2 ^ n
-- Mathlib.Topology.UniformSpace.Defs
/-- See also `isOpen_iff_isOpen_ball_subset`.  -/
isOpen_iff_ball_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, UniformSpace.ball x V ⊆ s
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.inter : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s.OrdConnected → t.OrdConnected → (s ∩ t).OrdConnected
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.termE_ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toOrderHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], Function.Injective OrderAddMonoidHom.toOrderHom
-- Mathlib.Algebra.BigOperators.Pi
eqOn_fun_finsetSum : ∀ {ι : Type u_8} {α : Type u_9} {β : Type u_10} [inst : AddCommMonoid α] {s : Set β} {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) →
    ∀ (v : Finset ι), Set.EqOn (fun b => ∑ i ∈ v, f i b) (fun b => ∑ i ∈ v, f' i b) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_append : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getEntry? a (l ++ l') = (Std.Internal.List.getEntry? a l).or (Std.Internal.List.getEntry? a l')
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.mk.sizeOf_spec : ∀ (assumptions : Array Lean.Elab.Tactic.Omega.Proof) (numVars : ℕ)
  (constraints : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact) (equalities : Std.HashSet Lean.Omega.Coeffs)
  (eliminations : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)) (possible : Bool)
  (proveFalse? : Option Lean.Elab.Tactic.Omega.Proof)
  (proveFalse?_spec :
    autoParam ((possible || proveFalse?.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam)
  (explanation? : Thunk String),
  sizeOf
      { assumptions := assumptions, numVars := numVars, constraints := constraints, equalities := equalities,
        eliminations := eliminations, possible := possible, proveFalse? := proveFalse?,
        proveFalse?_spec := proveFalse?_spec, explanation? := explanation? } =
    1 + sizeOf assumptions + sizeOf numVars + sizeOf constraints + sizeOf equalities + sizeOf eliminations +
            sizeOf possible +
          sizeOf proveFalse? +
        sizeOf proveFalse?_spec +
      sizeOf explanation?
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.hom.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Lean.Compiler.Old
/-- Return `some _` if the given name was created using `mkUnsafeRecName`  -/
Lean.Compiler.isUnsafeRecName? : Lean.Name → Option Lean.Name
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.FinitaryExtensive C]
  [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteColimits A],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.continuousOn : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁}, ContinuousOn (⇑e) s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α},
  (m.insertMany l)[k]? =
    (List.findSomeRev?
          (fun x_2 =>
            match x_2 with
            | (a, b) => if (a == k) = true then some b else none)
          l).or
      m[k]?
-- Mathlib.Analysis.Convex.Strong
/-- A function `f` from a real normed space is `m`-strongly concave if is strongly concave with
modulus `φ(r) = m / 2 * r ^ 2`.

In an inner product space, this is equivalent to `x ↦ f x + m / 2 * ‖x‖ ^ 2` being concave.  -/
StrongConcaveOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Set E → ℝ → (E → ℝ) → Prop
-- Mathlib.Logic.Equiv.Defs
Equiv.extend_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {f : α ≃ β} (g : α → γ) (e' : β → γ) (b : β),
  Function.extend (⇑f) g e' b = g (f.symm b)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instLocallyOfFinitePresentationResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.LocallyOfFinitePresentation f],
  AlgebraicGeometry.LocallyOfFinitePresentation (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.ContainsZero],
  P.unop.ContainsZero
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_iff_pos_imp_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.ins : ∀ {α : Type u_1} {cmp : α → α → Ordering} {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.Path.Ordered cmp path →
      RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t → RBTree.RBNode.Ordered cmp (path.ins t)
-- Aesop.RuleTac.Apply
Aesop.RuleTac.apply : Aesop.RuleTerm → Lean.Meta.TransparencyMode → Aesop.RuleTac
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  CategoryTheory.IsSeparator G →
    (CategoryTheory.MorphismProperty.monomorphisms C).rlp.llp = CategoryTheory.MorphismProperty.monomorphisms C
-- Lean.Server.References
Lean.Server.References.mk.sizeOf_spec : ∀ (ileans : Lean.Server.ILeanMap) (workers : Lean.Server.WorkerRefMap),
  sizeOf { ileans := ileans, workers := workers } = 1 + sizeOf ileans + sizeOf workers
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.toStructured? : {α : Type u_1} → [Lean.ToJson α] → α → Except String Lean.Json.Structured
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_X : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) (s : σ), (MvPolynomial.aeval f) (MvPolynomial.X s) = f s
-- Mathlib.Data.Nat.Init
Nat.stepInduction.eq_def : ∀ {motive : ℕ → Sort u_1} (k : ℕ) (base : (i : ℕ) → i < k → motive i)
  (step : (n : ℕ) → ((i : ℕ) → i < k → motive (n + i)) → motive (n + k)) (a : ℕ),
  Nat.stepInduction k base step a =
    if h : a < k then base a h else ⋯ ▸ step (a - k) fun x x_1 => Nat.stepInduction k base step (a - k + x)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.isDirectedOrder : ∀ (α : Type u) [inst : Preorder α] [CategoryTheory.IsFiltered α], IsDirectedOrder α
-- Mathlib.Topology.Connected.TotallyDisconnected
instTotallyDisconnectedSpaceAdditive : ∀ {α : Type u} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α], TotallyDisconnectedSpace (Additive α)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
/-- Kullback-Leibler divergence between two measures.  -/
InformationTheory.klDiv : {α : Type u_2} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → ENNReal
-- Lean.Data.Lsp.Internal
Lean.Lsp.DeclInfo.mk.injEq : ∀
  (rangeStartPosLine rangeStartPosCharacter rangeEndPosLine rangeEndPosCharacter selectionRangeStartPosLine
    selectionRangeStartPosCharacter selectionRangeEndPosLine selectionRangeEndPosCharacter rangeStartPosLine_1
    rangeStartPosCharacter_1 rangeEndPosLine_1 rangeEndPosCharacter_1 selectionRangeStartPosLine_1
    selectionRangeStartPosCharacter_1 selectionRangeEndPosLine_1 selectionRangeEndPosCharacter_1 : ℕ),
  ({ rangeStartPosLine := rangeStartPosLine, rangeStartPosCharacter := rangeStartPosCharacter,
        rangeEndPosLine := rangeEndPosLine, rangeEndPosCharacter := rangeEndPosCharacter,
        selectionRangeStartPosLine := selectionRangeStartPosLine,
        selectionRangeStartPosCharacter := selectionRangeStartPosCharacter,
        selectionRangeEndPosLine := selectionRangeEndPosLine,
        selectionRangeEndPosCharacter := selectionRangeEndPosCharacter } =
      { rangeStartPosLine := rangeStartPosLine_1, rangeStartPosCharacter := rangeStartPosCharacter_1,
        rangeEndPosLine := rangeEndPosLine_1, rangeEndPosCharacter := rangeEndPosCharacter_1,
        selectionRangeStartPosLine := selectionRangeStartPosLine_1,
        selectionRangeStartPosCharacter := selectionRangeStartPosCharacter_1,
        selectionRangeEndPosLine := selectionRangeEndPosLine_1,
        selectionRangeEndPosCharacter := selectionRangeEndPosCharacter_1 }) =
    (rangeStartPosLine = rangeStartPosLine_1 ∧
      rangeStartPosCharacter = rangeStartPosCharacter_1 ∧
        rangeEndPosLine = rangeEndPosLine_1 ∧
          rangeEndPosCharacter = rangeEndPosCharacter_1 ∧
            selectionRangeStartPosLine = selectionRangeStartPosLine_1 ∧
              selectionRangeStartPosCharacter = selectionRangeStartPosCharacter_1 ∧
                selectionRangeEndPosLine = selectionRangeEndPosLine_1 ∧
                  selectionRangeEndPosCharacter = selectionRangeEndPosCharacter_1)
-- Batteries.Data.Stream
/-- Tail recursive version of `Stream.take`.  -/
Std.Stream.takeTR : {σ : Type u_1} → {α : Type u_2} → [Std.Stream σ α] → σ → ℕ → List α × σ
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects
and checking compatibility with counit and comultiplication only in the forward direction.
 -/
CategoryTheory.Comon.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Comon C} → (f : M.X ≅ N.X) → [CategoryTheory.IsComonHom f.hom] → M ≅ N
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.functor_ext : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (h₁ :
    ∀ (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
      F.obj (SSet.Truncated.HomotopyCategory.mk x) = G.obj (SSet.Truncated.HomotopyCategory.mk x)),
  (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
      (e : SSet.Truncated.Edge x y),
      F.map (SSet.Truncated.HomotopyCategory.homMk e) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map (SSet.Truncated.HomotopyCategory.homMk e))
            (CategoryTheory.eqToHom ⋯))) →
    F = G
-- Mathlib.Algebra.Field.Basic
add_div' : ∀ {K : Type u_1} [inst : DivisionSemiring K] (a b c : K), c ≠ 0 → b + a / c = (b * c + a) / c
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Tor'_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X Y : C} (f : X ⟶ Y) (j : C),
  ((CategoryTheory.Tor' C n).map f).app j =
    (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).map f
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁' : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (hr : r₀ ≤ r) (pq' : κ)
  {i₀ i₁ : ι}, i₀ = data.i₀ r pq' ⋯ → i₁ = data.i₁ pq' → i₀ ≤ i₁
-- Init.Data.List.Lemmas
List.append_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → β},
  L₁ ++ L₂ = List.map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = L₁ ∧ List.map f l₂ = L₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f t[k]?).isSome = true else k' ∈ t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_eq_neg_pi_div_two_iff : ∀ {θ : Real.Angle}, θ.toReal = -Real.pi / 2 ↔ θ = ↑(-Real.pi / 2)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] (g : β →*₀ γ) (f : α →*₀ β), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasStrictFDerivAt_iff_isLittleO`. -/
HasStrictFDerivAt.isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofBitVec : ∀ (b : BitVec 64), { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a ≤ x` and `x < b`. Basically `Set.Ico a b` as a
multiset.  -/
Multiset.Ico : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Multiset α
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAtFilter_const_add_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter (fun x => c + f x) f' L ↔ HasDerivAtFilter f f' L
-- Mathlib.Order.Filter.Extr
IsMinFilter.filter_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
  IsMinFilter f l a → l' ≤ l → IsMinFilter f l' a
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.domMulActCongrRight_symm_apply : ∀ {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15}
  {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₁'] [inst_2 : Semiring R₂'] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₁'] [inst_5 : AddCommMonoid M₂'] [inst_6 : Module R₁ M₁] [inst_7 : Module R₁' M₁']
  [inst_8 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₁₂' : R₁ →+* R₂'}
  [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_11 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_12 : Semiring S] [inst_13 : Module S M₁]
  [inst_14 : SMulCommClass R₁ S M₁] [inst_15 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂')
  (a : M₁ →ₛₗ[σ₁₂'] M₂'), e₂.domMulActCongrRight.symm a = ((LinearEquiv.refl R₁ M₁).arrowCongrAddEquiv e₂).invFun a
-- Mathlib.Order.Ideal
Order.Ideal.isProper_iff : ∀ {P : Type u_1} [inst : LE P] (I : Order.Ideal P), I.IsProper ↔ ↑I ≠ Set.univ
-- Mathlib.Algebra.Algebra.Operations
Submodule.instIsScalarTower : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α A] [inst_5 : SMulCommClass α R A] [IsScalarTower α A A],
  IsScalarTower α (Submodule R A) (Submodule R A)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.toLetValue : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.ker_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.QuasiCompact f] (U : ↑Y.affineOpens),
  f.ker.ideal U = RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_mul_mul_comm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M] {Z : C}
  (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_TFAE : ∀ (α : Type u_1) [inst : TopologicalSpace α],
  [TopologicalSpace.NoetherianSpace α, WellFoundedLT (TopologicalSpace.Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s].TFAE
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.instAddCommGroupStandardOneDimIsocrystal : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) → [inst_1 : CommRing k] → (_m : ℤ) → AddCommGroup (WittVector.StandardOneDimIsocrystal p k _m)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.vsub_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f g : P1 →ᵃ[k] P2) (p : P1), (f -ᵥ g) p = f p -ᵥ g p
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regulator_pos : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 < NumberField.Units.regulator K
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- Composition of reflective functors.  -/
CategoryTheory.Reflective.comp : {C : Type u₁} →
  {D : Type u₂} →
    {E : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Reflective F] → [CategoryTheory.Reflective G] → CategoryTheory.Reflective (F.comp G)
-- Mathlib.Data.Num.ZNum
PosNum.div'_to_nat : ∀ (n d : PosNum), ↑(n.div' d) = ↑n / ↑d
-- Mathlib.Probability.Moments.MGFAnalytic
/-- For `t ∈ interior (integrableExpSet X μ)`, the derivative of `mgf X μ` at `t` is
`μ[X * exp (t * X)]`.  -/
ProbabilityTheory.hasDerivAt_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    HasDerivAt (ProbabilityTheory.mgf X μ) (∫ (x : Ω), (fun ω => X ω * Real.exp (t * X ω)) x ∂μ) t
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.comp_mapCommMon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.MonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E}
  [inst_9 : F.LaxBraided] [inst_10 : G.LaxBraided] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
      ((F.comp G).map CategoryTheory.MonObj.mul)
-- Mathlib.Topology.Algebra.Order.UpperLower
IsOrderedAddMonoid.to_hasUpperLowerClosure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : Preorder α] [IsOrderedAddMonoid α]
  [ContinuousConstVAdd α α], HasUpperLowerClosure α
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_neg : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddGroup (G i)] [inst_3 : ∀ (i : ι), AddSubgroupClass (S i) (G i)]
  (i : ι) (r : G i), RestrictedProduct.single A i (-r) = -RestrictedProduct.single A i r
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_natCast_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R} {n : ℕ},
  Polynomial.eval x (↑n * p) = ↑n * Polynomial.eval x p
-- Init.Data.UInt.Lemmas
UInt16.le_or_lt : ∀ (a b : UInt16), a ≤ b ∨ b < a
-- Mathlib.RingTheory.Multiplicity
/-- A `ℕ`-valued version of `emultiplicity`, returning `1` instead of `⊤`.  -/
multiplicity : {α : Type u_1} → [Monoid α] → α → α → ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true →
    Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k m₂ = true