mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Support
mulTSupport_fun_inv : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : DivisionMonoid α] (f : X → α),
  (mulTSupport fun x => (f x)⁻¹) = mulTSupport f
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_ciInf : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {f : ι → α},
  Antitone f → BddBelow (Set.range f) → Filter.Tendsto f Filter.atTop (nhds (⨅ i, f i))
-- Mathlib.CategoryTheory.Equivalence
/-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is
an isomorphism, then there is an equivalence of categories whose inverse is `G`.  -/
CategoryTheory.Equivalence.changeInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → {G : CategoryTheory.Functor D C} → (e.inverse ≅ G) → (C ≌ D)
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.OfNat (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Init.Data.List.Lex
List.lex_lt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, List.Lex (fun x1 x2 => x1 < x2) l₁ l₂ ↔ l₁ < l₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Logic.Function.Basic
Function.Surjective.forall : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
  Function.Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
-- Lean.Elab.AutoBound
/-- This always matches the `autoImplicit` option; it is duplicated here in
order to support the behavior of the deprecated `Lean.Elab.Term.Context.autoImplicit`
method.
 -/
Lean.Elab.AutoBoundImplicitContext.autoImplicitEnabled : Lean.Elab.AutoBoundImplicitContext → Bool
-- Mathlib.Topology.Algebra.Monoid
tendsto_multiset_prod : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : CommMonoid M] [ContinuousMul M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) →
    Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).prod) x (nhds (Multiset.map a s).prod)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.isPrime_of_prime : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A}, Prime P → P.IsPrime
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableDSimpArgs : Hashable Lean.Elab.Tactic.Grind.DSimpArgs
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- The dimension of a strict submodule is strictly bounded by the dimension of the ambient
space.

