mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  (LinearMap.toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁
-- Mathlib.Data.Int.ModEq
Int.ext_ediv_modEq_iff : ∀ (n a b : ℤ), a = b ↔ a / n = b / n ∧ a ≡ b [ZMOD n]
-- Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
SymmetricAlgebra.counit_ι : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  CoalgebraStruct.counit ((SymmetricAlgebra.ι R M) x) = 0
-- Mathlib.Data.Set.Defs
/-- Pretty printing for set-builder notation with pattern matching.  -/
Mathlib.Meta.ofPredPatternMatchUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_top_eq_top_of_infinite : ∀ (V : Type u_4) [Infinite V], ⊤.chromaticNumber = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3),
  (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δ f₂ f₃ n₀ n₁ ⋯
-- Mathlib.Logic.Function.Basic
/-- **Cantor's diagonal argument** implies that there are no surjective functions from `α`
to `Set α`.  -/
Function.cantor_surjective : ∀ {α : Type u_4} (f : α → Set α), ¬Function.Surjective f
-- Lean.Data.AssocList
Lean.AssocList.instForInProdOfMonad : {α : Type u} → {β : Type v} → {m : Type w → Type w'} → [Monad m] → ForIn m (Lean.AssocList α β) (α × β)
-- Lean.Compiler.CSimpAttr
/-- If `e` (as a whole) matches a `[csimp]` theorem, returns the replacement expression.  -/
Lean.Compiler.CSimp.replaceConstant? : Lean.Environment → Lean.Expr → Lean.CoreM (Option Lean.Expr)
-- Mathlib.Dynamics.Flow
/-- The orbit of a point under a flow.  -/
Flow.orbit : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddMonoid τ] → Flow τ α → α → Set α
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0},
  F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 = G.obj 0 → F = G
-- Mathlib.Algebra.Group.Action.End
mulAutArrow_apply_apply : ∀ {G : Type u_1} {M : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : MulAction G A] [inst_2 : Monoid M] (x : G)
  (a : A → M) (a_1 : A), (mulAutArrow x) a a_1 = (x • a) a_1
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain.eq_1 : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K],
  ZSpan.fundamentalDomain b = {m | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1}
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A subset closed under the additive action inherits that action.  -/
SetLike.vadd : {S : Type u'} →
  {R : Type u} →
    {M : Type v} → [inst : VAdd R M] → [inst_1 : SetLike S M] → [hS : VAddMemClass S R M] → (s : S) → VAdd R ↥s
-- Mathlib.Topology.Constructions.SumProd
isOpenQuotientMap_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty Y],
  IsOpenQuotientMap Prod.fst
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) {Z_1 : CommRingCat}
  (h : X.presheaf.obj (Opposite.op V) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e)
      h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e) h)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The parts are ordered by increasing greatest element.  -/
OrderedFinpartition.parts_strictMono : ∀ {n : ℕ} (self : OrderedFinpartition n), StrictMono fun m => self.emb m ⟨self.partSize m - 1, ⋯⟩
-- Mathlib.Data.Finset.Sym
Finset.sym_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), {a}.sym n = {Sym.replicate n a}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The Weierstrass curve mapped over a ring homomorphism `f : R →+* A`.  -/
WeierstrassCurve.map : {R : Type u} →
  [inst : CommRing R] → WeierstrassCurve R → {A : Type v} → [inst_1 : CommRing A] → (R →+* A) → WeierstrassCurve A
-- Init.Data.String.Iterate
String.Slice.PosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad : {m : Type → Type u_1} →
  {n : Type u_2 → Type u_3} → {s : String.Slice} → [inst : Monad m] → [Monad n] → Std.IteratorLoop s.PosIterator m n
-- Mathlib.Data.ZMod.Units
ZMod.coe_int_inv_mul_eq_one : ∀ {n : ℕ} {x : ℤ}, IsCoprime x ↑n → (↑x)⁻¹ * ↑x = 1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₁ = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- Constructor for `Equivalence.IsTriangulated`.  -/
CategoryTheory.Equivalence.IsTriangulated.mk'' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.CommShift ℤ], E.inverse.IsTriangulated → E.IsTriangulated
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- Any vertex adjacent to a vertex of `C` and not lying in `K` must lie in `C`.
 -/
SimpleGraph.ComponentCompl.mem_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} (c d : V), c ∈ C → d ∉ K → G.Adj c d → d ∈ C
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolynomialOn : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {s : Set ((i : ι) → Em i)}, CPolynomialOn 𝕜 (⇑f) s
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from an additive magma to its quotient by
an additive congruence relation.  -/
AddCon.mkAddHom : {M : Type u_1} → [inst : Add M] → (c : AddCon M) → M →ₙ+ c.Quotient
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.right =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj
            (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt).obj
        CategoryTheory.Limits.WalkingCospan.right)
