mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- A functor has an underlying refl prefunctor.  -/
CategoryTheory.Functor.toReflPrefunctor : {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] → CategoryTheory.Functor C D → C ⥤rq D
-- Batteries.Data.String.Legacy
/-- Folds a function over a substring from the left, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `Substring.Raw.foldl`.
 -/
Substring.Raw.Legacy.foldl : {α : Type u} → (α → Char → α) → α → Substring.Raw → α
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_lt_mul_of_neg_left : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a < b → c < 0 → c * b < c * a
-- Mathlib.Order.WithBot
WithBot.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α],
  WithBot.instPreorder =
    { toLE := WithBot.instLE, toLT := WithBot.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_replaceEntry_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.containsKey k l = false →
    Std.Internal.List.getEntry? a (Std.Internal.List.replaceEntry k v l) = Std.Internal.List.getEntry? a l
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_irreducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a : α}, Irreducible a → UniqueFactorizationMonoid.normalizedFactors a = {normalize a}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} {k : α},
  Std.DTreeMap.Const.insertManyIfNewUnit t [k] = t.insertIfNew k ()
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_carrier : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x : L}, x ∈ L'.carrier ↔ x ∈ ↑L'
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Mapping an element `j` of `Fin n` to the element in the block containing it, identified with
`Fin (c.blocksFun (c.index j))` through the canonical increasing bijection.  -/
Composition.invEmbedding : {n : ℕ} → (c : Composition n) → (j : Fin n) → Fin (c.blocksFun (c.index j))
-- Aesop.RuleTac.ElabRuleTerm
Aesop.matchInductiveTypeSynonym? : Lean.Name → Lean.MetaM (Option Lean.InductiveVal)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_inj`.

---

A variant of `SkewMonoidAlgebra.ofCoeff_injective` in terms of `Iff`.  -/
SkewMonoidAlgebra.ofFinsupp_inj : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : G →₀ k}, { coeff := a } = { coeff := b } ↔ a = b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsert.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.containsThenInsert a b = t_1.containsThenInsert a b_1
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_le_orderOf : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M},
  0 < orderOf m → ∀ (a : α), MulAction.period m a ≤ orderOf m
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
this is the split monomormphism from the chain complex `s.nondegComplex` to
the alternating face map complex of `X`.  -/
CategoryTheory.SimplicialObject.Splitting.fromNondegComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        [inst_1 : CategoryTheory.Preadditive C] → s.nondegComplex ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.valuationSubring_not_isField : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup] [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup],
  ¬IsField ↥v.valuationSubring
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk'_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsFibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y]
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))),
  (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).p =
    CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_fst_prod : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith 1 l f' fun x => (f' x, g' x)
-- Lean.Parser.Extra
Lean.Parser.sepByElemParser.parenthesizer : Lean.PrettyPrinter.Parenthesizer → String → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_one_lt_of_lt : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a < b → a + 1 < b
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- The pointwise intersection of an upper hemicontinuous function with a fixed closed set is
upper hemicontinuous.  -/
UpperHemicontinuousOn.inter : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  UpperHemicontinuousOn f s → ∀ {u : Set β}, IsClosed u → UpperHemicontinuousOn (fun x => f x ∩ u) s
-- Mathlib.Topology.Algebra.Monoid
Topology.IsInducing.continuousAdd : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N] [ContinuousAdd N] (f : F),
  Topology.IsInducing ⇑f → ContinuousAdd M
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_compl : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f : α → G), sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
-- Init.Data.Array.Bootstrap
Array.toList_append : ∀ {α : Type u_1} {xs ys : Array α}, (xs ++ ys).toList = xs.toList ++ ys.toList
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The Picard iteration. It will be shown that if `α : ℝ → E` and `picard f t₀ x₀ α` agree on an
interval containing `t₀`, then `α` is a solution to `f` with `α t₀ = x₀` on this interval.  -/
ODE.picard : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E → E) → ℝ → E → (ℝ → E) → ℝ → E
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_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.cokernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.sInf_glb : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (S : Set (LieSubalgebra R L)), IsGLB S (sInf S)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 5`.  -/
CategoryTheory.ComposableArrows.mk₅ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X₀ X₁ X₂ X₃ X₄ X₅ : C} →
      (X₀ ⟶ X₁) → (X₁ ⟶ X₂) → (X₂ ⟶ X₃) → (X₃ ⟶ X₄) → (X₄ ⟶ X₅) → CategoryTheory.ComposableArrows C 5
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- An equivalence between the type of objects underlying a category and the type of 0-simplices in
the 2-truncated nerve.  -/
SSet.OneTruncation₂.nerveEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve C)) ≃ C
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.mk : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  Set.MapsTo f A B →
    (∀ ⦃s t : Multiset α⦄,
        (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
          (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
            s.card = n → t.card = n → s.prod = t.prod → (Multiset.map f s).prod = (Multiset.map f t).prod) →
      IsMulFreimanHom n A B f
-- Mathlib.Topology.Sequences
/-- If `x : ℕ → X` has no convergent subsequence, then `⋃ i, closure {x i}` is closed.  -/
isClosed_iUnion_closure_singleton_of_not_tendsto : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : ℕ → X} [SequentialSpace X],
  (∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Filter.Tendsto (x ∘ φ) Filter.atTop (nhds l)) → IsClosed (⋃ i, closure {x i})
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.isPullback_of_binaryFan_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y Z : CategoryTheory.Over X}
  (c : CategoryTheory.Limits.BinaryFan Y Z) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.IsPullback (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) Y.hom Z.hom
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The commutator of `G` as a morphism. This is the map `(x, y) ↦ x + y + (-x) + (-y)`,
see `CategoryTheory.AddGrpObj.lift_commutator_eq_add_add_neg_neg`.
This morphism is constant with value `0` if and only if `G` is commutative
(see `CategoryTheory.isCommAddMonObj_iff_commutator_eq_toAddUnit_η`).  -/
CategoryTheory.AddGrpObj.addCommutator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.AddGrpObj G] → CategoryTheory.MonoidalCategoryStruct.tensorObj G G ⟶ G
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk_eq_top : ∀ {M : Type u_1} [inst : Mul M] (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier),
  { carrier := carrier, mul_mem' := mul_mem' } = ⊤ ↔ carrier = Set.univ
