mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Determinant
LinearMap.coe_equivOfIsUnitDet : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] {f : M →ₗ[R] M} (h : IsUnit (LinearMap.det f)),
  ↑(LinearMap.equivOfIsUnitDet h) = f
-- Mathlib.CategoryTheory.Types.Basic
/-- The functor embedding `Type u` into `Type (max u v)`.
Write this as `uliftFunctor.{5, 2}` to get `Type 2 ⥤ Type 5`.
 -/
CategoryTheory.uliftFunctor : CategoryTheory.Functor (Type u) (Type (max u v))
-- Std.Http.Data.URI.Basic
Std.Http.URI.Query.instEmptyCollection : EmptyCollection Std.Http.URI.Query
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.chosenEnd_def : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))},
  CategoryTheory.Limits.chosenEnd F = CategoryTheory.Limits.Types.end_ F
-- Mathlib.Logic.Function.Basic
/-- Composition by a surjective function on the left is itself surjective.  -/
Function.Surjective.comp_left : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ}, Function.Surjective g → Function.Surjective fun x => g ∘ x
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The standard resolution of `k` as a trivial representation as a complex of `k`-modules.  -/
Rep.standardComplex.forget₂ToModuleCat : (k G : Type u) → [inst : CommRing k] → [Monoid G] → HomologicalComplex (ModuleCat k) (ComplexShape.down ℕ)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instInhabitedStrictOrLazy : {a : Type} → [Inhabited a] → {a_1 : Type} → Inhabited (Lean.Widget.StrictOrLazy a a_1)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
_private.Mathlib.Analysis.BoxIntegral.Partition.Additive.0.Option.elim'.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_entryAtIdx? : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {i : ℕ} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.entryAtIdxD t i fallback =
    (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t i).getD fallback
-- Init.Data.SInt.Lemmas
Int64.le_minValue_iff : ∀ {a : Int64}, a ≤ Int64.minValue ↔ a = Int64.minValue
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.instInner : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → Inner 𝕜 (TensorProduct 𝕜 E F)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_union₀`. -/
MeasureTheory.integral_union_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      MeasureTheory.IntegrableOn f s μ →
        MeasureTheory.IntegrableOn f t μ → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
-- Init.Data.List.Lemmas
List.headD.eq_2 : ∀ {α : Type u} (x a : α) (as : List α), (a :: as).headD x = a
-- Mathlib.Data.Set.Lattice
Set.biUnion_union : ∀ {α : Type u_1} {β : Type u_2} (s t : Set α) (u : α → Set β), ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x
-- Mathlib.Tactic.Choose
/-- Given `α : Sort u`, `nonemp : Nonempty α`, `p : α → Prop`, a context of free variables
`ctx`, and a pair of an element `val : α` and `spec : p val`,
`mkSometimes u α nonemp p ctx (val, spec)` produces another pair `val', spec'`
such that `val'` does not have any free variables from elements of `ctx` whose types are
propositions. This is done by applying `Function.sometimes` to abstract over all the propositional
arguments.  -/
Mathlib.Tactic.Choose.mkSometimes : Lean.Level →
  Lean.Expr → Lean.Expr → Lean.Expr → List Lean.Expr → Lean.Expr × Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.mk : ℕ → Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.State✝
-- Lean.CoreM
Lean.DeclNameGenerator.mk.inj : ∀ {namePrefix : Lean.Name} {idx : ℕ} {parentIdxs : List ℕ} {namePrefix_1 : Lean.Name} {idx_1 : ℕ}
  {parentIdxs_1 : List ℕ},
  { namePrefix := namePrefix, idx := idx, parentIdxs := parentIdxs } =
      { namePrefix := namePrefix_1, idx := idx_1, parentIdxs := parentIdxs_1 } →
    namePrefix = namePrefix_1 ∧ idx = idx_1 ∧ parentIdxs = parentIdxs_1