-- Lean.Server.References
Lean.Server.Reference.mk.sizeOf_spec : ∀ (ident : Lean.Lsp.RefIdent) (aliases : Array Lean.Lsp.RefIdent) (range : Lean.Lsp.Range) (stx : Lean.Syntax)
  (ci : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (isBinder : Bool),
  sizeOf
      { ident := ident, aliases := aliases, range := range, stx := stx, ci := ci, info := info, isBinder := isBinder } =
    1 + sizeOf ident + sizeOf aliases + sizeOf range + sizeOf stx + sizeOf ci + sizeOf info + sizeOf isBinder
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_pi_of_countable : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Set ι},
  Countable ↑s →
    ∀ {t : (i : ι) → Set (X i)},
      (∀ i ∈ s, MeasurableSet (t i)) → (MeasureTheory.Measure.infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.getD (Std.DTreeMap.filter f t) k fallback =
      (Option.filter (fun x => f k' x) (Std.DTreeMap.Const.get? t k)).getD fallback
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ},
  Set.MapsTo T F F →
    ∀ [U.IsSymm],
      n ≠ 0 →
        ∀ {s : Finset X},
          Dynamics.IsDynCoverOf T F U n ↑s → Dynamics.coverEntropyEntourage T F (U.comp U) ≤ (↑s.card).log / ↑n
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_sup : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => x.1 ⊔ x.2
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.State.mk.inj : ∀ {cache : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64}
  {keyToExprs : Std.HashMap UInt64 (List Lean.Expr)}
  {cache_1 : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64}
  {keyToExprs_1 : Std.HashMap UInt64 (List Lean.Expr)},
  { cache := cache, keyToExprs := keyToExprs } = { cache := cache_1, keyToExprs := keyToExprs_1 } →
    cache = cache_1 ∧ keyToExprs = keyToExprs_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.forEachEqcRoot : (Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_iff_exists_forall_reachable : ∀ {V : Type u} (G : SimpleGraph V), G.Connected ↔ ∃ v, ∀ (w : V), G.Reachable v w
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.map f t) k fallback =
        (Option.map (f k') (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.a : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      {n : ℕ} → {Z : C} → AlgebraicTopology.DoldKan.MorphComponents X n Z → (X.obj (Opposite.op { len := n + 1 }) ⟶ Z)
-- Init.WF
WellFounded.transGen : ∀ {α : Sort u_1} {r : α → α → Prop}, WellFounded r → WellFounded (Relation.TransGen r)
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_lieInvariant : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LinearMap.BilinForm.lieInvariant L (LieModule.traceForm R L M)
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α},
  Dense s → ∀ (x : α), ∃ y ∈ s, x < y
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.x_mul : ∀ {d : ℤ} (a b : Pell.Solution₁ d), (a * b).x = a.x * b.x + d * (a.y * b.y)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_prod : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The morphism `tensorObj X Y₁ ⟶ tensorObj X Y₂` induced by a morphism of graded objects
`φ : Y₁ ⟶ Y₂`.  -/
CategoryTheory.GradedObject.Monoidal.whiskerLeft : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X : CategoryTheory.GradedObject I C) →
            {Y₁ Y₂ : CategoryTheory.GradedObject I C} →
              (Y₁ ⟶ Y₂) →
                [inst_3 : X.HasTensor Y₁] →
                  [inst_4 : X.HasTensor Y₂] →
                    CategoryTheory.GradedObject.Monoidal.tensorObj X Y₁ ⟶
                      CategoryTheory.GradedObject.Monoidal.tensorObj X Y₂
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (y : OreLocalization S R) (x : OreLocalization S X),
  y.smul x = OreLocalization.liftExpand (fun x1 x2 => OreLocalization.smul''✝ x1 x2 x) ⋯ y
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_nonneg : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], 0 ≤ schnirelmannDensity A
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.comp_apply : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G] {H : Type u → Type s}
  [inst_2 : Applicative H] (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) {α : Type u}
  (x : F α), (fun {α} => (η'.comp η).app α) x = (fun {α} => η'.app α) ((fun {α} => η.app α) x)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_self : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Ioc a a = ∅
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_generateFrom : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, t ∈ s → MeasurableSet t
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (p₁ p₂ : Int.Internal.Linear.Poly) (a_1 b_1 : Lean.Expr) (p₁_1 p₂_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core a b p₁ p₂ =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core a_1 b_1 p₁_1 p₂_1) =
    (a = a_1 ∧ b = b_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1)
-- Init.Data.Float.Model.Unpacked.Round
/-- Rounds the given mantissa with the given accuracy according to the
round-to-nearest strategy, with ties breaking in favor of even
mantissas.
 -/
Float.Model.UnpackedFloat.Accuracy.roundToNearestEven : ℕ → Float.Model.UnpackedFloat.Accuracy → ℕ
-- Std.Http.Protocol.H1.Message
/-- Gets the message head type based on direction.
 -/
Std.Http.Protocol.H1.Message.Head : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals.injEq : ∀ (stx : Lean.TSyntax `tactic) (goals : List Lean.MessageData) (stx_1 : Lean.TSyntax `tactic)
  (goals_1 : List Lean.MessageData),
  (Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals✝ stx goals =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals✝ stx_1 goals_1) =
    (stx = stx_1 ∧ goals = goals_1)
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_single : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} (i : ι k) (m : M),
  (fun₀ | i => m).embSigma = fun₀ | ⟨k, i⟩ => m
