mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.liftAlgHom_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} [inst_1 : CommRing A] {K : Type u_5} [inst_2 : Field K]
  {L : Type u_7} [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : Algebra R A]
  [inst_7 : Algebra R K] [inst_8 : IsScalarTower R A K] [inst_9 : Algebra R L] {g : A →ₐ[R] L}
  (hg : Function.Injective ⇑g) (x : K), (IsFractionRing.liftAlgHom hg) x = (IsFractionRing.lift hg) x
-- Mathlib.Logic.Encodable.Basic
/-- If `α` and `β` are encodable, then so is their sum.  -/
Sum.encodable : {α : Type u_1} → {β : Type u_2} → [Encodable α] → [Encodable β] → Encodable (α ⊕ β)
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a<...b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a + 1`, the statement holds for the empty range `a<...b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, if the
statement holds for `a<...b`, it also holds for the larger range `a<...(b + 1)`.

The following is an example reproving `length_toList_roo`.

```
example (a b : Int) : (a<...b).toList.length = (b - a - 1).toNat := by
  induction a, b using Int.induct_roo_right
  case base =>
    simp only [Int.toList_roo_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Int.toList_roo_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega
``` -/
Int.induct_roo_right : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a + 1 → motive a b) →
    (∀ (a b : ℤ), a + 1 ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℤ), motive a b
-- Mathlib.Order.Basic
LE.le.le_or_ge : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, b ≤ a → ∀ (c : α), c ≤ a ∨ b ≤ c
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_insert : ∀ (x y : PSet.{u_1}), (insert x y).rank = max (Order.succ x.rank) y.rank
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_undef : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  AEMeasurable X μ →
    ¬MeasureTheory.Integrable (fun ω => Real.exp (z.re * X ω)) μ → ProbabilityTheory.complexMGF X μ z = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
PartialOrder.mem_nerve_nonDegenerate_iff_strictMono : ∀ {X : Type u_1} [inst : PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })),
  s ∈ (CategoryTheory.nerve X).nonDegenerate n ↔ StrictMono s.obj
-- Init.Prelude
/-- Unpacks a `UInt32` into a `BitVec 32`. This function is overridden with a native implementation.
 -/
