mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_hom_apply_2_2 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.2 = x.2
-- Init.Data.Array.Erase
Array.size_erase_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, a ∈ xs → (xs.erase a).size = xs.size - 1
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.one_sub_K_ne_top : ∀ {K : NNReal}, 1 - ↑K ≠ ⊤
-- Mathlib.Tactic.CasesM
/-- Core tactic for `casesm` and `cases_type`. Calls `cases` on all fvars in `g` for which
`matcher ldecl.type` returns true.
* `recursive`: if true, it calls itself repeatedly on the resulting subgoals
* `allowSplit`: if false, it will skip any hypotheses where `cases` returns more than one subgoal.
* `throwOnNoMatch`: if true, then throws an error if no match is found
 -/
Lean.MVarId.casesMatching : (Lean.Expr → Lean.MetaM Bool) →
  optParam Bool false → optParam Bool true → optParam Bool true → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
_private.Mathlib.Analysis.InnerProductSpace.LinearPMap.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_id : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R), Ideal.map (RingHom.id R) I = I
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.bot_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], ↑⊥ = {0}
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A product of Gaussian distributions is Gaussian.  -/
ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [SecondCountableTopologyEither E F]
  {ν : MeasureTheory.Measure F} [ProbabilityTheory.IsGaussian ν], ProbabilityTheory.IsGaussian (μ.prod ν)
-- Init.Core
instInhabitedProp : Inhabited Prop
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.forget₂_map : ∀ {R S : CommGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ CommGrpCat GrpCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ CommGrpCat GrpCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Adj.reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → G.Reachable u v
-- Mathlib.Geometry.Manifold.HasGroupoid
continuousGroupoid.eq_1 : ∀ (H : Type u_2) [inst : TopologicalSpace H], continuousGroupoid H = (continuousPregroupoid H).groupoid
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_zero : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, multiplicity a b = 0 ↔ ¬a ∣ b
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m + n). Is every element of `t₁` equivalent to some element of `t₂`?

```
is_subset {1, 4} {1, 2, 4} = tt
is_subset {1, 3} {1, 2, 4} = ff
```  -/
Ordnode.isSubset : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Bool
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.Script.TacticBuilder.simpAllOrSimpAtStarOnlyStx : Bool → Lean.MVarId → Option Lean.Term → Lean.Meta.Simp.UsedSimps → Lean.MetaM Lean.Syntax.Tactic
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integral_countable : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X} [Countable X],
  MeasureTheory.Integrable f μ → ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.node.inj : ∀ {step : Aesop.Script.Step} {index : ℕ} {children : Array Aesop.Script.StepTree} {step_1 : Aesop.Script.Step}
  {index_1 : ℕ} {children_1 : Array Aesop.Script.StepTree},
  Aesop.Script.StepTree.node step index children = Aesop.Script.StepTree.node step_1 index_1 children_1 →
    step = step_1 ∧ index = index_1 ∧ children = children_1
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocSemiring.toDistrib_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalNonAssocSemiring.toDistrib R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).size =
        if k ∈ t ∧ (f (t.get? k)).isNone = true then t.size - 1
        else if k ∉ t ∧ (f (t.get? k)).isSome = true then t.size + 1 else t.size
-- Lean.Meta.Sym.SymM
/-- Cache for `isDefEqI` results  -/
Lean.Meta.Sym.State.defEqI : Lean.Meta.Sym.State → Lean.PHashMap (Lean.Meta.Sym.ExprPtr × Lean.Meta.Sym.ExprPtr) Bool
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_neg : ∀ (k : ℤ), pentagonal (-k) = (k * (3 * k + 1) / 2).toNat
-- Lean.Compiler.NameMangling
/-- Assuming `s` has been produced by `Name.mangle _ ""`, return the original name.  -/
Lean.Name.demangle : String → Lean.Name
-- Mathlib.Order.Bounds.Basic
lowerBounds_empty : ∀ {α : Type u_1} [inst : Preorder α], lowerBounds ∅ = Set.univ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limitsOfShape_limMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasLimit X] [inst_3 : CategoryTheory.Limits.HasLimit Y],
  W.functorCategory J f → W.limitsOfShape J (CategoryTheory.Limits.limMap f)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.interpolatedStr.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Time.Time.Unit.Second
