mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.mk.sizeOf_spec : ∀ {matType : ℕ → ℕ → Type} [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType]
  [inst_1 : (a a_1 : ℕ) → SizeOf (matType a a_1)] (basic free : Array ℕ) (mat : matType basic.size free.size),
  sizeOf { basic := basic, free := free, mat := mat } = 1 + sizeOf basic + sizeOf free + sizeOf mat
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_eq_mul_of_div_eq_div : ∀ {α : Type u} [inst : DivisionCommMonoid α] {b d : α}, IsUnit b → IsUnit d → ∀ (a c : α), a / b = c / d → a * d = c * b
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_apply : ∀ {α : Type u_1} (s t : Set α) (m : MeasureTheory.OuterMeasure α),
  ((MeasureTheory.OuterMeasure.restrict s) m) t = m (t ∩ s)
-- Batteries.Control.Nondet.Basic
/-- Apply a function which returns values in the monad to every alternative of a `Nondet m α`.  -/
Nondet.mapM : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → (α → m β) → Nondet m α → Nondet m β
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_cyclesIsoSc'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_of_eq' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, b₁ + ↑a₂ = a₁ + ↑b₂ → f.mk' a₁ a₂ = f.mk' b₁ b₂
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.del.sizeOf_spec : ∀ {β : Type u} {α : Type v} [inst : SizeOf β] [inst_1 : SizeOf α] (ids : Array ℕ),
  sizeOf (Std.Tactic.BVDecide.LRAT.Action.del ids) = 1 + sizeOf ids
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.fold_eq_match_step : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Std.Iter β},
  Std.Iter.fold f init it =
    match it.step with
    | ⟨Std.IterStep.yield it' out, property⟩ => Std.Iter.fold f (f init out) it'
    | ⟨Std.IterStep.skip it', property⟩ => Std.Iter.fold f init it'
    | ⟨Std.IterStep.done, property⟩ => init
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_univ_of_zero_mem : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α}, 0 ∈ s → s + Set.univ = Set.univ
-- Mathlib.Logic.ExistsUnique
/-- Checks to see that `xs` has only one binder.  -/
Mathlib.Notation.isExplicitBinderSingular : Lean.TSyntax `Lean.explicitBinders → Bool
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- The $n$-dimensional volume of an object in an $n$-dimensional space is equal to the integral
of the volume of $(n-1)$-dimensional orthogonal cross-section along a line defined by a direction
vector. This is a special case of `AffineSubspace.euclideanHausdorffMeasure_eq_lintegral` with a
one-dimensional subspace.  -/
EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (p : P) {v : V},
  v ≠ 0 →
    ∀ {t : Set P},
      MeasurableSet t →
        (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) t =
          ‖v‖ₑ *
            ∫⁻ (x : ℝ),
              (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V - 1))
                (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))
-- Init.Data.Array.Lex.Lemmas
Array.map_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {xs ys : Array α} {f : α → β},
  (∀ (x y : α), x < y → f x < f y) → xs < ys → Array.map f xs < Array.map f ys
-- Init.Data.List.Lex
List.cons_lex_cons_iff : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {l₁ : List α} {b : α} {l₂ : List α},
  List.Lex r (a :: l₁) (b :: l₂) ↔ r a b ∨ a = b ∧ List.Lex r l₁ l₂
-- Mathlib.Data.Num.Bitwise
SNum.instSub : Sub SNum
-- Std.Data.HashSet.Raw
/-- Internal implementation detail of the hash set  -/
Std.HashSet.Raw.WF.out : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α}, m.WF → m.inner.WF
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_iff_forall_indepSet : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m₁ m₂ : MeasurableSpace Ω) {_m0 : MeasurableSpace Ω}
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ ↔
    ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.Kernel.IndepSet s t κ μ
-- Mathlib.RingTheory.IdealFilter.Basic
/-- `F • G` is the Gabriel composition of ideal filters `F` and `G`.  -/
IdealFilter.«term_•_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.id_weightMap_apply : ∀ {ι : 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) (x : M),
  (RootPairing.Hom.id P).weightMap x = x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : S.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst S.hom U.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  0 < N → a < b → n ≤ MeasureTheory.upcrossingsBefore a b f N ω → MeasureTheory.upperCrossingTime a b f N n ω < N
-- Init.Prelude
/-- The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
 * `Nat.ble 2 5 = true`
 * `Nat.ble 5 2 = false`
 * `Nat.ble 5 5 = true`
 -/
Nat.ble : ℕ → ℕ → Bool
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], r.toList = [] ↔ ¬r.lower ≤ r.upper
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- Boxes of countably spanning sets are countably spanning.  -/
IsCountablySpanning.pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), IsCountablySpanning (C i)) → IsCountablySpanning (Set.univ.pi '' Set.univ.pi C)
-- Mathlib.Data.ZMod.Defs
Fin.instNonUnitalCommRing : (n : ℕ) → [NeZero n] → NonUnitalCommRing (Fin n)
-- Mathlib.Data.Set.Lattice
Set.iUnion_subset_iUnion_const : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {s : Set α} (h : ι → ι₂), ⋃ x, s ⊆ ⋃ x, s
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C),
  (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X)
          (CategoryTheory.Limits.kernel.ι α)).hom
      (CategoryTheory.Limits.cokernel.map ((CategoryTheory.Limits.kernel.ι α).app X)
        (CategoryTheory.Limits.kernel.ι (α.app X))
        (CategoryTheory.Limits.kernelComparison α ((CategoryTheory.evaluation C D).obj X))
        (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_eq_iff_rpow_eq : ∀ {b x y : ℝ}, 0 < b → b ≠ 1 → 0 < y → (Real.logb b y = x ↔ b ^ x = y)
-- Init.Omega.IntList
Lean.Omega.IntList.instSub : Sub Lean.Omega.IntList
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType) {Z : C}
  (h : ((CategoryTheory.SmallObject.iteration I κ).obj f).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.iterationFunctorObjObjRightIso I κ f j).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f)) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j) h
-- Mathlib.Order.Lattice
MonotoneOn.of_map_sup : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β],
  (∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) → MonotoneOn f s
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The reverse direction of `WithLp.volume_preserving_ofLp`, since
`MeasurePreserving.symm` only works for `MeasurableEquiv`s.  -/
WithLp.volume_preserving_toLp : ∀ (U : Type u_4) (V : Type u_5) [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : MeasurableSpace U] [inst_3 : BorelSpace U] [inst_4 : FiniteDimensional ℝ U] [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  [inst_9 : FiniteDimensional ℝ V],
  MeasureTheory.MeasurePreserving (WithLp.toLp 2) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_eq_zero : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
  (g : σ → S₂) (φ : MvPolynomial σ R),
  (∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0) → (MvPolynomial.eval₂Hom f g) φ = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.min_le_max_of_add_le_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] {a b c d : α} [AddLeftStrictMono α] [AddRightMono α],
  a + b ≤ c + d → min a b ≤ max c d
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_one : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A], CFC.sqrt 1 = 1
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.decidableLT : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → [DecidableLT α] → DecidableLT (AddLocalization s)
-- Std.Http.Data.Body.Stream
/-- Sets known size metadata.
 -/
Std.Http.Body.Stream.setKnownSize : Std.Http.Body.Stream → Option Std.Http.Body.Length → Std.Async.Async Unit
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorUnit_isModule : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).isModule = Semiring.toModule
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- A functor `F : J ⥤ C` from a filtered category is eventually constant if there
exists `i : J`, such that for any `f : i ⟶ j`, the induced map `F.map f` is an isomorphism.  -/
CategoryTheory.IsFiltered.IsEventuallyConstant : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] → CategoryTheory.Functor J C → Prop
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
/-- In any concrete category, injective morphisms are monomorphisms.  -/
CategoryTheory.ConcreteCategory.mono_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.Mono f
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_C_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R),
  Polynomial.toLaurent ((Polynomial.monomial n) r) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
AddSubgroup.properlyDiscontinuousVAdd_iff : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : VAdd Γ α]
  (S : AddSubgroup Γ),
  ProperlyDiscontinuousVAdd (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ ((g +ᵥ K) ∩ L).Nonempty}.Finite
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_hom_app : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C),
  (CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor C D).hom.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.right (Opposite.op X)))
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear_apply_two : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.instHasBinaryCoproductsOfOrderBot : ∀ {α : Type u} [inst : SemilatticeSup α] [OrderBot α], CategoryTheory.Limits.HasBinaryCoproducts α
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.tree_eq_bot : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)}, T = ⊥ ↔ [] ∉ T
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A transitive relation is a jointly monic pair of parallel morphisms `p₁, p₂ : R ⟶ X`, together
with a limiting pullback cone `c` for `p₁` and `p₂` and a map `c.pt ⟶ R` which factors the two
projections `c.pt ⟶ X` through `R`.  -/
CategoryTheory.TransitiveRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X : C} → (R ⟶ X) → (R ⟶ X) → Type (max u_1 v_1)
-- Mathlib.Data.List.Sigma
List.lookupAll_eq_dlookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)},
  l.NodupKeys → List.lookupAll a l = (List.dlookup a l).toList
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
/-- For any `w`-small family `X : ι → Type u` of `w`-small types, there exists
a regular cardinal `κ : Cardinal.{w}` such that `HasCardinalLT (X i) κ` for all `i : ι`.  -/
HasCardinalLT.exists_regular_cardinal_forall : ∀ {ι : Type v} (X : ι → Type u) [Small.{w, v} ι] [∀ (i : ι), Small.{w, u} (X i)],
  ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprMon.repr : Lean.Grind.CommRing.Mon → ℕ → Std.Format
-- Mathlib.Topology.Connected.PathConnected
Submonoid.coe_pathComponentOne : ∀ (M : Type u_4) [inst : Monoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousMul M],
  ↑(Submonoid.pathComponentOne M) = pathComponent 1
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.refl : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation.below ⋯
-- Mathlib.RingTheory.TensorProduct.Maps
Module.End.lTensorAlgHom_apply_apply : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (a : Module.End R M) (a_1 : TensorProduct R N M),
  ((Module.End.lTensorAlgHom R M N) a) a_1 = (TensorProduct.liftAux ((TensorProduct.mk R N M).compl₂ a)) a_1
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous (ν₁ + ν₂) → μ.MutuallySingular ν₂ → μ.AbsolutelyContinuous ν₁
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lhom_ext'_iff : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] {φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N},
  φ = ψ ↔ ∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i
-- Init.Data.Vector.Lemmas
Vector.forIn_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → β → m (ForInStep β)}
  {xs : Array α} (h : xs.size = n) {b : β}, forIn (Vector.mk xs h) b f = forIn xs b f
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  K.extendCyclesIso e hj' = K.extendCyclesIso e hj'
-- Init.Data.Nat.Simproc
Nat.Simproc.add_le_add_le : ∀ (a c : ℕ) {b d : ℕ}, b ≤ d → (a + b ≤ c + d) = (a ≤ c + (d - b))
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.instLinearEquivClass : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N},
  LinearEquivClass (Q₁.IsometryEquiv Q₂) R M₁ M₂
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instUnion : Union ZFSet.{u_1}
-- Mathlib.Order.Lattice
/-- A lattice is a join-semilattice which is also a meet-semilattice.  -/
Lattice : Type u → Type u
-- Mathlib.Geometry.Manifold.Instances.Icc
mfderiv_subtypeVal_Icc_one : ∀ {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)), (mfderiv% Subtype.val z) 1 = 1
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Stirling's Formula**, formulated in terms of `Asymptotics.IsEquivalent`.  -/
Stirling.factorial_isEquivalent_stirling : Asymptotics.IsEquivalent Filter.atTop (fun n => ↑n.factorial) fun n => √(2 * ↑n * Real.pi) * (↑n / Real.exp 1) ^ n
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left : ∀ {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} {p x : P},
  x ∈ s.orthRadius p ↔ inner ℝ (x -ᵥ p) (p -ᵥ s.center) = 0
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.closedComplemented_top : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], ⊤.ClosedComplemented
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} [Nonempty α] (x : ↥P.parts.offDiag),
  ε ≤ 1 →
    P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
      100 ≤ 4 ^ P.parts.card * ε ^ 5 →
        ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 + ((if G.IsUniform ε (↑x).1 (↑x).2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
          (∑ i ∈ SzemerediRegularity.distinctPairs✝ hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ P.parts.card
-- Mathlib.Tactic.MinImports
/-- `getAttrs env stx` returns all attribute declaration names contained in `stx` and registered
in the `Environment` `env`.  -/
Mathlib.Command.MinImports.getAttrs : Lean.Environment → Lean.Syntax → Lean.NameSet
-- Mathlib.GroupTheory.ArchimedeanDensely
instDenselyOrderedWithZeroOfNoMinOrder : ∀ {X : Type u_3} [inst : Preorder X] [NoMinOrder X] [DenselyOrdered X], DenselyOrdered (WithZero X)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_formPerm_nil : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (x : α), [].formPerm.toList x = []
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Init.Data.SInt.Bitwise
ISize.shiftRight_zero : ∀ {a : ISize}, a >>> 0 = a
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- An `AddSubgroup` is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form `Characteristic.iff...`  -/
AddSubgroup.Characteristic : {A : Type u_4} → [inst : AddGroup A] → AddSubgroup A → Prop
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instAdditiveModuleCatCoinvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G], (Rep.coinvariantsFunctor k G).Additive
-- Mathlib.Data.PEquiv
PEquiv.trans_refl : ∀ {α : Type u} {β : Type v} (f : α ≃. β), f.trans (PEquiv.refl β) = f
-- Mathlib.FieldTheory.Laurent
/-- The Laurent expansion of rational functions about a value.
Auxiliary definition, usage when over integral domains should prefer `RatFunc.laurent`.  -/
RatFunc.laurentAux : {R : Type u} → [inst : CommRing R] → R → RatFunc R →+* RatFunc R
-- Mathlib.Algebra.Free
FreeAddSemigroup.instAddSemigroup.eq_1 : ∀ {α : Type u},
  FreeAddSemigroup.instAddSemigroup =
    { add := fun L1 L2 => { head := L1.head, tail := L1.tail ++ L2.head :: L2.tail }, add_assoc := ⋯ }
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_pos_of_is_add_left_invariant : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : AddGroup G]
  [inst_2 : IsTopologicalAddGroup G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) →
    ∀ (K : TopologicalSpace.Compacts G),
      μ K ≠ 0 → ∀ (U : TopologicalSpace.Opens G), (↑U).Nonempty → 0 < μ.innerContent U
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.CoherenceHom.mk.inj : ∀ {e : Lean.Expr} {src tgt : Mathlib.Tactic.BicategoryLike.Mor₁} {inst unfold e_1 : Lean.Expr}
  {src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {inst_1 unfold_1 : Lean.Expr},
  { e := e, src := src, tgt := tgt, inst := inst, unfold := unfold } =
      { e := e_1, src := src_1, tgt := tgt_1, inst := inst_1, unfold := unfold_1 } →
    e = e_1 ∧ src = src_1 ∧ tgt = tgt_1 ∧ inst = inst_1 ∧ unfold = unfold_1