UInt32.toBitVec : UInt32 → BitVec 32
-- Mathlib.GroupTheory.HNNExtension
/-- The empty word  -/
HNNExtension.NormalWord.empty : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → {d : HNNExtension.NormalWord.TransversalPair G A B} → HNNExtension.NormalWord d
-- Mathlib.RingTheory.FiniteType
/-- If `R[M]` is of finite type then `M` is finitely generated.  -/
AddMonoidAlgebra.fg_of_finiteType : ∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommRing R] [Nontrivial R]
  [h : Algebra.FiniteType R (AddMonoidAlgebra R M)], AddMonoid.FG M
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.homToNerveMk_app_one : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (F : CategoryTheory.Functor X.HomotopyCategory C)
  (f : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
  (CategoryTheory.ConcreteCategory.hom
        ((SSet.Truncated.HomotopyCategory.homToNerveMk F).app
          (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })))
      f =
    CategoryTheory.ComposableArrows.mk₁ (F.map (SSet.Truncated.HomotopyCategory.homMk (SSet.Truncated.Edge.mk' f)))
-- Mathlib.Data.Fintype.Card
card_finset_fin_le : ∀ {n : ℕ} (s : Finset (Fin n)), s.card ≤ n
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.singleZeroAlgHom_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] (a : A), AddMonoidAlgebra.singleZeroAlgHom a = AddMonoidAlgebra.single 0 a
-- Init.Data.Array.Monadic
Array.forIn'_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {as bs : Array α} (w : as = bs) {b b' : β},
  b = b' →
    ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
      (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
-- Mathlib.Algebra.Group.Action.Opposite
Semigroup.opposite_smulCommClass : ∀ {α : Type u_3} [inst : Semigroup α], SMulCommClass αᵐᵒᵖ α α
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le_ofNat_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.lift.{v, u} a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_lt_iff_exists : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] {x : HahnSeries Γ R} {i : WithTop Γ},
  x.orderTop < i ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.instIsIsoHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.IsIso (𝒞₁.hom 𝒞₂)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.comp_lift : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  {P' : Type u_4} [inst_3 : AddMonoid P'] (f : P →+ P') (g₁ : M →+ P) (g₂ : N →+ P),
  f.comp (AddMonoid.Coprod.lift g₁ g₂) = AddMonoid.Coprod.lift (f.comp g₁) (f.comp g₂)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.eraseKey : {α : Type u} → {β : α → Type v} → [BEq α] → α → List ((a : α) × β a) → List ((a : α) × β a)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.filter f` is another iterator that applies a
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

In situations where `f` is monadic, use `filterM` instead.

**Marble diagram (without monadic effects):**

```text
it            ---a--b--c--d-e--⊥
it.filter     ---a-----c-------⊥
```

(given that `f a = f c = true` and `f b = f d = d e = false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though
no `Productive` instance is provided. For example, if `f` always returns `True`, the resulting
iterator will be productive as long as `it` is. In such situations, the missing instance needs to
be proved manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned value.
 -/
Std.IterM.filter : {α β : Type w} →
  {m : Type w → Type w'} → [Std.Iterator α m β] → [inst : Monad m] → (f : β → Bool) → Std.IterM m β → Std.IterM m β
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_zpow : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β] (f : C(α, β)) (z : ℤ), ⇑(f ^ z) = ⇑f ^ z
-- Mathlib.Analysis.Complex.Circle
Circle.coe_one : ↑1 = 1
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_sub : ∀ {α : 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 α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      MeasureTheory.setToFun μ T hT (f - g) = MeasureTheory.setToFun μ T hT f - MeasureTheory.setToFun μ T hT g
-- Lean.Declaration
/-- List of all (including this one) declarations in the same mutual block.
See comment at `DefinitionVal.all`.  -/
Lean.TheoremVal.all : Lean.TheoremVal → List Lean.Name
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instRightCancelSemigroup : {α : Type u_1} → [RightCancelSemigroup α] → RightCancelSemigroup (Lex α)
-- Mathlib.Data.Fin.Fin2
Fin2.brecOn.go : {motive : (a : ℕ) → Fin2 a → Sort u} →
  {a : ℕ} → (t : Fin2 a) → ((a : ℕ) → (t : Fin2 a) → Fin2.below t → motive a t) → motive a t ×' Fin2.below t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ((m₁.inter! m₂).isEmpty = true ↔
        ∀ (k : α), Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k m₂ = false)
-- Mathlib.RingTheory.WittVector.MulP
WittVector.wittMulN.eq_def : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℕ),
  WittVector.wittMulN p x =
    match (motive := ℕ → ℕ → MvPolynomial ℕ ℤ) x with
    | 0 => 0
    | n.succ => fun k =>
      (MvPolynomial.bind₁ (Function.uncurry ![WittVector.wittMulN p n, MvPolynomial.X])) (WittVector.wittAdd p k)
-- Mathlib.Analysis.Normed.Group.Defs
enorm_lt_coe : ∀ {E : Type u_8} [inst : NNNorm E] {x : E} {r : NNReal}, ‖x‖ₑ < ↑r ↔ ‖x‖₊ < r
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.basis_apply_eq_mkQ : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} [inst_1 : NeZero n] {ι : Type u_4} (b : Module.Basis ι ℤ G) (i : ι),
  (ModN.basis b) i = (ModN.mkQ n) (b i)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : AddGroup β],
  FreeAddGroup.lift =
    { toFun := fun f => AddMonoidHom.mk' (Quot.lift (FreeAddGroup.Lift.aux f) ⋯) ⋯,
      invFun := fun g => ⇑g ∘ FreeAddGroup.of, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instMul : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Mul ↑(Set.Icc 0 1)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.tensor_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
  (g₂ : Y₂ ⟶ Z₂) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
        (CategoryTheory.CategoryStruct.comp f₂ g₂))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) h)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f g : P ⟶ Q), f.f = g.f → f = g