Std.Time.Second.instAddOffset : Add Std.Time.Second.Offset
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α), Nonempty g.Basis
-- Init.Data.Iterators.Lemmas.Monadic.Basic
/-- Induction principle for productive monadic iterators: One can define a function `f` that maps every
iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
the plausible skip successors of `it'.
 -/
Std.IterM.inductSkips : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Productive α m] →
          (motive : Std.IterM m β → Sort x) →
            ((it : Std.IterM m β) →
                ({it' : Std.IterM m β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it) →
              (it : Std.IterM m β) → motive it
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_univ_iff : ∀ {α : Type v} [inst : LinearOrder α], IsStationary Set.univ ↔ Nonempty α
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsLeftRegular.isUnit_of_finite : ∀ {R : Type u_1} [inst : Monoid R] {r : R} [Finite R], IsLeftRegular r → IsUnit r
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Clopens α}, s = t ↔ ↑s = ↑t
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring R)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : cc.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf)
      (CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv h) =
    h
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- Reindexing both indices along the same equivalence preserves the determinant.

For the `simp` version of this lemma, see `det_submatrix_equiv_self`.
 -/
Matrix.det_reindexLinearEquiv_self : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (e : m ≃ n) (M : Matrix m m R),
  ((Matrix.reindexLinearEquiv R R e e) M).det = M.det
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isEqvAux.match_1.eq_2 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_lsub_le : ∀ {ι : Type u} (f : ι → Ordinal.{u}), (Ordinal.lsub f).cof ≤ Cardinal.mk ι
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instInv : {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → Inv (Monoid.Coprod G H)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.mul.sizeOf_spec : sizeOf FirstOrder.ringFunc.mul = 1
-- Mathlib.Combinatorics.Matroid.Map
/-- Map `M : Matroid α` across an embedding defined on all of `α`  -/
Matroid.mapEmbedding : {α : Type u_1} → {β : Type u_2} → Matroid α → (α ↪ β) → Matroid β
-- Init.Data.Nat.Simproc
Nat.Simproc.add_le_le : ∀ (a : ℕ) {b c : ℕ}, b ≤ c → (a + b ≤ c) = (a ≤ c - b)
-- Mathlib.Data.Rel.Cover
SetRel.isCover_empty_right : ∀ {X : Type u_1} {U : SetRel X X} {s : Set X}, U.IsCover s ∅ ↔ s = ∅
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep.linearEquiv.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤),
  ind.linearEquiv iSup_top = LinearEquiv.ofBijective ((DFinsupp.lsum ℕ) fun i => (p i).subtype) ⋯
-- Init.Data.List.Find
List.IsSuffix.findIdx?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <:+ l₂ → List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
-- Mathlib.Data.Quot
Quotient.mk_out : ∀ {α : Sort u_1} {s : Setoid α} (a : α), s ⟦a⟧.out a
-- Mathlib.Topology.Separation.Regular
/-- Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`,
with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint.  -/
disjoint_nested_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T3Space X] {x y : X},
  x ≠ y →
    ∃ U₁ ∈ nhds x,
      ∃ V₁ ∈ nhds x,
        ∃ U₂ ∈ nhds y,
          ∃ V₂ ∈ nhds y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_isPredLimit_of_not_isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α], ¬IsMax a → (Order.IsPredPrelimit a ↔ Order.IsPredLimit a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_roo_iff : ∀ {m n i : ℕ}, 0 < (m<...n).toList[i]! ↔ i < n - (m + 1)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function commutes with the actions.  -/
MulActionHom.map_smul' : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  (self : X →ₑ[φ] Y) (m : M) (x : X), self.toFun (m • x) = φ m • self.toFun x
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instEquivLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → EquivLike (α ≃*o β) α β
-- Mathlib.Geometry.Manifold.Instances.Real
closure_open_halfSpace : ∀ {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n), closure {y | a < y.ofLp i} = {y | a ≤ y.ofLp i}
-- Mathlib.Geometry.Convex.Cone.Basic
/-- In a subsingleton module, the empty convex cone is generating.  -/
ConvexCone.isGenerating_bot : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Subsingleton M], ⊥.IsGenerating
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_sup_eq_top' : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ}, I ⊔ J = ⊤ → I ^ n ⊔ J = ⊤
-- ImportGraph.Imports.Redundant
/-- Return the redundant imports (i.e. those transitively implied by another import)
of a specified module (or the current module if `none` is specified).
 -/
