mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The algebra homomorphism from `End M ⊗ End N` to `End (M ⊗ N)` sending `f ⊗ₜ g` to
the `TensorProduct.map f g`, the tensor product of the two maps.

This is an `AlgHom` version of `TensorProduct.AlgebraTensorModule.homTensorHomMap`. Like that
definition, this is generalized across many different rings; namely a tower of algebras `A/S/R`.  -/
Module.endTensorEndAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Semiring A] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Algebra R S] →
                      [inst_6 : Algebra S A] →
                        [inst_7 : Algebra R A] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module S M] →
                              [inst_10 : Module A M] →
                                [inst_11 : Module R N] →
                                  [inst_12 : IsScalarTower R A M] →
                                    [inst_13 : IsScalarTower S A M] →
                                      [inst_14 : IsScalarTower R S M] →
                                        TensorProduct R (Module.End A M) (Module.End R N) →ₐ[S]
                                          Module.End A (TensorProduct R M N)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.lift_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) (CategoryTheory.Limits.biprod.desc h i) =
    CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g i
-- Mathlib.Topology.Compactness.Compact
/-- A variant of `generalized_tube_lemma` that only replaces the set in one direction.  -/
generalized_tube_lemma_left : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s s' : Set X},
  IsCompact s →
    ∀ {t : Set Y},
      IsCompact t → ∀ {n : Set (X × Y)}, n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t) → ∃ u ∈ nhdsSetWithin s s', u ×ˢ t ⊆ n
-- Mathlib.Topology.MetricSpace.Algebra
instLipschitzAddOrderDual : ∀ (α : Type u_1) [inst : PseudoMetricSpace α] [inst_1 : AddMonoid α] [LipschitzAdd α], LipschitzAdd αᵒᵈ
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithScott α)
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.inner : {α : Sort u} → {b : α} → Lean.Order.FlatOrder b → α
-- Mathlib.Data.Sign.Basic
sign_sum : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {ι : Type u_1} {s : Finset ι}
  {f : ι → α}, s.Nonempty → ∀ (t : SignType), (∀ i ∈ s, SignType.sign (f i) = t) → SignType.sign (∑ i ∈ s, f i) = t
-- Mathlib.RingTheory.Polynomial.IsIntegral
Polynomial.isIntegral_coeff_prod : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (s : Finset ι) (p : ι → Polynomial S),
  (∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) → ∀ (j : ℕ), IsIntegral R ((s.prod p).coeff j)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.iselect_eq_default : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (ps : PFunctor.Approx.Path F) (x : F.M),
  ¬PFunctor.M.IsPath ps x → PFunctor.M.iselect ps x = default.head
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.lift_symm_apply : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] (F : UniversalEnvelopingAlgebra R L →ₐ[R] A),
  (UniversalEnvelopingAlgebra.lift R).symm F = F.toLieHom.comp (UniversalEnvelopingAlgebra.ι R)
-- Mathlib.Topology.Order.Compact
IsCompact.continuous_sInf : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] {f : γ → β → α} {K : Set β},
  IsCompact K → Continuous ↿f → Continuous fun x => sInf (f x '' K)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.IsConstant.mem_essImage : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u_2} {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.HasWeakSheafify J D}
  {F : CategoryTheory.Sheaf J D} [self : CategoryTheory.Sheaf.IsConstant J F],
  (CategoryTheory.constantSheaf J D).essImage F
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_pow : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (m : ℕ),
  WittVector.truncateFun n (x ^ m) = WittVector.truncateFun n x ^ m