-- Mathlib.Algebra.Torsor.Basic
Set.prod_vsub_prod_comm : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (s₁ s₂ : Set P) (t₁ t₂ : Set P'),
  s₁ ×ˢ t₁ -ᵥ s₂ ×ˢ t₂ = (s₁ -ᵥ s₂) ×ˢ (t₁ -ᵥ t₂)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod.lift_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁)
  (τ₂ : F ⟶ F₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂)
      CategoryTheory.FunctorToTypes.prod.fst =
    τ₁
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_eq_one_iff_inv_eq : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit a → (a * b = 1 ↔ a⁻¹ = b)
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.lTensorAlgEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (A : Type u_5) (B : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CommMonoid M],
  MonoidAlgebra.lTensorAlgEquiv R A B =
    (Algebra.TensorProduct.comm R (MonoidAlgebra A M) B).trans
      ((MonoidAlgebra.rTensorEquivAlgEquiv R R B A).trans
        (MonoidAlgebra.mapAlgEquiv R M (Algebra.TensorProduct.comm R B A)))
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.and_left : ∀ (lhs rhs : Bool), (lhs && rhs) = true → lhs = true
-- Lean.Meta.DiscrTree.Util
/-- Extract the keys and values stored in a `DiscrTree`.
 -/
Lean.Meta.DiscrTree.toArray : {α : Type} → Lean.Meta.DiscrTree α → Array (Array Lean.Meta.DiscrTree.Key × α)
-- Lean.Elab.MutualInductive
/-- Given a universe level `u`, computes a simplified representative `u' ≤ u` such that
`u` and `u'` are equivalent *at infinity*. This means that `u = u'` for all
sufficiently large assignments of parameters or metavariables in `u` and `u'`.
If `u` is non-constant, this procedure effectively removes the constant part.

The primary example is `max a b ≈ a` if `a` has variables and `b` is constant.
For example, `max ?u 1` and `?u` are equivalent at infinity, since they are equal for all `?u ≥ 1`.

Options:
- If `paramConst = true`, then parameters are treated like constants (only metavariables
  are considered to be varying).
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.simplifyResultingUniverse : Lean.Level → optParam Bool false → Lean.Level
-- Std.Http.Protocol.H1.Reader
/-- State that it completed a single request or response and can go to the next one
 -/
