mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_4 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.single j, CategoryTheory.Pairwise.Hom.right i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_4 i j
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceTo_le : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos}, String.Slice.Pos.ofSliceTo pos ≤ p₀
-- Init.Data.Array.Lemmas
Array.id_run_foldrM : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → Id β} {b : β} {xs : Array α} {start stop : ℕ},
  (Array.foldrM f b xs start stop).run = Array.foldr (fun x1 x2 => (f x1 x2).run) b xs start stop
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.continuous : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L], Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {k : α},
  m.WF → Std.DHashMap.Raw.Const.insertManyIfNewUnit m [k] = m.insertIfNew k ()
-- Init.Data.Nat.Lemmas
Nat.le_log2 : ∀ {n k : ℕ}, n ≠ 0 → (k ≤ n.log2 ↔ 2 ^ k ≤ n)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_toUSize : ∀ (n : ISize) (h : System.Platform.numBits = 32), n.toUSize.toBitVec32 h = n.toBitVec32 h
-- Lean.Data.Options
Lean.Option.getM : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadOptions m] → [Lean.KVMap.Value α] → Lean.Option α → m α
-- Mathlib.Lean.Meta
/-- Analogue of `liftMetaTactic` for tactics that return a single goal.  -/
Lean.Elab.Tactic.liftMetaTactic' : (Lean.MVarId → Lean.MetaM Lean.MVarId) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_id_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.CategoryStruct.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'_d_eq : ∀ {ι : 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.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hj : ¬e.BoundaryLE j),
  (K.truncLE' e).d i j =
    CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e hi' ⋯).hom
      (CategoryTheory.CategoryStruct.comp (K.d i' j') (K.truncLE'XIso e hj' hj).inv)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.isCoprime_row : ∀ {R : Type v} [inst : CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) (i : Fin 2), IsCoprime (↑A i 0) (↑A i 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Given `p` a polynomial being inserted into `lowers`, `uppers`, or `dvdCnstrs`,
get its leading variable `y`, and adds `y` as an occurrence for the remaining variables in `p`.
 -/
Int.Internal.Linear.Poly.updateOccs : Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivAddCircle_symm_apply_mk : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜),
  (AddCircle.equivAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
-- Init.Data.BitVec.Lemmas
BitVec.toFin_twoPow : ∀ {w i : ℕ}, (BitVec.twoPow w i).toFin = Fin.ofNat (2 ^ w) (2 ^ i)
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_eq_deriv' : ∀ {g : ℝ → ℝ} {u : ℝ}, gradient g u = deriv g u
-- Init.Data.Array.Lemmas
Array.flatten_singleton : ∀ {α : Type u_1} {xs : Array α}, #[xs].flatten = xs
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.inseparable' : ∀ {F : Type u_1} {E : Type u_2} {inst : CommRing F} {inst_1 : Ring E} {inst_2 : Algebra F E}
  [self : IsPurelyInseparable F E] (x : E), IsSeparable F x → x ∈ (algebraMap F E).range
-- Mathlib.RingTheory.Congruence.Hom
/-- Homomorphisms on the quotient of a ring by a ring congruence relation are
equal if they are equal on elements that are coercions from the ring.  -/
RingCon.Quotient.hom_extₐ : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] {c : RingCon M} {f g : c.Quotient →ₐ[R] P},
  f.comp (RingCon.mkₐ R c) = g.comp (RingCon.mkₐ R c) → f = g
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `Dvd.intro_left`. -/
dvd_of_mul_left_eq : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The equivalence between an additive topological group `G` and `Gᵃᵒᵖ` as a uniform
equivalence when `G` is equipped with the left uniformity and `Gᵃᵒᵖ` with the right uniformity.  -/
AddOpposite.opUniformEquivLeft : (G : Type u_2) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalAddGroup G] → G ≃ᵤ Gᵃᵒᵖ
-- Mathlib.Data.Nat.PSub
Nat.ppred_eq_pred : ∀ {n : ℕ}, 0 < n → n.ppred = some n.pred
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `Int32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toInt32 : Float.Model.UnpackedFloat → Int32
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.isZero_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  CategoryTheory.Limits.IsZero (G.X i) →
    (∀ (j : ι), c.Rel i j → CategoryTheory.Limits.IsZero (F.X j)) →
      CategoryTheory.Limits.IsZero (HomologicalComplex.homotopyCofiber.X φ i)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.MemLp.aestronglyMeasurable : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace ε] {f : α → ε} {p : ENNReal},
  MeasureTheory.MemLp f p μ → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.neg_eq : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}
  [NormOneClass 𝕜], Balanced 𝕜 s → -s = s
-- Lean.Declaration
Lean.ConstantInfo.hints : Lean.ConstantInfo → Lean.ReducibilityHints
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ)
  (X_1 : SimplexCategoryᵒᵖ),
  ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearIndepOn_id : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → LinearIndepOn R id (Set.range v)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_div : ∀ {a b : ISize} (h : System.Platform.numBits = 32), (a / b).toBitVec32 h = (a.toBitVec32 h).sdiv (b.toBitVec32 h)
-- Mathlib.RepresentationTheory.Basic
Representation.asAlgebraHom_ofMulAction_smul_eq_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] (x y : MonoidAlgebra k G),
  ((Representation.ofMulAction k G G).asAlgebraHom x) y = x * y
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.pushUnusedSimpArgsInfo : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.Syntax → Array Bool → m Unit
-- Mathlib.FieldTheory.KummerPolynomial
X_pow_sub_C_irreducible_iff_of_prime : ∀ {K : Type u} [inst : Field K] {p : ℕ},
  Nat.Prime p → ∀ {a : K}, Irreducible (Polynomial.X ^ p - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj { len := 0 }))
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive semigroup, if it admits an
injective map that preserves `+` to an additive semigroup.  -/
Function.Injective.addSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : AddSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddSemigroup M₁
-- Mathlib.Topology.WithTopology
WithTopology.toTopology_ofTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (x : WithTopology X t), WithTopology.toTopology t x.ofTopology = x
-- Std.Time.Zoned.Database.TZdb
/-- Static fallback paths to directories containing time zone files. `TZDIR` is not stored here;
it is re-read on every lookup via `resolveZonesPaths`.
 -/
Std.Time.Database.TZdb.zonesPaths : Std.Time.Database.TZdb → Array System.FilePath
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_le_left : ∀ {n m : ℕ}, n &&& m ≤ n
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The 0-dimensional generalized loops based at `x` are in bijection with `X`.  -/
genLoopHomeoOfIsEmpty : {X : Type u_2} → [inst : TopologicalSpace X] → (N : Type u_3) → (x : X) → [IsEmpty N] → ↑(GenLoop N X x) ≃ₜ X
-- Init.Data.Vector.Find
Vector.find?_some : ∀ {α : Type} {n : ℕ} {p : α → Bool} {a : α} {xs : Vector α n}, Vector.find? p xs = some a → p a = true
-- Mathlib.Data.List.Chain
List.isChain_append_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {b c : α} {l₁ l₂ : List α},
  List.IsChain R (l₁ ++ b :: c :: l₂) ↔ List.IsChain R (l₁ ++ [b]) ∧ R b c ∧ List.IsChain R (c :: l₂)
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_left_of_le' : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ᶠ (x : α) in l, C ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Order.Monotone.Union
/-- If `f` is monotone both on `(-∞, a]` and `[a, ∞)`, then it is monotone on the whole line.  -/
MonotoneOn.Iic_union_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
  MonotoneOn f (Set.Iic a) → MonotoneOn f (Set.Ici a) → Monotone f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.HashMap.ofList l).getKey? k' = some k
-- Mathlib.Combinatorics.SimpleGraph.Girth
/-- The extended girth of a simple graph is the length of its smallest cycle, or `∞` if the graph is
acyclic.
 -/
SimpleGraph.egirth : {α : Type u_1} → SimpleGraph α → ℕ∞
-- Init.Data.Int.Order
Int.nonneg_or_nonneg_neg : ∀ (a : ℤ), a.NonNeg ∨ (-a).NonNeg
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimageImageComparison.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.Abelian.coimageImageComparison f =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f)
      (CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) f ⋯) ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- Power series expansion of `log(1 + x) - log(1 - x)` for `|x| < 1`.  -/
Real.hasSum_log_sub_log_of_abs_lt_one : ∀ {x : ℝ}, |x| < 1 → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (Real.log (1 + x) - Real.log (1 - x))
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.left_inv : ∀ {R : Type u_5} [inst : CommSemiring R] {A : Type u_6} {B : Type u_7} [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (self : A ≃ₗc[R] B), Function.LeftInverse self.invFun self.toFun
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategoryStruct C
-- Mathlib.Algebra.Quandle
Rack.op_act_op_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R},
  Shelf.act (MulOpposite.op x) (MulOpposite.op y) = MulOpposite.op (Rack.invAct x y)
-- Mathlib.Algebra.Group.Defs
add_neg_cancel_comm : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = b
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fifth cosimplicial identity  -/
CategoryTheory.CosimplicialObject.σ_comp_σ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i j : Fin (n + 1)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) (X.σ j) =
      CategoryTheory.CategoryStruct.comp (X.σ j.succ) (X.σ i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.eq_append_of_dropSuffix?_prop_eq_some : ∀ {P : Char → Prop} [inst : DecidablePred P] {s res : String.Slice},
  s.dropSuffix? P = some res → ∃ c, s.copy = res.copy ++ String.singleton c ∧ P c
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} [inst_5 : SizeOf C] [inst_6 : SizeOf J]
  [inst_7 : (a : J) → SizeOf (α a)] (j : J) (hj : ¬IsMax j) (k : (c.attachCells j hj).ι),
  sizeOf { j := j, hj := hj, k := k } = 1 + sizeOf j + sizeOf k
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_lift : ∀ (a : Ordinal.{u}), Ordinal.lift.{w, max v u} (Ordinal.lift.{v, u} a) = Ordinal.lift.{max v w, u} a
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_comp_single : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (i : n),
  CoalgebraStruct.comul ∘ₗ LinearMap.single R A i =
    TensorProduct.map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ CoalgebraStruct.comul
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g h : X ⟶ Y} (α : f ⟶ g) (β : g ⟶ h),
  CategoryTheory.CategoryStruct.comp α β =
    CategoryTheory.CatEnrichedOrdinary.Hom.mk
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.Hom.base α)
        (CategoryTheory.CatEnrichedOrdinary.Hom.base β))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.productUniqueIso_inv_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) =
    CategoryTheory.eqToHom ⋯
-- Batteries.Data.Vector.Lemmas
Vector.back?_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as).back? = some (Vector.foldl f init as)
-- Mathlib.Order.Category.Semilat
SemilatSupCat.isSemilatticeSup : (self : SemilatSupCat) → SemilatticeSup self.X
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- the normalized `gramSchmidt` (i.e each vector in `gramSchmidtNormed` has unit length.)  -/
InnerProductSpace.gramSchmidtNormed : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [InnerProductSpace 𝕜 E] →
          {ι : Type u_3} → [inst : LinearOrder ι] → [LocallyFiniteOrderBot ι] → [WellFoundedLT ι] → (ι → E) → ι → E
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput.invert.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput)
  (linv rinv : Bool), input.invert linv rinv = { lhs := input.lhs.flip linv, rhs := input.rhs.flip rinv }
-- Mathlib.Data.ZMod.Defs
/-- Commutative ring structure on `Fin n`.

This is not a global instance, but can introduced locally using `open Fin.CommRing in ...`.

This is not an instance because the `binop%` elaborator assumes that
there are no non-trivial coercion loops,
but this instance would introduce a coercion from `Nat` to `Fin n` and back.
Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.

For example, for `x : Fin k` and `n : Nat`,
it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
silently introducing wraparound arithmetic.
 -/
Fin.instCommRing : (n : ℕ) → [NeZero n] → CommRing (Fin n)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom_comp : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f)
      (CategoryTheory.FreeBicategory.liftHom F g)
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupComap_surjective_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H' : AddSubgroup G'),
  Function.Surjective ⇑f → Function.Surjective ⇑(f.addSubgroupComap H')
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that for every cell of the subcomplex the corresponding closed cell is a subset of `E`.  -/
Topology.RelCWComplex.Subcomplex.mk' : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) →
        {D : Set X} →
          [inst : Topology.RelCWComplex C D] →
            (E : Set X) →
              (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) →
                (∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) →
                  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_mul_X_sub_C_pow : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {a : R} {n : ℕ},
  p ≠ 0 → Polynomial.rootMultiplicity a (p * (Polynomial.X - Polynomial.C a) ^ n) = Polynomial.rootMultiplicity a p + n
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
HomotopyCategory.instAdditiveIntUpSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ), (HomotopyCategory.singleFunctor C n).Additive
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.getRepr.match_1.eq_1 : ∀ {n : ℕ} (motive : Option (Fin n) → Sort u_1) (y : Fin n) (h_1 : (y_1 : Fin n) → some y = some y_1 → motive (some y_1))
  (h_2 : some y = none → motive none),
  (match h : some y with
    | some y_1 => h_1 y_1 h
    | none => h_2 h) =
    h_1 y ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- The subcategory `D` of `C` expressed as an inclusion functor is an *exponential ideal* if
`B ∈ D` implies `A ⟹ B ∈ D` for all `A`.
 -/
CategoryTheory.ExponentialIdeal : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        CategoryTheory.Functor D C →
          [inst_2 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.MonoidalClosed C] → Prop
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).hom = CategoryTheory.inv (F.mapComp f g)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.posDef_of_nonneg : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {Q : QuadraticMap R₂ M N},
  (∀ (x : M), 0 ≤ Q x) → Q.Anisotropic → Q.PosDef
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).getD k fallback = fallback
-- Init.Data.Nat.Basic
/-- Alias for `Nat.lt_asymm`.  -/
Nat.not_lt_of_lt : ∀ {a b : ℕ}, a < b → ¬b < a
-- Mathlib.CategoryTheory.Opposites
/-- The equivalence of functor categories induced by `op` and `unop`.
 -/
CategoryTheory.Functor.opUnopEquiv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.Functor C D)ᵒᵖ ≌ CategoryTheory.Functor Cᵒᵖ Dᵒᵖ
-- Mathlib.Data.Setoid.Basic
Setoid.prodQuotientEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) (q : Quotient (r.prod s)),
  (r.prodQuotientEquiv s).symm q = q.liftOn' (fun xy => (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