mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_1.congr_eq_3 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (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₂))
  (a : ℤ) (x : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly) (k₂ : ℤ),
  p₁ = Int.Internal.Linear.Poly.add a x p →
    p₂ = Int.Internal.Linear.Poly.num k₂ →
      (match p₁, p₂ 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_3 a x p k₂
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.findLongestPrefix?.loop : {α : Type u_1} → {β : Type u_2} → (cmp : α → α → Ordering) → Option β → Lean.PrefixTreeNode α β cmp → List α → Option β
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Add a morphism to a pre-`0`-hypercover.  -/
CategoryTheory.PreZeroHypercover.add : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreZeroHypercover S → {T : C} → (T ⟶ S) → CategoryTheory.PreZeroHypercover S
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_hom_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.snd f g)) h
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr₂.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (motive : List α → List β → γ → Sort u_3) (x : List β) (c : γ)
  (h_1 : (x : List β) → (c : γ) → motive [] x c) (h_2 : (x : List α) → (c : γ) → motive x [] c)
  (h_3 : (x : α) → (xr : List α) → (y : β) → (yr : List β) → (c : γ) → motive (x :: xr) (y :: yr) c),
  (match [], x, c with
    | [], x, c => h_1 x c
    | x, [], c => h_2 x c
    | x :: xr, y :: yr, c => h_3 x xr y yr c) =
    h_1 x c
-- Mathlib.Topology.UniformSpace.Completion
/-- Embedding of `α` into its completion `CauchyFilter α`  -/
CauchyFilter.pureCauchy : {α : Type u} → [inst : UniformSpace α] → α → CauchyFilter α
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_le_iff_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (n : WithBot ℕ), f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- The image of `SL(n, ℤ)` in `SL(n, ℝ)` is discrete.  -/
Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRangeSL : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n],
  DiscreteTopology ↥(Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)).range
-- Mathlib.Data.DFinsupp.Module
DFinsupp.isCentralScalar : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → SMulZeroClass γ (β i)]
  [inst_2 : (i : ι) → SMulZeroClass γᵐᵒᵖ (β i)] [∀ (i : ι), IsCentralScalar γ (β i)],
  IsCentralScalar γ (Π₀ (i : ι), β i)
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.div_right : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b c : G₀}, Commute a b → Commute a c → Commute a (b / c)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  UniqueFactorizationMonoid.radical a ∣ UniqueFactorizationMonoid.radical b ↔
    UniqueFactorizationMonoid.normalizedFactors a ⊆ UniqueFactorizationMonoid.normalizedFactors b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α},
  k ∈ m.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.X_eq_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2
-- Mathlib.Order.Filter.Extr
isMaxOn_univ_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMaxOn f Set.univ a ↔ ∀ (x : α), f x ≤ f a
-- Init.Data.SInt.Lemmas
Int64.add_neg_eq_sub : ∀ {a b : Int64}, a + -b = a - b
-- Mathlib.Analysis.Convex.Between
affineSegment.eq_1 : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P),
  affineSegment R x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1
-- Mathlib.Data.NNRat.Defs
NNRat.den.eq_1 : ∀ (q : ℚ≥0), q.den = (↑q).den
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertOffsetX : Std.Time.OffsetX → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteAtBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.FiniteAtFilter ⊥
-- Mathlib.GroupTheory.SemidirectProduct
/-- The canonical map `N →* N ⋊[φ] G` sending `n` to `⟨n, 1⟩`  -/
SemidirectProduct.inl : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N →* N ⋊[φ] G
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (a : ℕ) → motive (Int.negSucc a) 0)
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n.succ with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc a, 0 => h_3 a
    | Int.negSucc m, Int.ofNat n.succ => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_4 m n
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.biSup_finset : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M),
  (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Mathlib.Data.Finsupp.Basic
Finsupp.graph_eq_empty : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, f.graph = ∅ ↔ f = 0
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.toNormSeqResult : Aesop.DisplayRuleName → Aesop.NormRuleResult → Aesop.NormSeqResult
-- Mathlib.Data.Nat.Factorization.Basic
/-- The set of positive powers of prime `p` that divide `n` is exactly the set of
positive natural numbers up to `n.factorization p`.  -/
Nat.Icc_factorization_eq_pow_dvd : ∀ (n : ℕ) {p : ℕ}, Nat.Prime p → Finset.Icc 1 (n.factorization p) = {i ∈ Finset.Ico 1 n | p ^ i ∣ n}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey?.isSome = true
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
CommRingCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.top_prod_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N], ⊤.prod ⊤ = ⊤
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticWithinAt.clog : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  AnalyticWithinAt ℂ f s x → f x ∈ Complex.slitPlane → AnalyticWithinAt ℂ (fun z => Complex.log (f z)) s x
-- Mathlib.Util.Export
Lean.Export.exportExpr : Lean.Expr → Lean.ExportM ℕ
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- Try to use the universal property of the span (e.g., `Submodule.span_induction`) instead of
this.  -/
Ideal.span_eq_map_homogeneousSubmodule : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : ι → R),
  Ideal.span (Set.range x) = Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R 1)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme}
  (h : CategoryTheory.Limits.multicoequalizer (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram i) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) h
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.IsHashSelf.hashes_to : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Array (Std.DHashMap.Internal.AssocList α β)},
  Std.DHashMap.Internal.IsHashSelf m →
    ∀ (i : ℕ) (h : i < m.size), Std.DHashMap.Internal.List.HashesTo m[i].toList i m.size