Std.Http.Protocol.H1.Reader.State.complete : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.HasMap.isUnit_derivative_f : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) {x : S}, P.HasMap x → IsUnit ((Polynomial.aeval x) (Polynomial.derivative P.f))
-- Init.Data.Sum.Basic
Sum.isLeft_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β}, (Sum.inr x).isLeft = false
-- Mathlib.Topology.UniformSpace.Basic
/-- Entourages are neighborhoods of the diagonal.  -/
nhds_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] (x : α), nhds (x, x) ≤ uniformity α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.cos_eq_zero_iff : ∀ {θ : ℝ}, Real.cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * Real.pi / 2
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
has a right adjoint.  -/
CategoryTheory.ExponentiableMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} → (f : I ⟶ J) → [CategoryTheory.ChosenPullbacksAlong f] → Type (max u v)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.homeomorphProd_apply : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (x : Bundle.TotalSpace F fun x => F), (Bundle.Trivial.homeomorphProd B F) x = (x.proj, x.snd)
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- Variant of `algebraicIndependent_of_finite_type` using `Transcendental`.  -/
algebraicIndependent_of_finite_type' : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  Function.Injective ⇑(algebraMap R A) →
    (∀ (t : Set ι),
        t.Finite →
          (AlgebraicIndependent R fun i => x ↑i) → ∀ i ∉ t, Transcendental (↥(Algebra.adjoin R (x '' t))) (x i)) →
      AlgebraicIndependent R x
-- Init.Data.BitVec.Bitblast
BitVec.toInt_dvd_toInt_iff_of_msb_true_msb_false : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → y.msb = false → (y.toInt ∣ x.toInt ↔ -x % y = 0#w)
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Icc : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p),
  (∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) →
    Finset.map (Function.Embedding.subtype p) (Finset.Icc a b) = Finset.Icc ↑a ↑b
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (k₁ k₂ : ℤ)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ with
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
    | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_1 k₁ k₂
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoLetVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.params : Lean.Elab.ComputedFields.Context → Array Lean.Expr
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.lcoeff_apply : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (f : Polynomial R), (Polynomial.lcoeff R n) f = f.coeff n
-- Lean.SubExpr
Lean.SubExpr.Pos.instRepr : Repr Lean.SubExpr.Pos
-- Init.Data.Order.MinMaxOn
minOn_assoc : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α},
  minOn f (minOn f x y) z = minOn f x (minOn f y z)
-- Mathlib.RingTheory.FiniteLength
isFiniteLength_iff_exists_compositionSeries : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsFiniteLength R M ↔ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.mk : Lean.Name → Bool → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.SimprocOLeanEntry
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone is a colimit cocone iff its extension by an isomorphism is.  -/
CategoryTheory.Limits.IsColimit.extendIsoEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cocone F} →
            {X : C} →
              (i : s.pt ⟶ X) →
                [CategoryTheory.IsIso i] →
                  CategoryTheory.Limits.IsColimit s ≃ CategoryTheory.Limits.IsColimit (s.extend i)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.liftHom_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T]
  (hx' : (Polynomial.aeval x) f = 0) (z : Polynomial R), (h.liftHom x hx') (h.map z) = (Polynomial.aeval x) z
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.Quotient.inner_mk_mk : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x y : E),
  x ∈ Kᗮ → y ∈ Kᗮ → inner 𝕜 (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) = inner 𝕜 x y
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.isTopCompl_range_ker_of_leftInverse : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace N] [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f₁ : M →L[R] N) (f₂ : N →L[R] M),
  Function.LeftInverse ⇑f₂ ⇑f₁ → Submodule.IsTopCompl (↑f₁).range (↑f₂).ker
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtTreeMap.ofList l cmp = ∅ ↔ l = []
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The cocone `coconeOfHasColimitCurryCompColim` is in fact a limit cocone.
 -/
CategoryTheory.Limits.isColimitCoconeOfHasColimitCurryCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [inst_4 :
                    CategoryTheory.Limits.HasColimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfHasColimitCurryCompColim G)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).X i =
    CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
      (CategoryTheory.Limits.pullback.snd g (𝒰.f i))
-- Mathlib.Data.Sym.Basic
Sym.oneEquiv_apply : ∀ {α : Type u_1} (a : α), Sym.oneEquiv a = ⟨{a}, ⋯⟩
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.sum.match_3.splitter : (C : Type u_1) →
  (D : Type u_2) →
    (motive : C ⊕ D → Sort u_3) →
      (X : C ⊕ D) → ((X : C) → motive (Sum.inl X)) → ((X : D) → motive (Sum.inr X)) → motive X
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_inj : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S T : Subsemiring Rᵐᵒᵖ}, S.unop = T.unop ↔ S = T
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.size ≤ (t.insert k v).size
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.unop : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → αᵐᵒᵖ}, Summable f L → Summable (MulOpposite.unop ∘ f) L
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toList_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdxM m pos).toList = pure (List.drop pos xs.toList)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.ringEquivOpMop_apply : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (a : ↥S.toSubsemiring),
  S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombination.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
  Finset.affineCombination k s p =
    { toFun := fun w => (s.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯,
      linear := s.weightedVSub p, map_vadd' := ⋯ }
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J],
  CategoryTheory.InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)