-- Init.Data.List.Pairwise
List.pairwise_flatten : ∀ {α : Type u_1} {R : α → α → Prop} {L : List (List α)},
  List.Pairwise R L.flatten ↔ (∀ l ∈ L, List.Pairwise R l) ∧ List.Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.le_centralizer_centralizer : ∀ {R : Type u_1} [inst : Semiring R] {s : Subsemiring R}, s ≤ Subsemiring.centralizer ↑(Subsemiring.centralizer ↑s)
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_iff : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R}, IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_eq_norm_mul_norm : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), inner ℝ x x = ‖x‖ * ‖x‖
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_natCast_eq_self : ∀ {n a : ℕ} [NeZero n], (↑a).valMinAbs = ↑a ↔ a ≤ n / 2
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonUniforms.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (ε : 𝕜),
  P.nonUniforms G ε =
    {x ∈ P.parts.offDiag |
      match x with
      | (u, v) => ¬G.IsUniform ε u v}
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- Auxiliary equivalence with a product type used to lift an order.  -/
BoxIntegral.IntegrationParams.equivProd : BoxIntegral.IntegrationParams ≃ Bool × Boolᵒᵈ × Boolᵒᵈ
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.mapsTo_symm`. -/
OpenPartialHomeomorph.symm_mapsTo : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.MapsTo (↑e.symm) e.target e.source
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_filterMap_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)}
  {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true),
        (f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h)).isSome = true)
-- Mathlib.Topology.MetricSpace.Contracting
/-- If a map `f` is `ContractingWith K`, and `s` is a forward-invariant set, then
restriction of `f` to `s` is `ContractingWith K` as well.  -/
ContractingWith.restrict : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {s : Set α} (hs : Set.MapsTo f s s), ContractingWith K (Set.MapsTo.restrict f s s hs)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_comp_swap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P), (AddMonoid.Coprod.lift f g).comp (AddMonoid.Coprod.swap N M) = AddMonoid.Coprod.lift g f
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.mk : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.LocalDeclKind → Lean.Meta.Hypothesis
-- Lean.Elab.DocString
Lean.Doc.instMonadStateOfStateDocM : MonadStateOf Lean.Doc.State Lean.Doc.DocM
-- Mathlib.Data.Set.Card
/-- A function `f : α → β` decreases cardinality by at most one if and only if
there is at most a collision between a unique pair of elements.  -/
Set.ncard_le_ncard_image_add_one_iff : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [Finite ↑s] (f : α → β),
  s.ncard ≤ (f '' s).ncard + 1 ↔
    ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, ∀ d ∈ s, f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofEquivalence_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (𝒞₁ : CategoryTheory.Subobject.Classifier C) (e : C ≌ D) {U X : D} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  (𝒞₁.ofEquivalence e).χ m =
    CategoryTheory.CategoryStruct.comp (e.counitInv.app X) (e.functor.map (𝒞₁.χ (e.inverse.map m)))
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.left_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_sum_of_ne_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] {f : ι → M}
  {s t : Finset ι}, (∀ x ∈ s, f x ≠ 0 → x ∈ t) → ∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
-- Init.Data.List.Basic
/-- If the first list is a prefix of the second, returns the result of dropping the prefix.

In other words, `isPrefixOf? l₁ l₂` returns `some t` when `l₂ == l₁ ++ t`.

Examples:
* `[1, 2].isPrefixOf? [1, 2, 3] = some [3]`
* `[1, 2].isPrefixOf? [1, 2] = some []`
* `[1, 2].isPrefixOf? [1] = none`
* `[1, 2].isPrefixOf? [1, 1, 2, 3] = none`
 -/
List.isPrefixOf? : {α : Type u} → [BEq α] → List α → List α → Option (List α)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.variance (X + Y) μ =
        ProbabilityTheory.variance X μ + 2 * ProbabilityTheory.covariance X Y μ + ProbabilityTheory.variance Y μ
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.addConj`.

---