See also `Submodule.length_lt`.  -/
Submodule.finrank_lt : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {s : Submodule K V}, s ≠ ⊤ → Module.finrank K ↥s < Module.finrank K V
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.Hom.mk.sizeOf_spec : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} [inst_2 : SizeOf k]
  [inst_3 : SizeOf G] (hom' : A.ρ.IntertwiningMap B.ρ), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.Compatible.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (f : P ⟶ Q) {x : CategoryTheory.Presieve.FamilyOfElements P R},
  x.Compatible → (x.map f).Compatible
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_union_neg_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s ∪ (-c +ᵥ t)) = μ ((c +ᵥ s) ∪ t)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `normalizeIso`. Here we construct the isomorphism between
`n ⊗ X` and `normalize X n`.  -/
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp : (C : Type u) →
  (X : CategoryTheory.FreeMonoidalCategory C) →
    (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
      ((CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj X).obj n ≅
        ((CategoryTheory.FreeMonoidalCategory.normalize' C).obj X).obj n
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_pf_left : ∀ {R : Type u_1} [inst : CommSemiring R] {a₃ b c : R} (a₁ : R) (a₂ : ℕ), a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}, ⊤.IsLocalAtTarget K
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.MVarId.apply.go.match_1.eq_1 : ∀ (motive : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr → Sort u_1) (newMVars : Array Lean.Expr)
  (binderInfos : Array Lean.BinderInfo) (eType : Lean.Expr)
  (h_1 :
    (newMVars : Array Lean.Expr) →
      (binderInfos : Array Lean.BinderInfo) → (eType : Lean.Expr) → motive (newMVars, binderInfos, eType)),
  (match (newMVars, binderInfos, eType) with
    | (newMVars, binderInfos, eType) => h_1 newMVars binderInfos eType) =
    h_1 newMVars binderInfos eType
-- Mathlib.Logic.Equiv.Basic
Equiv.comp_swap_eq_update : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] (i j : α) (f : α → β),
  f ∘ ⇑(Equiv.swap i j) = Function.update (Function.update f j (f i)) i (f j)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Second.Offset`.
 -/
Std.Time.Nanosecond.Offset.toSeconds : Std.Time.Nanosecond.Offset → Std.Time.Second.Offset
-- Mathlib.Geometry.Euclidean.Projection
/-- The distance between a point and its orthogonal projection is
nonzero if it does not lie in the subspace.  -/
EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  p ∉ s → dist p ↑((EuclideanGeometry.orthogonalProjection s) p) ≠ 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadAutoImplicits.getAutoImplicits : {m : Type → Type} → [self : Lean.Elab.MonadAutoImplicits m] → m (Array Lean.Expr)
-- Mathlib.Analysis.Fourier.Notation
/-- `𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  -/
FourierTransform.term𝓕 : Lean.ParserDescr
-- Init.Data.Option.Lemmas
Option.pfilter_none : ∀ {α : Type u_1} {p : (a : α) → none = some a → Bool}, none.pfilter p = none
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Zₙ(G, A) ⟶ Zₙ(H, B)` sending `∑ aᵢ·gᵢ : Gⁿ →₀ A` to
`∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B`.  -/
groupHomology.cyclesMap : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (n : ℕ) → groupHomology.cycles A n ⟶ groupHomology.cycles B n
-- Mathlib.Order.UpperLower.Prod
IsUpperSet.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β},
  IsUpperSet s → IsUpperSet t → IsUpperSet (s ×ˢ t)
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_toAddSubmonoid : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N : Submodule R M}, (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHModInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.map.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (E : CategoryTheory.PreZeroHypercover S),
  CategoryTheory.PreZeroHypercover.map F E = { I₀ := E.I₀, X := fun i => F.obj (E.X i), f := fun i => F.map (E.f i) }
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.essSurjInducedFunctor : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D),
  (CategoryTheory.inducedFunctor ⇑e).EssSurj
-- Mathlib.MeasureTheory.Measure.Prod
MeasurableEquiv.prodAssoc.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ],
  MeasurableEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).maxKey! = t.maxKey!
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ring : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [Monoid M] → Ring (MonoidAlgebra R M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
      (CategoryTheory.Limits.pullback.fst f g) =
    h
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instCoeAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instCoeAddSubgroup = { coe := fun H => H.toAddSubgroup }
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_uniqueElim : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [inst_1 : Unique δ], Measurable uniqueElim
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.step_uLift : ∀ {α β : Type u} [inst : Std.Iterator α Id β] {it : Std.Iter β},
  it.uLift.step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield it'.uLift { down := out } ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip it'.uLift ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_roo_eq : ∀ {m n i : ℕ}, ((m<...n).toArray[i]?.isSome = true) = (i < n - (m + 1))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Square roots of operators, based on the non-unital continuous functional calculus.  -/
CFC.sqrt : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : NonUnitalRing A] →
      [inst_2 : TopologicalSpace A] →
        [inst_3 : StarRing A] →
          [inst_4 : Module ℝ A] →
            [inst_5 : SMulCommClass ℝ A A] →
              [inst_6 : IsScalarTower ℝ A A] →
                [StarOrderedRing A] →
                  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → [NonnegSpectrumClass ℝ A] → A → A
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_eq_top_iff : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ → (ProbabilityTheory.evariance X μ = ⊤ ↔ ¬MeasureTheory.MemLp X 2 μ)
-- Init.Data.UInt.Lemmas
UInt16.toNat_toUInt32 : ∀ (x : UInt16), x.toUInt32.toNat = x.toNat
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_notMem_fst : ∀ (σ : Type u_1) [inst : DecidableEq σ] {t : Finset σ × σ} (h : t.2 ∉ t.1),
  MvPolynomial.NewtonIdentities.pairMap✝ σ t = (Finset.cons t.2 t.1 h, t.2)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Iic_eq_integral_Iio' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x : X},
  μ {x} = 0 → ∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.tprod_prod : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → CommSemiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {κ : Type u_5} (s : Finset κ) (x : κ → (i : ι) → A i),
  (PiTensorProduct.tprod R) (∏ k ∈ s, x k) = ∏ k ∈ s, (PiTensorProduct.tprod R) (x k)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The topology of the Lévy-Prokhorov metric on probability measures on a separable space
coincides with the topology of convergence in distribution.  -/
MeasureTheory.LevyProkhorov.eq_convergenceInDistribution : ∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  [TopologicalSpace.SeparableSpace Ω],
  inferInstance = TopologicalSpace.coinduced MeasureTheory.LevyProkhorov.toMeasure inferInstance
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- The additive version of a multiplicativized additive monoid is add-equivalent to itself.  -/
AddEquiv.toAdditive_toMultiplicative : {G : Type u_2} → [inst : AddZeroClass G] → Additive (Multiplicative G) ≃+ G
-- Mathlib.Order.Fin.Tuple
Monotone.vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  Monotone f → a ≤ f 0 → Monotone (Matrix.vecCons a f)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.sub.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Sub β],
  e.sub = { sub := fun x y => e.invFun (e.toFun x - e.toFun y) }
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toArray.size = m.size
-- Mathlib.Order.Hom.Lattice
SupHom.instOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β],
  SupHom.instOrderBot = OrderBot.lift DFunLike.coe ⋯ ⋯
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
_private.Mathlib.Topology.Algebra.IsUniformGroup.Basic.0.IsDenseInducing.extend_Z_bilin_key : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [inst : TopologicalSpace α]
  [inst_1 : AddCommGroup α] [IsTopologicalAddGroup α] [inst_3 : TopologicalSpace β] [inst_4 : AddCommGroup β]
  [inst_5 : TopologicalSpace γ] [inst_6 : AddCommGroup γ] [IsTopologicalAddGroup γ] [inst_8 : TopologicalSpace δ]
  [inst_9 : AddCommGroup δ] [inst_10 : UniformSpace G] [inst_11 : AddCommGroup G] {e : β →+ α},
  IsDenseInducing ⇑e →
    ∀ {f : δ →+ γ},
      IsDenseInducing ⇑f →
        ∀ {φ : β →+ δ →+ G},
          (Continuous fun p => (φ p.1) p.2) →
            ∀ {W' : Set G},
              W' ∈ nhds 0 →
                ∀ [IsUniformAddGroup G] (x₀ : α) (y₀ : γ),
                  ∃ U ∈ Filter.comap (⇑e) (nhds x₀),
                    ∃ V ∈ Filter.comap (⇑f) (nhds y₀),
                      ∀ x ∈ U,
                        ∀ x' ∈ U,
                          ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
-- Mathlib.Dynamics.OmegaLimit
mapsTo_omegaLimit' : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (s : Set α) {α' : Type u_5} {β' : Type u_6}
  [inst_1 : TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : Set α'},
  Set.MapsTo ga s s' →
    ∀ {gb : β → β'},
      (∀ᶠ (t : τ) in f, Set.EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) →
        Continuous gb → Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filter f m) k fallback =
        (Option.filter (fun x => f k' x) (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
IsTensorProduct.assocOfMapSMul.congr_simp : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] {T : Type u_16} [inst_21 : CommSemiring T] [inst_22 : Algebra R T]
  [inst_23 : Module T M₁] [inst_24 : IsScalarTower R T M₁] [inst_25 : Module T M₁₂] [inst_26 : SMulCommClass S T M₁₂]
  [inst_27 : IsScalarTower R T M₁₂] (f f_1 : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂) (e_f : f = f_1) (hf : IsTensorProduct f)
  (g g_1 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (e_g : g = g_1) (hg : IsTensorProduct g)
  (h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y)
  (h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y),
  IsTensorProduct.assocOfMapSMul f hf g hg h₁ h₂ = IsTensorProduct.assocOfMapSMul f_1 ⋯ g_1 ⋯ ⋯ ⋯
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.moment_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.moment X 1 μ = ∫ (x : Ω), X x ∂μ
-- Mathlib.Data.Finset.Sort
Finset.sorted_last_eq_max'_aux : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α)
  (h : (s.sort fun a b => a ≤ b).length - 1 < (s.sort fun a b => a ≤ b).length) (H : s.Nonempty),
  (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1] = s.max' H
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instAdd : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Add (MeasureTheory.FiniteMeasure Ω)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.mk.injEq : ∀ {α : Type u} (next next_1 : Option α), ({ next := next } = { next := next_1 }) = (next = next_1)
-- Init.Data.List.MapIdx
List.getElem?_mapIdx_go : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l : List α} {acc : Array β} {i : ℕ},
  (List.mapIdx.go f l acc)[i]? = if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.Perm.prod_comp' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → ι → M),
  {a | σ a ≠ a} ⊆ ↑s → ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Connection.mk : (tokens : Array String) → tokens.all Std.Http.Internal.isToken = true → Std.Http.Header.Connection
-- Std.Http.Data.Headers
/-- Checks if the entry is present in the `Headers`.
 -/
Std.Http.Headers.hasEntry : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Header.Value → Bool
-- Mathlib.Combinatorics.Hindman
Hindman.FP.mul_two : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (i j : ℕ), i < j → a.get i * a.get j ∈ Hindman.FP a
-- Init.Core
/-- The first component of a dependent pair.
 -/
Sigma.fst : {α : Type u} → {β : α → Type v} → Sigma β → α
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFaithfulCompPreRight : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) [F.Faithful], (CategoryTheory.Comma.preRight L F R).Faithful
-- Init.Data.Iterators.Lemmas.Producers.List
List.iter.eq_1 : ∀ {α : Type w} (l : List α), l.iter = (l.iterM Id).toIter
-- Lean.Elab.AssertExists
Lean.Elab.Command.instBEqAssertExists : BEq Lean.Elab.Command.AssertExists
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.denoteSInt_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (k : ℤ), Lean.Grind.CommRing.denoteSInt k = ↑k.toNat
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A variant of `Matrix.trace_units_conj`.  -/
Matrix.trace_conj : ∀ {m : Type u} {α : Type v} [inst : CommRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m α},
  IsUnit M → ∀ (N : Matrix m m α), (M * N * M⁻¹).trace = N.trace
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coconeOfDiagramInitial.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX hX_1 : CategoryTheory.Limits.IsInitial X),
  hX = hX_1 →
    ∀ (F : CategoryTheory.Functor J C) [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
      CategoryTheory.Limits.coconeOfDiagramInitial hX F = CategoryTheory.Limits.coconeOfDiagramInitial hX_1 F
-- Mathlib.Order.Basic
/-- A symmetric relation implies two values are equal, when it implies they're less-equal.  -/
rel_imp_eq_of_rel_imp_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder β] (r : α → α → Prop) [Std.Symm r] {f : α → β},
  (∀ (a b : α), r a b → f a ≤ f b) → ∀ {a b : α}, r a b → f a = f b
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_symm_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 H : CategoryTheory.Functor D C} (adj : F ⊣ G) (iso : G ≅ H) {X : C} {Y : D}
  (f : X ⟶ H.obj Y),
  ((adj.ofNatIsoRight iso).homEquiv X Y).symm f =
    (adj.homEquiv X Y).symm (CategoryTheory.CategoryStruct.comp f (iso.inv.app Y))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `p`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.p (CategoryTheory.CategoryStruct.comp self.φQ h) =
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h)
-- Mathlib.Algebra.Ring.Invertible
/-- Multiplying an additive unit from the left produces another additive unit.  -/
AddUnits.mulLeft : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → AddUnits R → R → AddUnits R
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a == b) = false) toInsert →
      (∀ (a : α), Std.Internal.List.containsKey a l = true → toInsert.contains a = false) →
        (Std.Internal.List.insertListIfNewUnit l toInsert).length = l.length + toInsert.length