-- Init.Prelude
Nat.le.below.refl : ∀ {n : ℕ} {motive : (a : ℕ) → n.le a → Prop}, Nat.le.below ⋯
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.toPointedCone_bot : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : T1Space E], ↑⊥ = ⊥
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Provide default replacement (`String`) for a disallowed character, or `none` if none defined  -/
Mathlib.Linter.TextBased.UnicodeLinter.replaceDisallowed : Char → Option String
-- Mathlib.Algebra.Group.Hom.Basic
invMonoidHom.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α], invMonoidHom = { toFun := Inv.inv, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `DecidableEq` across an equivalence.  -/
Equiv.decidableEq : {α : Sort u} → {β : Sort v} → α ≃ β → [DecidableEq β] → DecidableEq α
-- Lean.Parser.Command
Lean.Parser.Command.namespace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.RelIso.Basic
RelIso.apply_eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {x y : α}, f x = f y ↔ x = y
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.instCoalgebra : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) →
      [inst_1 : Semiring A] → (X : Type u_3) → [inst_2 : Module R A] → [Coalgebra R A] → Coalgebra R (MonoidAlgebra A X)
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A Hilbert basis of is an unconditional Schauder basis (`UnconditionalSchauderBasis`),
with coordinate functionals `x ↦ ⟪b i, x⟫`. The basis expansion `x = ∑' i, ⟪b i, x⟫ • b i`
converges unconditionally.  -/
HilbertBasis.toUnconditionalSchauderBasis : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → HilbertBasis ι 𝕜 E → UnconditionalSchauderBasis ι 𝕜 E
-- Mathlib.Analysis.RCLike.Basic
RCLike.instPosMulReflectLE : ∀ {K : Type u_1} [inst : RCLike K], PosMulReflectLE K
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.exists_eq_add_of_deriv_eq : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {s : Set 𝕜}
  {f g : 𝕜 → G},
  IsOpen s →
    IsPreconnected s →
      DifferentiableOn 𝕜 f s →
        DifferentiableOn 𝕜 g s → Set.EqOn (deriv f) (deriv g) s → ∃ a, Set.EqOn f (fun x => g x + a) s
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.RingCat.Hom.mk : {R S : RingCat} → (↑R →+* ↑S) → R.Hom S
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_equiv_eq_comap_symm : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (f : R ≃+* S)
  (K : NonUnitalSubsemiring R), NonUnitalSubsemiring.map (↑f) K = NonUnitalSubsemiring.comap f.symm K
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n ≠ 0 → (p.trailingDegree = ↑n ↔ p.natTrailingDegree = n)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.topology_eq_upperSetTopology : ∀ {α : Type u_4} {t : TopologicalSpace α} {inst : Preorder α} [self : Topology.IsUpperSet α], t = Topology.upperSet α
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.inner_nonneg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ inner 𝕜 x (T x)
-- Init.Data.Vector.Basic
/-- The last element of a vector, or `none` if the vector is empty.  -/
Vector.back? : {α : Type u_1} → {n : ℕ} → Vector α n → Option α
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaCongrRight_trans : ∀ {α : Type u_4} {β₁ : α → Type u_1} {β₂ : α → Type u_2} {β₃ : α → Type u_3} (F : (a : α) → β₁ a ≃ β₂ a)
  (G : (a : α) → β₂ a ≃ β₃ a),
  (Equiv.sigmaCongrRight F).trans (Equiv.sigmaCongrRight G) = Equiv.sigmaCongrRight fun a => (F a).trans (G a)
-- Init.Data.Vector.Basic
instReprVector : {α : Type u_1} → {n : ℕ} → [Repr α] → Repr (Vector α n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∈ t₂ → (t₁ \ t₂)[k]! = default
-- Init.Data.Int.DivMod.Lemmas
Int.le_emod_self_add_one_iff : ∀ {a b : ℤ}, 0 < b → (b ≤ a % b + 1 ↔ b ∣ a + 1)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Q : C},
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.instIsLowerSet : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsLowerSet α
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The free/forgetful adjunction between `PointedToBipointed_snd` and `BipointedToPointed_snd`.
 -/
pointedToBipointedSndBipointedToPointedSndAdjunction : pointedToBipointedSnd ⊣ bipointedToPointedSnd
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instDiv : {K : Type u} → [inst : CommRing K] → [IsDomain K] → Div (RatFunc K)
-- Mathlib.Order.Lattice.Nat
Nat.iSup_le_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.cofibration_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.Cofibration f ↔ HomotopicalAlgebra.cofibrations C f
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- The inclusion of `P.fullsubcategory` in `F`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.ι : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) → [inst_1 : P.IsClosedUnderMapObj] → P.fullsubcategory.StrongTrans F
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_fun_curry : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : One M] (f : ι × κ → M),
  (Function.mulSupport fun i j => f (i, j)) = Prod.fst '' Function.mulSupport f
