mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y_1).right.right =
    Y_1.right.right
-- Mathlib.RingTheory.Support
Submodule.localized.eq_1 : ∀ {R : Type u_1} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submonoid R) (M' : Submodule R M),
  Submodule.localized p M' = Submodule.localized' (Localization p) p (LocalizedModule.mkLinearMap p M) M'
-- Mathlib.Order.Hom.Bounded
TopHom.instSemilatticeSup : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : SemilatticeSup β] → [inst_2 : OrderTop β] → SemilatticeSup (TopHom α β)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) {Z : GrpCat}
  (h : (CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteGrp.ProfiniteCompletion.lift f)) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Order.WithBot
WithBot.eq_bot_iff_forall_ne : ∀ {α : Type u_1} {x : WithBot α}, x = ⊥ ↔ ∀ (a : α), ↑a ≠ x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions.mk : Bool → Lean.Lsp.RenameOptions
-- Mathlib.Algebra.Star.Subalgebra
/-- A \*-subalgebra is a subalgebra of a \*-algebra which is closed under `*`.  -/
StarSubalgebra : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] → [inst_3 : StarRing A] → [inst_4 : Algebra R A] → [StarModule R A] → Type v
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- If we're analytic at a point, we're analytic in a nonempty ball  -/
AnalyticAt.exists_ball_analyticOnNhd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {x : E}, AnalyticAt 𝕜 f x → ∃ r, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r)
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
Submodule.mem_orthogonalBilin_iff : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : CommSemiring R₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂]
  {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {S : Submodule R₁ M₁} {m : M₂},
  m ∈ Submodule.orthogonalBilin B S ↔ ∀ n ∈ S, (B n) m = 0
-- Mathlib.Order.Fin.Finset
Fin.orderIsoTriple_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c),
  ↑((Fin.orderIsoTriple a b c hab hbc) 0) = a
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R 2 = Polynomial.X ^ 2 - 1
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.isVariableInfo : Lean.Elab.HoverableInfoPrio → Bool
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateCohomologyFunctor.eq_1 : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (n : ℤ),
  tateCohomologyFunctor n =
    (tateComplexFunctor R G).comp (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.up ℤ) n)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.of_isEquivalence : ∀ {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.isomorphisms C, ∀ [L.IsEquivalence], L.IsLocalization W
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.image_symm_eq_preimage : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M₂),
  ⇑e.symm '' s = ⇑e ⁻¹' s
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mk_le_mk : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.Ring.OfSemiring.Q.mk (a₁, a₂) ≤ Lean.Grind.Ring.OfSemiring.Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁
-- Init.Dynamic
instNonemptyDynamic : Nonempty Dynamic
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousMul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M],
  ContinuousMul (SeparationQuotient M)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_self_sub_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), (f - g).neLocus f = g.support
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_sub_of_le : ∀ {a b : ISize}, 0 ≤ b → b ≤ a → (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
-- Mathlib.Analysis.Convex.Intrinsic
isClosed_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P},
  IsClosed ↑(affineSpan 𝕜 s) → IsClosed (intrinsicFrontier 𝕜 s)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀
      (q :
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
      (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
      ↑z.num ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔
        HomogeneousLocalization.mk z ∈ q.asIdeal
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMonoid.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instMonoid =
    { toSemigroup := SeparationQuotient.instSemigroup, toOne := SeparationQuotient.instOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inl_leftDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.leftDistrib X Y Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl
-- Mathlib.CategoryTheory.Shift.ShiftedHom
/-- The element of `ShiftedHom X Y m₀` (when `m₀ = 0`) attached to a morphism `X ⟶ Y`.  -/
CategoryTheory.ShiftedHom.mk₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {M : Type u_4} →
      [inst_1 : AddMonoid M] →
        [inst_2 : CategoryTheory.HasShift C M] →
          {X Y : C} → (m₀ : M) → m₀ = 0 → (X ⟶ Y) → CategoryTheory.ShiftedHom X Y m₀
-- Mathlib.Data.List.Sym
List.right_mem_of_mk_mem_sym2 : ∀ {α : Type u_1} {xs : List α} {a b : α}, s(a, b) ∈ xs.sym2 → b ∈ xs
-- Mathlib.LinearAlgebra.Projection
/-- `ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → (f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T)
-- Mathlib.Condensed.Light.TopComparison
/-- Associate to a `u`-small topological space the corresponding light condensed set, given by
`yonedaPresheaf`.
 -/
TopCat.toLightCondSet : TopCat → LightCondSet
-- Mathlib.Data.Subtype
Subtype.map_def : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)),
  Subtype.map f h = fun x => ⟨f ↑x, ⋯⟩
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent.eq_1 : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), I.toCotangent = (I • ⊤).mkQ
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_7} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜},
  IsUnit c → ∀ (f : α → β), MeasureTheory.HasFiniteIntegral (c • f) μ ↔ MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Algebra.Order.ZeroLEOne
ZeroLEOneClass.factZeroLeOne : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [ZeroLEOneClass α], Fact (0 ≤ 1)
-- Mathlib.Data.Set.Subset
Set.image_val_inter_self_left_eq_coe : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, Subtype.val '' D ∩ A = Subtype.val '' D
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
AddMonCat.Hom.Simps.hom : (X Y : AddMonCat) → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.reindex_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {β γ : Type}
  [inst_2 : Finite β] (ε : β ≃ γ) (f : γ → C) [inst_3 : CategoryTheory.Limits.HasBiproduct f]
  [inst_4 : CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)],
  (CategoryTheory.Limits.biproduct.reindex ε f).hom =
    CategoryTheory.Limits.biproduct.desc fun b => CategoryTheory.Limits.biproduct.ι f (ε b)
-- Mathlib.Topology.Gluing
TopCat.GlueData.mk.inj : ∀ {toGlueData : CategoryTheory.GlueData TopCat}
  {f_open : ∀ (i j : toGlueData.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData.f i j))}
  {toGlueData_1 : CategoryTheory.GlueData TopCat}
  {f_open_1 :
    ∀ (i j : toGlueData_1.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData_1.f i j))},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1
-- Lean.Elab.Do.Legacy
/-- This method assumes `expandDoIf?` is not applicable.  -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.mkDoIfView : Lean.Syntax → Lean.Elab.Term.Do.DoIfView
-- Init.Data.List.Find
List.findIdx?_isSome : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, (List.findIdx? p xs).isSome = xs.any p
-- Mathlib.Order.Filter.Defs
/-- `pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but
with this definition we have `s ∈ pure a` defeq `a ∈ s`.  -/
Filter.instPure : Pure Filter
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mk.injEq : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  (measureOf' : Set α → M) (empty' : measureOf' ∅ = 0)
  (not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0)
  (m_iUnion' :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf' (f i)) (measureOf' (⋃ i, f i)))
  (measureOf'_1 : Set α → M) (empty'_1 : measureOf'_1 ∅ = 0)
  (not_measurable'_1 : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'_1 i = 0)
  (m_iUnion'_1 :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf'_1 (f i)) (measureOf'_1 (⋃ i, f i))),
  ({ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' } =
      { measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1,
        m_iUnion' := m_iUnion'_1 }) =
    (measureOf' = measureOf'_1)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- The `Finsupp` version of `Finset.univ_sum_single`  -/
Finsupp.univ_sum_single : ∀ {α : Type u_1} {M : Type u_8} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α →₀ M), (∑ a, fun₀ | a => f a) = f
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Recursor for `WithZero` using the preferred forms `0` and `↑a`.  -/
WithZero.recZeroCoe : {α : Type u} → {motive : WithZero α → Sort u_1} → motive 0 → ((a : α) → motive ↑a) → (n : WithZero α) → motive n
-- Mathlib.Topology.Algebra.Group.Basic
IsCompact.neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] {s : Set G},
  IsCompact s → IsCompact (-s)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetricProjection.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, IsIdempotentElem T → T.IsSymmetric → T.IsSymmetricProjection
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.edist_nearestPt_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (x : α) {k N : ℕ}, k ≤ N → edist ((MeasureTheory.SimpleFunc.nearestPt e N) x) x ≤ edist (e k) x
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.matcherName : Lean.Meta.Match.MkMatcherInput → Lean.Name
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.mkNameFromParserSyntax.visit : Lean.Syntax → String → String
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE] (i' j' : ι') (hij' : c'.Rel i' j'), ⋯.δ i' j' hij' = 0
-- Std.Http.Transport
/-- Shared state for a bidirectional mock connection.
 -/
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState : Type
-- Mathlib.Logic.Function.Basic
/-- Records a way to turn an element of `α` into a function from `β` to `γ`. The most generic use
is to recursively uncurry. For instance `f : α → β → γ → δ` will be turned into
`↿f : α × β × γ → δ`. One can also add instances for bundled maps.  -/
Function.HasUncurry : Type u_5 → outParam (Type u_6) → outParam (Type u_7) → Type (max (max u_5 u_6) u_7)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  (Std.Internal.List.Const.alterKey k f l).isEmpty =
    ((l.isEmpty || l.length == 1 && Std.Internal.List.containsKey k l) && (f (Std.Internal.List.getValue? k l)).isNone)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonResolvableCompletionItemData : Lean.ToJson Lean.Lsp.ResolvableCompletionItemData
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.isMin : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α],
  Order.IsSuccPrelimit a → IsMin a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {v : β}, (k, v) ∈ Std.DHashMap.Raw.Const.toList ↑m ↔ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instCoeHeadValuesArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → CoeHead (RBTree.RBMap.Values α β cmp) (Array β)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_map : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
  {R' : Type u_8} (f : R → R'), (A₁.fromRows A₂).map f = (A₁.map f).fromRows (A₂.map f)
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.isLimitEquivSections_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (j : J) (x : c.pt),
  ↑((CategoryTheory.Limits.Types.isLimitEquivSections t) x) j = (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x
-- Std.Time.Date.PlainDate
/-- Adds a given number of days to a `PlainDate`.
 -/
Std.Time.PlainDate.addDays : Std.Time.PlainDate → Std.Time.Day.Offset → Std.Time.PlainDate
-- Mathlib.Order.Max
noTopOrder_iff : ∀ {α : Type u_1} [inst : LE α], NoTopOrder α ↔ ∀ (x : α), ¬IsTop x
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_id_map : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → ProbabilityTheory.complexMGF id (MeasureTheory.Measure.map X μ) = ProbabilityTheory.complexMGF X μ
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoGT.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  e.toRelIsoGT = { toEquiv := { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }.toEquiv, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_add : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t : Set α}, s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.none.sizeOf_spec : sizeOf Lean.Elab.Tactic.ResolveSimpIdResult.none = 1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀)
  (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k))
  (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (CategoryTheory.CategoryStruct.comp (z i' j' ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (z i j k)
      (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv
-- Lean.Meta.Closure
Lean.Meta.Closure.State.nextLevelIdx : Lean.Meta.Closure.State → ℕ
-- Mathlib.GroupTheory.Coset.Basic
/-- `α ⧸ ⊥` is in bijection with `α`. See `QuotientAddGroup.quotientBot` for an
additive version.  -/
QuotientAddGroup.quotientEquivSelf : (α : Type u_1) → [inst : AddGroup α] → α ⧸ ⊥ ≃ α
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.assump.injEq : ∀ (a a_1 : ℕ), (Mathlib.Tactic.Linarith.CompSource.assump a = Mathlib.Tactic.Linarith.CompSource.assump a_1) = (a = a_1)
-- Batteries.Recycling.RBTree.Basic
/-- True if `x` is equivalent to an element of `t`.  -/
RBTree.RBNode.Mem : {α : Type u_1} → (α → α → Ordering) → α → RBTree.RBNode α → Prop
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The over category has any connected limit which the original category has.  -/
CategoryTheory.CostructuredArrow.hasLimitsOfShape_of_isConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CostructuredArrow K B)
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.coe_toMultiplicative : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f : α →+ β),
  ⇑(AddMonoidHom.toMultiplicative f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Multiplicative.toAdd
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.is_compatible_of_exists_amalgamation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R),
  (∃ t, x.IsAmalgamation t) → x.Compatible
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.smoothingFn.eq_1 : ∀ (n : ℝ), AkraBazziRecurrence.smoothingFn n = 1 / Real.log n
-- Mathlib.Topology.Clopen
/-- Variant of `isClopen_inter_of_disjoint_cover_clopen` with weaker disjointness condition.  -/
isClopen_inter_of_disjoint_cover_clopen' : ∀ {X : Type u} [inst : TopologicalSpace X] {s a b : Set X},
  IsClopen s → s ⊆ a ∪ b → IsOpen a → IsOpen b → s ∩ a ∩ b = ∅ → IsClopen (s ∩ a)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.induct_unfolding : ∀ (s : String) (motive : ℕ → s.Pos → ℕ → Option (s.Pos × ℕ) → Prop),
  (∀ (p : s.Pos) (acc : ℕ), motive 0 p acc (some (p, acc))) →
    (∀ (acc k : ℕ), motive k.succ s.endPos acc none) →
      (∀ (p : s.Pos) (acc k : ℕ) (h : ¬p = s.endPos) (d : ℕ),
          Lean.fromHex?✝ (p.get h) = some d →
            motive k (p.next h) (acc <<< 4 ||| d) (Lean.parseLowerHex?✝ k s (p.next h) (acc <<< 4 ||| d)) →
              motive k.succ p acc (Lean.parseLowerHex?✝ k s (p.next h) (acc <<< 4 ||| d))) →
        (∀ (p : s.Pos) (acc k : ℕ) (h : ¬p = s.endPos), Lean.fromHex?✝ (p.get h) = none → motive k.succ p acc none) →
          ∀ (k : ℕ) (p : s.Pos) (acc : ℕ), motive k p acc (Lean.parseLowerHex?✝ k s p acc)
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- If `α` is equipped with the upper set topology, then it is homeomorphic to
`WithUpperSet α`.  -/
Topology.IsUpperSet.WithUpperSetHomeomorph : {α : Type u_1} →
  [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsUpperSet α] → Topology.WithUpperSet α ≃ₜ α
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.vecMul_injective_iff : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] {M : Matrix m n R},
  (Function.Injective fun v => Matrix.vecMul v M) ↔ LinearIndependent R M.row
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- To construct an isomorphism of cones over the walking cospan,
it suffices to construct an isomorphism
of the cone points and check it commutes with the legs to `left` and `right`.  -/
CategoryTheory.Limits.WalkingCospan.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      {s t : CategoryTheory.Limits.Cone F} →
        (i : s.pt ≅ t.pt) →
          s.π.app CategoryTheory.Limits.WalkingCospan.left =
              CategoryTheory.CategoryStruct.comp i.hom (t.π.app CategoryTheory.Limits.WalkingCospan.left) →
            s.π.app CategoryTheory.Limits.WalkingCospan.right =
                CategoryTheory.CategoryStruct.comp i.hom (t.π.app CategoryTheory.Limits.WalkingCospan.right) →
              (s ≅ t)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_pointReflection_right : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (𝕜 : Type u_5) [inst_3 : NormedField 𝕜] [NormedSpace 𝕜 V] (p q : P),
  dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_fst' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, proj x ∈ e.baseSet → (↑e x).1 = proj x
-- Init.Prelude
instHOrElseOfOrElse : {α : Type u_1} → [OrElse α] → HOrElse α α α