-- Lean.Elab.MutualInductive
/-- Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit.
 -/
Lean.Elab.Command.withExplicitToImplicit : {α : Type} → Array Lean.Expr → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Data.Fin.Tuple.Basic
Fin.comp_cons : ∀ {n : ℕ} {α : Sort u_1} {β : Sort u_2} (g : α → β) (y : α) (q : Fin n → α), g ∘ Fin.cons y q = Fin.cons (g y) (g ∘ q)
-- Init.PropLemmas
/-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`.
(This is sometimes taken as an alternate definition of decidability.)  -/
decidable_of_bool : {a : Prop} → (b : Bool) → (b = true ↔ a) → Decidable a
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonalRingHom_apply : ∀ (m : Type u_2) (o : Type u_4) (α : Type u_12) [inst : DecidableEq o] [inst_1 : DecidableEq m] [inst_2 : Fintype o]
  [inst_3 : Fintype m] [inst_4 : NonAssocSemiring α] (M : o → Matrix m m α),
  (Matrix.blockDiagonalRingHom m o α) M = Matrix.blockDiagonal M
-- Init.System.IO
/-- Times the execution of an `IO` action.

The provided message `msg` and the time take are printed to the current standard error as a side
effect.
 -/
timeit : {α : Type} → String → IO α → IO α
-- Lean.Class
Lean.ClassEntry.lt : Lean.ClassEntry → Lean.ClassEntry → Bool
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.sum_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : AddCommMonoid A] {p : MvPolynomial σ R}
  {b : (σ →₀ ℕ) → R → A}, p.coeff.sum b = ∑ m ∈ p.support, b m (MvPolynomial.coeff m p)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- a cofibration that is a section of `p`  -/
HomotopicalAlgebra.CofibrantBrownFactorization.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} → {f : X ⟶ Y} → (self : HomotopicalAlgebra.CofibrantBrownFactorization f) → Y ⟶ self.Z
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- A sheaf is constant if it is in the essential image of the constant sheaf functor.
 -/
CategoryTheory.Sheaf.IsConstant : {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] →
          [CategoryTheory.HasWeakSheafify J D] → CategoryTheory.Sheaf J D → Prop
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.isSplittingField_of_card_eq : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [inst : Field K] [inst_1 : Fintype K]
  [inst_2 : Algebra (ZMod p) K],
  Fintype.card K = p ^ n → Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toArray_rcc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...=n).toArray[i]?.isNone = true) = ((n + 1 - m).toNat ≤ i)
-- Init.Data.UInt.Basic
instAddUInt64 : Add UInt64
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.qr₁' : ∀ (a b : ℕ) (r : ℤ),
  a % 2 = 1 → b % 4 = 1 → Mathlib.Meta.NormNum.jacobiSymNat b a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiff.subtypeVal_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M']
  (U : TopologicalSpace.Opens M') (f : M → ↥U), ContMDiff I I' (↑⊤) (Subtype.val ∘ f) ↔ ContMDiff I I' (↑⊤) f
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.isUnit_algebraMap : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  IsUnit ((algebraMap R (ExteriorAlgebra R M)) r) ↔ IsUnit r
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.epimorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.MorphismProperty.epimorphisms C).RespectsIso
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Algebra.instIsScalarTowerCarrier : ∀ {S₀ : Type u₀} [inst : CommSemiring S₀] {S : Type u} [inst_1 : Ring S] [inst_2 : Algebra S₀ S] {M : ModuleCat S},
  IsScalarTower S₀ S ↑M
-- Mathlib.Algebra.Ring.Prod
RingHom.prod_apply : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R), (f.prod g) x = (f x, g x)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.cone_π_app : ∀ {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] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) [inst_2 : CategoryTheory.IsCofiltered J] (j : J), h.cone.π.app j = h.coneπApp j
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R),
  IsScalarTower R (Localization S) ↑(M.localizedModule S)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.compLinearMap_inj : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (f : (i : ι) → M₁ i →ₗ[R] M₁' i),
  (∀ (i : ι), Function.Surjective ⇑(f i)) →
    ∀ (g₁ g₂ : MultilinearMap R M₁' M₂), g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.η F)) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj T (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ennrealToMeasure.eq_1 : ∀ {α : Type u_1} {x : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ENNReal),
  v.ennrealToMeasure = MeasureTheory.Measure.ofMeasurable (fun s x_1 => v s) ⋯ ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.iInf_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  (S : ι → Subalgebra R A), (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Canonical increasing bijection from `Fin c.boundaries.card` to `c.boundaries`.  -/
CompositionAsSet.boundary : {n : ℕ} → (c : CompositionAsSet n) → Fin c.boundaries.card ↪o Fin (n + 1)
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseYear : (Std.Time.Year → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_comp_changeForm : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
  (h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q'),
  CliffordAlgebra.changeForm h' ∘ₗ CliffordAlgebra.changeForm h = CliffordAlgebra.changeForm ⋯
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃ : UInt8 → UInt8 → UInt8 → Option Char
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.throwUnexpected : {α : Type} → Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.GoalM α
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.comap_exp_nhds_zero : Filter.comap Complex.exp (nhds 0) = Filter.comap Complex.re Filter.atBot
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.map_id : ∀ {α : Type u} (s : Stream'.Seq1 α), Stream'.Seq1.map id s = s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.nsmul_neg_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] {n : ℕ} {x : M},
  0 < n → (n • x < 0 ↔ x < 0)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHBinOp : Lean.Expr → Bool
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensorInv_injective : ∀ {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R), Function.Injective ⇑(Module.Invertible.rTensorInv P Q e)
-- Lean.Data.JsonRpc
/-- Generic version of `Message.request`.

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

- [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#requestMessage)
- [JSON-RPC](https://www.jsonrpc.org/specification#request_object)
 -/
Lean.JsonRpc.Request : Type u → Type u
-- Mathlib.Topology.Algebra.UniformConvergence
instSMulCommClassUniformFun : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : SMul M β] [inst_1 : SMul N β]
  [SMulCommClass M N β], SMulCommClass M N (UniformFun α β)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_iff_mem_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] {a : α},
  a ∈ r ↔ a ∈ Std.PRange.UpwardEnumerable.least...r.upper
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.mem_of_normAtPlace_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x y : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K →
    (∀ (w : NumberField.InfinitePlace K),
        (NumberField.mixedEmbedding.normAtPlace w) y = (NumberField.mixedEmbedding.normAtPlace w) x) →
      y ∈ NumberField.mixedEmbedding.fundamentalCone K
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.compLeft_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {γ : Type u_5} [inst_3 : TopologicalSpace γ] [inst_4 : Zero γ] {g : C(β, γ)},
  g 0 = 0 →
    ∀ (f : CompactlySupportedContinuousMap α β) (a : α), (CompactlySupportedContinuousMap.compLeft g f) a = g (f a)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.vdecl.injEq : ∀ (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId)
  (ty_1 : Lean.IR.IRType) (e_1 : Lean.IR.Expr) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.vdecl x ty e b = Lean.IR.FnBody.vdecl x_1 ty_1 e_1 b_1) = (x = x_1 ∧ ty = ty_1 ∧ e = e_1 ∧ b = b_1)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.forget_reflects_isos : (CategoryTheory.forget CommMonCat).ReflectsIsomorphisms
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_top_iff : ∀ {K : Type u_2} [inst : Field K], NumberField.IsTotallyReal ↥⊤ ↔ NumberField.IsTotallyReal K
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.hasLimit_parallelPair_comp_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f.hom],
  CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.parallelPair f 0).comp P.ι)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_self_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⁅H, H⁆ = ⊥ ↔ IsMulCommutative ↥H