-- Lean.Exception
Lean.MonadRecDepth.getRecDepth : {m : Type → Type} → [self : Lean.MonadRecDepth m] → m ℕ
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_sum_of_subadditive_on_pred : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop),
  f 0 ≤ 0 →
    p 0 →
      (∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) →
        (∀ (a b : α), p a → p b → p (a + b)) → ∀ (l : List α), (∀ a ∈ l, p a) → f l.sum ≤ (List.map f l).sum
-- Init.Data.Array.Lemmas
Array.exists_mem_empty : ∀ {α : Type u_1} (p : α → Prop), ¬∃ x, ∃ (_ : x ∈ #[]), p x
-- Mathlib.Logic.Unique
/-- If `α` is inhabited and admits an injective map to a subsingleton type, then `α` is `Unique`.  -/
Function.Injective.unique : {α : Sort u_1} → {β : Sort u_2} → {f : α → β} → [Inhabited α] → [Subsingleton β] → Function.Injective f → Unique α
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_smul_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {r : 𝕜}, inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y
-- Lean.Data.Lsp.Internal
Lean.Lsp.DeclInfo.mk : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Lean.Lsp.DeclInfo
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H ≤ AddSubgroup.normalClosure ↑H
-- Mathlib.Order.KrullDimension
Order.exists_series_of_le_coheight : ∀ {α : Type u_1} [inst : Preorder α] (a : α) {n : ℕ}, ↑n ≤ Order.coheight a → ∃ p, RelSeries.head p = a ∧ p.length = n
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g h i : a ⟶ b} {j : b ⟶ c} {α : f ≅ g} {η : g ⟶ h}
  {ηs : h ⟶ i} {ηs₁ : CategoryTheory.CategoryStruct.comp h j ⟶ CategoryTheory.CategoryStruct.comp i j}
  {η₁ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp h j}
  {η₂ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp i j}
  {η₃ : CategoryTheory.CategoryStruct.comp f j ⟶ CategoryTheory.CategoryStruct.comp i j},
  CategoryTheory.Bicategory.whiskerRight ηs j = ηs₁ →
    CategoryTheory.Bicategory.whiskerRight η j = η₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α j).hom η₂ = η₃ →
          CategoryTheory.Bicategory.whiskerRight
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) j =
            η₃
-- Mathlib.Probability.Martingale.Convergence
/-- A realization of a stochastic process with bounded upcrossings and bounded limit inferiors is
convergent.

We use the spelling `< ∞` instead of the standard `≠ ∞` in the assumptions since it is not as easy
to change `<` to `≠` under binders.  -/
MeasureTheory.tendsto_of_uncrossing_lt_top : ∀ {Ω : Type u_1} {f : ℕ → Ω → ℝ} {ω : Ω},
  Filter.liminf (fun n => ↑‖f n ω‖₊) Filter.atTop < ⊤ →
    (∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤) →
      ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Mathlib.Algebra.Group.Opposite
AddCommute.op : ∀ {α : Type u_1} [inst : Add α] {x y : α}, AddCommute x y → AddCommute (AddOpposite.op x) (AddOpposite.op y)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.natDegree_pow_X_add_C : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ) (r : R), ((Polynomial.X + Polynomial.C r) ^ n).natDegree = n
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.isEmpty : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → (s.isEmpty = true ↔ m = [])
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_1.eq_2 : ∀ {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ Id β₁] {it₁ : Std.Iter β₁} (motive : it₁.Step → Sort u_2)
  (it₁' : Std.Iter β₁) (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.Iter β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.Iter β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.skip it₁', hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_2 it₁' hp
-- Mathlib.Data.Num.Lemmas
Num.toZNum_inj : ∀ {m n : Num}, m.toZNum = n.toZNum ↔ m = n
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLT : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.lt) → (a : α) × β a
-- Mathlib.Data.PFun
PFun.prodMap_id_id : ∀ {α : Type u_1} {β : Type u_2}, (PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)
-- Init.Data.Fin.Fold
Fin.foldr_congr : ∀ {α : Sort u_1} {n k : ℕ} (w : n = k) (f : Fin n → α → α), Fin.foldr n f = Fin.foldr k fun i => f (Fin.cast ⋯ i)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- A Lie group is a topological group. This is not an instance for technical reasons,
see note [Design choices about smooth algebraic structures].  -/
topologicalGroup_of_lieGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I n G],
  IsTopologicalGroup G
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a product.