redundantImports : optParam (Option Lean.Name) none → Lean.CoreM Lean.NameSet
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_le_maximal : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ), (f.genEigenspace μ) ↑k ≤ f.maxGenEigenspace μ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.lie_h_h : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Fintype ι] (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.h i, RootPairing.GeckConstruction.h j⁆ = 0
-- Mathlib.Data.Nat.Choose.Basic
/-- A faster implementation of `choose`, to be used during bytecode evaluation
and in compiled code.  -/
Nat.fast_choose : ℕ → ℕ → ℕ
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.coeff_freeMonic : ∀ (R : Type u_1) [inst : CommRing R] (n k : ℕ),
  (Polynomial.freeMonic R n).coeff k = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y y' : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F y y' → CommRingCat.Colimits.Relation F (x.mul y) (x.mul y')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine.eq_1 : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Projective F) (P : Fin 3 → F),
  WeierstrassCurve.Projective.Point.toAffine W P =
    if hP : W.Nonsingular P ∧ P 2 ≠ 0 then WeierstrassCurve.Affine.Point.some (P 0 / P 2) (P 1 / P 2) ⋯ else 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Operator seminorm on the space of continuous multilinear maps, as `Seminorm`.

We use this seminorm
to define a `SeminormedAddCommGroup` structure on `ContinuousMultilinearMap 𝕜 E G`,
but we have to override the projection `UniformSpace`
so that it is definitionally equal to the one coming from the topologies on `E` and `G`.  -/
ContinuousMultilinearMap.seminorm : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → [Fintype ι] → Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
`1 / (monomial n a)` (as an element of the field of rational functions) is equal
to `(v RatFunc.X) ^ (- n)`.  -/
Polynomial.valuation_inv_monomial_eq_valuation_X_zpow : ∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K},
  a ≠ 0 → v (1 / ↑((Polynomial.monomial n) a)) = v RatFunc.X ^ (-↑n)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Context.mk.inj : ∀ {elaborator : Lean.Name} {recover : Bool} {elaborator_1 : Lean.Name} {recover_1 : Bool},
  { elaborator := elaborator, recover := recover } = { elaborator := elaborator_1, recover := recover_1 } →
    elaborator = elaborator_1 ∧ recover = recover_1
-- Init.Data.Int.DivMod.Bootstrap
Int.ofNat_dvd : ∀ {m n : ℕ}, ↑m ∣ ↑n ↔ m ∣ n
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_mul_right : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → b < c → a * b < a * c
-- Mathlib.Order.LiminfLimsup
Filter.limsSup.eq_1 : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : Filter α), f.limsSup = sInf {a | ∀ᶠ (n : α) in f, n ≤ a}
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.assocOfMapSMul_symm_tmul : ∀ {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 : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂) (hf : IsTensorProduct f) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃)
  (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) (x₁ : M₁) (x₂ : M₂) (x₃ : M₃),
  (IsTensorProduct.assocOfMapSMul f hf g hg h₁ h₂).symm (x₁ ⊗ₜ[R] (g x₂) x₃) = (f x₁) x₂ ⊗ₜ[S] x₃
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocMod hp (a + OfNat.ofNat m * p) b = toIocMod hp a b + OfNat.ofNat m * p
-- Mathlib.Tactic.FunProp.Elab
/-- Command that prints all function properties attached to a function.