-- Mathlib.Algebra.Algebra.Unitization
Unitization.linearMap_ext : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [inst : CommSemiring S] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S A]
  [inst_6 : Module S N] ⦃f g : Unitization R A →ₗ[S] N⦄,
  (∀ (r : R), f (Unitization.inl r) = g (Unitization.inl r)) → (∀ (a : A), f ↑a = g ↑a) → f = g
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If `F i → f` in `L1`, then `∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ]`.  -/
MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1 : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} (f : X → E),
  MeasureTheory.AEStronglyMeasurable f μ.variation →
    ∀ {F_1 : ι → X → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, μ.Integrable (F_1 i)) →
        Filter.Tendsto (fun i => ∫⁻ (x : X), ‖F_1 i x - f x‖ₑ ∂μ.variation) l (nhds 0) →
          ∀ (s : Set X),
            Filter.Tendsto (fun i => ∫ᵛ (x : X) in s, F_1 i x ∂[B; μ]) l (nhds ∫ᵛ (x : X) in s, f x ∂[B; μ])
-- Init.Data.List.Nat.Basic
List.getElem_intersperse : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : i < (List.intersperse sep l).length),
  (List.intersperse sep l)[i] = if i % 2 = 0 then l[i / 2] else sep
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `F` has a limit, then the limit projections can be interpreted as structured arrows
`limit F ⟶ F.obj -`.  -/
CategoryTheory.Limits.limit.toStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Functor J (CategoryTheory.StructuredArrow (CategoryTheory.Limits.limit F) F)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.dArrowIso₀₁_hom_right : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.dArrowIso₀₁ A).hom.right = (groupCohomology.cochainsIso₁ A).hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' fallback : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKeyD k' fallback =
        if compare k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Init.Data.Array.Basic
/-- Returns a new array that contains the first `i` elements of `xs`. If `xs` has fewer than `i`
elements, the new array contains all the elements of `xs`.

The returned array is always a new array, even if it contains the same elements as the input array.

Examples:
* `#["red", "green", "blue"].take 1 = #["red"]`
* `#["red", "green", "blue"].take 2 = #["red", "green"]`
* `#["red", "green", "blue"].take 5 = #["red", "green", "blue"]`
 -/
Array.take : {α : Type u} → Array α → ℕ → Array α
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Coyoneda.colimitCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) (x : C),
  (CategoryTheory.Coyoneda.colimitCocone X).ι.app x = TypeCat.ofHom fun x_1 => id PUnit.unit
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : AlgebraicGeometry.LocallyRingedSpace}
  (h : Z.toLocallyRingedSpace ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toLRSHom (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toLRSHom f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toLRSHom g) h)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_sSup : ∀ {M : Type u_2} [inst : Mul M] (S : Set (Subsemigroup Mᵐᵒᵖ)), (sSup S).unop = sSup (Subsemigroup.op ⁻¹' S)
-- Mathlib.Order.Monotone.Basic
/-- If `f` is a monotone function from `ℕ` to a preorder such that `x` lies between `f n` and
`f (n + 1)`, then `x` doesn't lie in the range of `f`.  -/
Monotone.ne_of_lt_of_lt_nat : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α},
  Monotone f → ∀ (n : ℕ) {x : α}, f n < x → x < f (n + 1) → ∀ (a : ℕ), f a ≠ x
-- Init.Data.Int.Order
Int.add_le_add_right : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), a + c ≤ b + c
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.getKey? a Std.DHashMap.Internal.AssocList.nil = none
-- Mathlib.Order.WellFoundedSet
/-- Higman's Lemma, which states that for any reflexive, transitive relation `r` which is
partially well-ordered on a set `s`, the relation `List.SublistForall₂ r` is partially
well-ordered on the set of lists of elements of `s`. That relation is defined so that
`List.SublistForall₂ r l₁ l₂` whenever `l₁` related pointwise by `r` to a sublist of `l₂`.  -/
Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ : ∀ {α : Type u_2} (r : α → α → Prop) [IsPreorder α r] {s : Set α},
  s.PartiallyWellOrderedOn r → {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_surjective_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f → Function.Surjective (FirstOrder.Language.Substructure.comap f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMergeWith : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.Equiv t₂ →
    t₃.Equiv t₄ →
      ∀ (h₁ : t₁.WF) (h₂ : t₂.WF),
        t₃.WF →
          t₄.WF →
            ∀ {f : α → β → β → β},
              (Std.DTreeMap.Internal.Impl.Const.mergeWith f t₁ t₃ ⋯).impl.Equiv
                (Std.DTreeMap.Internal.Impl.Const.mergeWith f t₂ t₄ ⋯).impl
-- Mathlib.ModelTheory.Basic
/-- The inverse of a first-order equivalence is a first-order equivalence.  -/
FirstOrder.Language.Equiv.symm : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → L.Equiv N M
-- Mathlib.Analysis.Complex.Basic
IsCompact.reProdIm : ∀ {s t : Set ℝ}, IsCompact s → IsCompact t → IsCompact (s ×ℂ t)