The difference with `Finset.prod_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.prod_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the products, rather than being non-dependent functions.  -/
Finset.prod_bij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
  (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s),
  (∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) →
    (∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) →
      (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → ∏ x ∈ s, f x = ∏ x ∈ t, g x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A trident `t` on the parallel family `f : J → (X ⟶ Y)` consists of two morphisms
`t.π.app zero : t.X ⟶ X` and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is
interesting, and we give it the shorter name `Trident.ι t`.  -/
CategoryTheory.Limits.Trident.ι : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          (t : CategoryTheory.Limits.Trident f) →
            ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj
                CategoryTheory.Limits.WalkingParallelFamily.zero ⟶
              (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ) {Z : C}
  (h :
    s.N (Opposite.unop (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })).fst).len ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (CategoryTheory.CategoryStruct.comp
        (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))) h) =
    CategoryTheory.CategoryStruct.comp
      (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))) h
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : α ⊕ List (Computation α) → Sort u_2) (o : α ⊕ List (Computation α))
  (h_1 : (a : α) → motive (Sum.inl a)) (h_2 : (ls : List (Computation α)) → motive (Sum.inr ls))
  (ls : List (Computation α)),
  o = Sum.inr ls →
    (match o with
      | Sum.inl a => h_1 a
      | Sum.inr ls => h_2 ls) ≍
      h_2 ls
-- Mathlib.Topology.MetricSpace.Thickening
Metric.diam_cthickening_le : ∀ {ε : ℝ} {α : Type u_2} [inst : PseudoMetricSpace α] (s : Set α),
  0 ≤ ε → Metric.diam (Metric.cthickening ε s) ≤ Metric.diam s + 2 * ε
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose),
  𝒰.finiteSubcover.X x = 𝒰.X (AlgebraicGeometry.Scheme.Cover.idx 𝒰 ↑x)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.lift_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (P : Type u_7)
  [inst_7 : NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i),
  (DirectLimit.NonUnitalRing.lift G f P g Hg) ((DirectLimit.NonUnitalRing.of G f i) x) = (g i) x
-- Mathlib.Data.Multiset.Count
Multiset.countP_congr : ∀ {α : Type u_1} {s s' : Multiset α},
  s = s' →
    ∀ {p p' : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred p'],
      (∀ x ∈ s, p x = p' x) → Multiset.countP p s = Multiset.countP p' s'
-- Init.Data.Float.Float32
instToStringFloat32 : ToString Float32
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (j : CategoryTheory.Discrete α),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).cone.π.app j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F)
        (Opposite.op {j}))
      (CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨j, ⋯⟩)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig len → aig.RefVec len
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.image_iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α},
  Function.IsFixedPt (Set.image f) s → ∀ (n : ℕ), Function.IsFixedPt (Set.image f^[n]) s
-- Mathlib.Data.Set.Pairwise.Lattice
Set.coe_snd_biUnionEqSigmaOfDisjoint : ∀ {α : Type u_5} {ι : Type u_6} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) (x : ↑(⋃ i ∈ s, f i)),
  ↑((Set.biUnionEqSigmaOfDisjoint h) x).snd = ↑x
-- Mathlib.NumberTheory.AlmostPrime
Nat.IsAtMostAlmostPrime.mul : ∀ {k l m n : ℕ}, k.IsAtMostAlmostPrime m → l.IsAtMostAlmostPrime n → (k + l).IsAtMostAlmostPrime (m * n)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : τ →₀ ℕ} (c : R),
  ↑s.support ⊆ Set.range f →
    (MvPolynomial.killCompl hf) ((MvPolynomial.monomial s) c) = (MvPolynomial.monomial (Finsupp.comapDomain f s ⋯)) c