Group conjugation, `AddAut.addConj g h = g + h + -g`, as an additive homomorphism
mapping addition in `G` into addition in the additive automorphism group `AddAut G`.  -/
AddAut.conj : {G : Type u_3} → [inst : AddGroup G] → G →+ AddAut G
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_bitVecToInt : ∀ (n : BitVec 32), Int32.ofIntLE n.toInt ⋯ ⋯ = Int32.ofBitVec n
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instCoeComplex : Coe GaussianInt ℂ
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instOne : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → One (CentroidHom α)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.continueToTerm : Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Constructs a multiseries from a `Multiseries basis_hd basis_tl` and a function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      (ℝ → ℝ) → Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)
-- Mathlib.Algebra.Polynomial.Splits
/-- Let `f` be a monic polynomial over that splits. Let `x` be a root of `f`.
Then $f'(r) = \prod_{a}(x-a)$, where the product in the RHS is taken over all roots of `f`,
with the multiplicity of `x` reduced by one.  -/
Polynomial.Splits.eval_root_derivative : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  f.Splits →
    f.Monic →
      ∀ {x : R},
        x ∈ f.roots →
          Polynomial.eval x (Polynomial.derivative f) = (Multiset.map (fun x_1 => x - x_1) (f.roots.erase x)).prod
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (x : E),
  (MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 ⋯ ⋯ x) = (T Set.univ) x
-- Init.Data.Range.Polymorphic.Basic
Std.Roo.lower_le_of_mem : ∀ {α : Type u} {r : Std.Roo α} {a : α} [inst : LT α], a ∈ r → r.lower < a
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_mul_comm : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a : ℤ) (b : α), ↑a * b = b * ↑a
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- The length of the `i`-th root w.r.t. a root-positive form taking values in `S`.  -/
RootPairing.RootPositiveForm.rootLength : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [inst_1 : LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] →
                          {P : RootPairing ι R M N} →
                            [inst_8 : P.IsValuedIn S] →
                              RootPairing.RootPositiveForm S P →
                                [FaithfulSMul S R] → [inst_10 : Module S M] → [IsScalarTower S R M] → ι → S
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Eta expand `f` in only one variable and reduce in others.