-- Mathlib.Topology.Irreducible
Function.Surjective.irreducibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Function.Surjective f → ∀ [IrreducibleSpace X], IrreducibleSpace Y
-- Mathlib.Data.ZMod.IntUnitsPower
/-- There is a canonical power operation on `ℤˣ` by `R` if `Additive ℤˣ` is an `R`-module.

In lemma names, this operation is called `uzpow` to match `zpow`.

Notably this is satisfied by `R ∈ {ℕ, ℤ, ZMod 2}`.  -/
Int.instUnitsPow : {R : Type u_1} → [inst : CommSemiring R] → [Module R (Additive ℤˣ)] → Pow ℤˣ R
-- Mathlib.CategoryTheory.Thin
/-- To show `X ≅ Y` in a thin category, it suffices to just give any morphism in each direction.  -/
CategoryTheory.iso_of_both_ways : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [Quiver.IsThin C] → {X Y : C} → (X ⟶ Y) → (Y ⟶ X) → (X ≅ Y)
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The equivalence `(ULift (Multiplicative ℤ) →* G) ≃ G` for any group `G`.  -/
uliftZPowersHom : (G : Type u) → [inst : Group G] → G ≃ (ULift.{u, 0} (Multiplicative ℤ) →* G)
-- Init.Data.Ord.Basic
Ordering.isLE_iff_eq_lt_or_eq_eq : ∀ {o : Ordering}, o.isLE = true ↔ o = Ordering.lt ∨ o = Ordering.eq
-- Mathlib.MeasureTheory.Measure.Prod
/-- `Prod.fst ⁻¹' s` is null measurable w.r.t. `μ.prod ν` iff `s` is null measurable w.r.t. `μ`
provided that `ν ≠ 0`.  -/
MeasureTheory.Measure.nullMeasurableSet_preimage_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [NeZero ν] {s : Set α},
  MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instNeBotSymmetricIcc : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G] [Filter.atTop.NeBot],
  (SummationFilter.symmetricIcc G).NeBot
-- Mathlib.Algebra.Symmetrized
SymAlg.addCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid αˢʸᵐ
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integral_le_measure_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ],
  ∫ (x : E), ↑f x ∂μ ≤ μ.real (Metric.closedBall c f.rOut)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.or_neg : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] (i : ι), b.IsPos i ∨ b.IsPos (-i)
-- Lean.Data.Options
Lean.Options.instToString : ToString Lean.Options
-- Mathlib.Topology.Algebra.Order.Group
Continuous.abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G}, Continuous f → Continuous fun x => |f x|
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.instInhabitedId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → {g : c ⟶ a} → Inhabited (CategoryTheory.Bicategory.LeftLift (CategoryTheory.CategoryStruct.id a) g)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_mul_degree_add_degree : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R),
  (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff
-- Mathlib.Algebra.Category.Grp.Basic
GrpMax.eq_1 : GrpMax = GrpCat
-- Init.Data.String.Basic
String.Slice.Pos.offset_sliceFrom : ∀ {s : String.Slice} {p₀ pos : s.Pos} {h : p₀ ≤ pos}, (p₀.sliceFrom pos h).offset = pos.offset.unoffsetBy p₀.offset
-- Mathlib.Tactic.NormNum.BigOperators
/-- This represents the result of trying to determine whether the given expression `n : Q(ℕ)`
is either `zero` or `succ`.  -/
Mathlib.Meta.Nat.UnifyZeroOrSuccResult : Q(ℕ) → Type
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_toLinearMap : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), ⇑↑f = ⇑f
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.tail : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Primrec' fun v => f v.tail
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- When `m = 0` this makes a term of `cycles A 0` from any element of `A` (or more precisely
any element in the kernel of `d₀,₀ = 0`). When `m` is positive, this makes a term of `cycles A m`
from any element of the kernel of `dₘ,ₘ₋₁`.  -/
groupHomology.cyclesMk : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {A : Rep.{u, u, u} k G} →
        (m n : ℕ) →
          (ComplexShape.down ℕ).next m = n →
            (f : (Fin m → G) →₀ ↑A) →
              (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains A).d m n)) f = 0 →
                ↑(groupHomology.cycles A m)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination with `affineCombinationSingleWeights` gives the specified point.  -/
Finset.affineCombination_piSingle : ∀ (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 ι) [inst_3 : DecidableEq ι] (p : ι → P) {i : ι},
  i ∈ s → (Finset.affineCombination k s p) (Pi.single i 1) = p i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.adj_symm : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) {u v : V}, G'.Adj u v → G'.Adj v u
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_insertIdx : ∀ {M : Type u_4} [inst : Monoid M] {l : List M} {a : M} {i : ℕ},
  i ≤ l.length → (∀ a' ∈ List.take i l, Commute a a') → (l.insertIdx i a).prod = a * l.prod