For example
```
#print_fun_prop_theorems HAdd.hAdd
```
might print out
```
Continuous
  continuous_add, args: [4,5], priority: 1000
  continuous_const_add, args: [5], priority: 1000
  continuous_add_const, args [4], priority: 1000
  ...
Differentiable
  Differentiable.add, args: [4,5], priority: 1000
  Differentiable.add_const, args: [4], priority: 1000
  Differentiable.const_add, args: [5], priority: 1000
  ...
```

You can also see only theorems about a concrete function property
```
#print_fun_prop_theorems HAdd.hAdd Continuous
```
 -/
Mathlib.Meta.FunProp.«command#print_fun_prop_theorems__» : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Map
Matroid.Indep.exists_bijOn_of_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {I : Set β} (hf : Set.InjOn f M.E),
  (M.map f hf).Indep I → ∃ I₀, M.Indep I₀ ∧ Set.BijOn f I₀ I
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_subset_mul`.  -/
Set.multiset_prod_subset_multiset_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcompose_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcompose.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.ofLeftInverse_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : ↥f.srange), (MulEquiv.ofLeftInverse f h).symm a = g ↑a
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
tsum_pow_div_one_sub_eq_tsum_sigma : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] {r : 𝕜},
  ‖r‖ < 1 →
    ∀ (k : ℕ), ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma k) ↑n) * r ^ ↑n
-- Mathlib.SetTheory.ZFC.Ordinal
/-- An ordinal is a transitive set of transitive sets.  -/
ZFSet.isOrdinal_iff_forall_mem_isTransitive : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ ∀ y ∈ x, y.IsTransitive
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- For two ordered monoid morphisms `f` and `g`, their product is the ordered monoid morphism
sending `a` to `f a * g a`.  -/
OrderMonoidWithZeroHom.instMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrderedCommMonoidWithZero α] → [inst_1 : LinearOrderedCommMonoidWithZero β] → Mul (α →*₀o β)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.FindAux.mk.inj : ∀ {n : ℕ} {s : Array Batteries.UFNode} {root : Fin n} {size_eq : s.size = n} {s_1 : Array Batteries.UFNode}
  {root_1 : Fin n} {size_eq_1 : s_1.size = n},
  { s := s, root := root, size_eq := size_eq } = { s := s_1, root := root_1, size_eq := size_eq_1 } →
    s = s_1 ∧ root = root_1
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Construct an object of `P.category`.  -/
CategoryTheory.Presieve.categoryMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (P : CategoryTheory.Presieve X) → {Y : C} → (f : Y ⟶ X) → P f → P.category
-- Mathlib.CategoryTheory.Sites.Plus
/-- An auxiliary definition used in `plus` below.  -/
CategoryTheory.GrothendieckTopology.plusMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → (J.plusObj P ⟶ J.plusObj Q)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_algebraMap : ∀ {K : Type u} [inst : Field K] (p : Polynomial K), ((algebraMap (Polynomial K) (RatFunc K)) p).denom = 1
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.isVonNBounded : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (self : Bundle.RiemannianMetric E) (b : B),
  Bornology.IsVonNBounded ℝ {v | ((self.inner b) v) v < 1}
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a constant function is `⊤` if the constant is zero and `0` otherwise.
 -/
meromorphicOrderAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (z₀ : 𝕜) (e : E) [inst_3 : Decidable (e = 0)],
  meromorphicOrderAt (fun x => e) z₀ = if e = 0 then ⊤ else 0
-- Mathlib.SetTheory.Lists
Lists'.subset_def : ∀ {α : Type u_1} {l₁ l₂ : Lists' α true}, l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂
-- Mathlib.Order.OmegaCompletePartialOrder
/-- See Note [custom simps projection]. We specify this explicitly because we don't have a DFunLike
instance.
 -/
OmegaCompletePartialOrder.ContinuousHom.Simps.apply : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → (α →𝒄 β) → α → β