Examples:
```
  f                ==> fun x => f x
  fun x y => f x y ==> fun x => f x
  HAdd.hAdd y      ==> fun x => HAdd.hAdd y x
  HAdd.hAdd        ==> fun x => HAdd.hAdd x
```  -/
Mathlib.Meta.FunProp.etaExpand1 : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.NumberField.Basic
/-- Any extension between ring of integers of number fields is Noetherian.  -/
NumberField.RingOfIntegers.extension_isNoetherian : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [NumberField K]
  [NumberField L], IsNoetherian (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_δ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.OplaxMonoidal] [inst_9 : G.OplaxMonoidal] (X Y : C × E),
  (CategoryTheory.Functor.OplaxMonoidal.δ (F.prod G) X Y).1 = CategoryTheory.Functor.OplaxMonoidal.δ F X.1 Y.1
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.πSummand.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  s.πSummand A = s.desc Δ fun B => if h : B = A then CategoryTheory.eqToHom ⋯ else 0
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofNat' : ∀ {n : ℕ}, (Int8.ofNat n).toBitVec = BitVec.ofNat 8 n
-- Mathlib.Tactic.Simps.NotationClass
/-- `@[notation_class]` attribute. Note: this is *not* a `NameMapAttribute` because we key on the
argument of the attribute, not the declaration name.  -/
Simps.notationClassAttr : Lean.NameMapExtension Simps.AutomaticProjectionData
-- Mathlib.Computability.RecursiveIn
/-- A total function is computable in `O` if its constant lift is recursive in `O`.  -/
ComputableIn : {α : Type u_5} → {σ : Type u_6} → [Primcodable α] → [Primcodable σ] → Set (ℕ →. ℕ) → (α → σ) → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.del.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15} {fvarId_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15},
  Lean.Compiler.LCNF.CodeDecl.del fvarId h = Lean.Compiler.LCNF.CodeDecl.del fvarId_1 h_1 → fvarId = fvarId_1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃},
  g.IsInvertible → (g ∘SL f).inverse v = f.inverse (g.inverse v)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.nthRemainder.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ)
  (a a_1 : Fin (n + 1) → k),
  a = a_1 →
    ∀ (a_2 a_3 : Fin (n + 1) → k), a_2 = a_3 → WittVector.nthRemainder p n a a_2 = WittVector.nthRemainder p_1 n a_1 a_3
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.isOrderedCancelAddMonoid_syn : ∀ {σ : Type u_1} (m : MonomialOrder σ), IsOrderedCancelAddMonoid m.syn
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkPrec.parenthesizer : ℕ → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (k : σ → τ) (g : τ → R) (p : MvPolynomial σ R),
  (MvPolynomial.eval g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval (g ∘ k)) p
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.loopHomeo_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : ↑(GenLoop N X x)), (GenLoop.loopHomeo i) p = GenLoop.toLoop i p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.diff.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α β) (e_t₁ : t₁ = t₁_1)
  (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α β), t₂ = t₂_1 → ∀ (h₁ : t₁.Balanced), t₁.diff t₂ h₁ = t₁_1.diff t₂_1 ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] (s : Finset α), s / ∅ = ∅
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.crown₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ j₄ k₁ k₂ : C}
  (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) (f₃ : j₃ ⟶ k₁) (g₃ : j₃ ⟶ k₂) (f₄ : j₄ ⟶ k₁)
  (g₄ : j₄ ⟶ k₂),
  ∃ s α β,
    CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
      CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β ∧
        CategoryTheory.CategoryStruct.comp f₃ α = CategoryTheory.CategoryStruct.comp g₃ β ∧
          CategoryTheory.CategoryStruct.comp f₄ α = CategoryTheory.CategoryStruct.comp g₄ β
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.mk.injEq : ∀ {G : Type u_6} [inst : AddGroup G] (toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm G)
  (eq_zero_of_map_eq_zero' : ∀ (x : G), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0)
  (toNonarchAddGroupSeminorm_1 : NonarchAddGroupSeminorm G)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : G), toNonarchAddGroupSeminorm_1.toFun x = 0 → x = 0),
  ({ toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm_1,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }) =
    (toNonarchAddGroupSeminorm = toNonarchAddGroupSeminorm_1)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_14 : HAdd Std.Time.Second.Offset Std.Time.Minute.Offset Std.Time.Second.Offset
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {k fallback : α}, k ∈ m → m.getKeyD k fallback = k
-- Std.Sync.Broadcast
/-- Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data.
 -/
Std.Broadcast.Receiver.recvSelector : {α : Type} → [Inhabited α] → Std.Broadcast.Receiver α → Std.Async.Selector (Option α)
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.subset_span_setGcd : ∀ (s : Set ℕ), s ⊆ ↑(Ideal.span {Nat.setGcd s})
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_of_lt_floor : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], n < ⌊a⌋₊ → ↑n < a
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.pathStar_bijective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {φ : U ⥤q V},
  φ.IsCovering → ∀ (u : U), Function.Bijective (φ.pathStar u)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.noPending : Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- `X _⦋n⦌` denotes the `n`th-term of the simplicial object X  -/
Simplicial.«term__⦋_⦌» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_le_succ_iSup : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), Ordinal.lsub f ≤ Order.succ (iSup f)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.uniqueLeft : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → [Subsingleton M] → Unique (TensorProduct R M N)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.vcomp.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  sizeOf (η.vcomp θ) = 1 + sizeOf a + sizeOf b + sizeOf f + sizeOf g + sizeOf h + sizeOf η + sizeOf θ
-- Mathlib.Analysis.Analytic.Constructions
alternatingGeometricSeries_apply_norm_le : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  (n : ℕ), ‖alternatingGeometricSeries 𝕜 A n‖ ≤ max 1 ‖1‖
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.DTreeMap.Raw.Const.unitOfList [] cmp = ∅
-- Mathlib.Analysis.Real.Sqrt
Real.continuous_sqrt : Continuous fun x => √x