-- Std.Data.DHashMap.Internal.HashesTo
Std.DHashMap.Internal.List.HashesTo.containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] {l : List ((a : α) × β a)}
  {i size : ℕ} (hs : 0 < size),
  Std.DHashMap.Internal.List.HashesTo l i size →
    ∀ (k : α), (↑(Std.DHashMap.Internal.mkIdx size hs (hash k))).toNat ≠ i → Std.Internal.List.containsKey k l = false
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instIsLeftCancelVAddSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd M' α]
  [IsLeftCancelVAdd M' α], IsLeftCancelVAdd (↥s) α
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsParabolic.of_neg : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R}, (-m).IsParabolic → m.IsParabolic
-- Mathlib.Algebra.RingQuot
RingQuot.mk : {R : Type uR} → [inst : Semiring R] → {r : R → R → Prop} → Quot (RingQuot.Rel r) → RingQuot r
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_assoc : ∀ {R : Type u_1} {M : Type u_3} {P : Type u_5} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₃ : Type u_16}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid P]
  [inst_4 : Module R P] [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₃] (f₃ : M₃ →ₗ[R] N₃) (f₁₂ : M →ₗ[R] TensorProduct R M₁ M₂) (f : P →ₗ[R] TensorProduct R M M₃),
  ↑(TensorProduct.assoc R M₁ M₂ N₃) ∘ₗ TensorProduct.map f₁₂ f₃ ∘ₗ f =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f₃) ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ TensorProduct.map f₁₂ LinearMap.id ∘ₗ f
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- A version of `MultilinearMap.cons_smul` for `AlternatingMap`.  -/
AlternatingMap.map_vecCons_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R)
  (x : M), f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_pi : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → Monoid (α i)] {s : (i : ι) → Set (α i)},
  (∀ (i : ι), ThreeGPFree (s i)) → ThreeGPFree (Set.univ.pi s)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.numArgs : Lean.Meta.RecursorInfo → ℕ
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.anyM.match_1.splitter : (motive : Bool → Sort u_1) → (__do_lift : Bool) → (Unit → motive true) → (Unit → motive false) → motive __do_lift
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(∃ ..., ...)⌝` syntax from applications of `SPred.exists`, lifting
nested applications of `spred(...)` from the body.
 -/
Std.Do.SPred.Notation.unexpandExists : Lean.PrettyPrinter.Unexpander
-- Init.Data.Range.Basic
Std.Legacy.Range.mk.injEq : ∀ (start stop step : ℕ) (step_pos : 0 < step) (start_1 stop_1 step_1 : ℕ) (step_pos_1 : 0 < step_1),
  ([start:stop:step] = [start_1:stop_1:step_1]) = (start = start_1 ∧ stop = stop_1 ∧ step = step_1)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.kerLift.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  QuotientAddGroup.kerLift φ = QuotientAddGroup.lift φ.ker φ ⋯
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ),
  g.onBoundedFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
-- Init.Data.SInt.Bitwise
Int64.shiftLeft_xor : ∀ {a b c : Int64}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofNotLT? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift.isLift_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C),
  (CategoryTheory.Quotient.lift.isLift r F H).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Std.Http.Data.Response
Std.Http.Response.Builder.mk : Std.Http.Response.Head → Std.Http.Extensions → Std.Http.Response.Builder
-- Mathlib.Order.Basic
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version auto-generates `min` and `max` fields. It also takes `[Ord α]`
as an argument and uses them for `compare` fields. See `LinearOrder.lift` for a version that
autogenerates `compare` fields, and `LinearOrder.liftWithOrd` for one that doesn't auto-generate
`min` and `max` fields. fields. See note [reducible non-instances].  -/
LinearOrder.liftWithOrd' : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder β] →
      [inst_1 : Ord α] →
        (f : α → β) → Function.Injective f → (∀ (a b : α), compare a b = compare (f a) (f b)) → LinearOrder α
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.union : ∀ {α : Type u_2} {r : α → α → Prop} {s t : Set α},
  s.PartiallyWellOrderedOn r → t.PartiallyWellOrderedOn r → (s ∪ t).PartiallyWellOrderedOn r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Mathlib.RingTheory.Congruence.Hom
/-- The **first isomorphism theorem for rings**.  -/
RingCon.quotientKerEquivRange : {M : Type u_1} →
  {P : Type u_3} → [inst : Ring M] → [inst_1 : Ring P] → (f : M →+* P) → (RingCon.ker f).Quotient ≃+* ↥f.range
-- Init.Data.List.Sublist
List.infix_of_mem_flatten : ∀ {α : Type u_1} {l : List α} {L : List (List α)}, l ∈ L → l <:+: L.flatten
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.omega_zero : ∅ ∈ ZFSet.omega
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Ici : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R},
  Int.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, then any `F`-linearly independent family on `B` remains
linearly independent over `A`.  -/
IntermediateField.LinearDisjoint.linearIndependent_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B → ∀ {ι : Type u_1} {b : ι → ↥B}, LinearIndependent F b → LinearIndependent (↥A) (⇑B.val ∘ b)