mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLattice.Basic
iSup_image2 : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β)
  (t : Set γ) (g : δ → α), ⨆ d ∈ Set.image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.data_take : ∀ {s : Substring.Raw}, s.Valid → ∀ (n : ℕ), (s.take n).toString.toList = List.take n s.toString.toList
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.ext_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] {f g : H}, f = g ↔ ∀ (x : X), f x = g x
-- Batteries.Recycling.RBTree.Basic
/-- Returns `true` iff any element of the tree satisfies `p`.  -/
RBTree.RBNode.any : {α : Type u_1} → (α → Bool) → RBTree.RBNode α → Bool
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousOn_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {z : β},
  UpperSemicontinuousOn (fun _x => z) s
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_mul_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G]
  (x y : AddMonoidAlgebra k G), (x * y).coeff.support ⊆ x.coeff.support + y.coeff.support
-- Mathlib.Topology.Spectral.ConstructibleTopology
constructibleTopologySubbasis.eq_1 : ∀ (X : Type u_2) [inst : TopologicalSpace X],
  constructibleTopologySubbasis X = {s | IsOpen s ∧ IsCompact s} ∪ {s | IsClosed s ∧ IsCompact sᶜ}
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.toAddSubsemigroup_closure : ∀ {M : Type u_1} [inst : Mul M] (S : Set M),
  Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Additive.toMul ⁻¹' S)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.pow_def : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Pow β M] (n : M) (x : α), x ^ n = e.symm (e x ^ n)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.Quasicategory₂.fill31 : ∀ {X : SSet.Truncated 2} [self : X.Quasicategory₂]
  {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₂₃ : SSet.Truncated.Edge x₂ x₃}
  {e₀₂ : SSet.Truncated.Edge x₀ x₂} {e₁₃ : SSet.Truncated.Edge x₁ x₃} {e₀₃ : SSet.Truncated.Edge x₀ x₃}
  (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃),
  Nonempty (e₀₂.CompStruct e₂₃ e₀₃)
-- Lean.Parser.Command
Lean.Parser.Command.openScoped.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Find
Array.findFinIdx?_append : ∀ {α : Type u_1} {xs ys : Array α} {p : α → Bool},
  Array.findFinIdx? p (xs ++ ys) =
    (Option.map (Fin.castLE ⋯) (Array.findFinIdx? p xs)).or
      (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.size) (Array.findFinIdx? p ys)))
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.ext : ∀ {x y : Std.Http.Header.Name}, x.value = y.value → x = y
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ‖f‖ = (MeasureTheory.eLpNorm (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ).toReal
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- Let $L$ be the graph Laplacian and let $x \in \mathbb{R}$, then
$$x^{\top} L x = \sum_{i \sim j} (x_{i}-x_{j})^{2}$$,
where $\sim$ denotes the adjacency relation  -/
SimpleGraph.lapMatrix_toLinearMap₂' : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : Field R] [CharZero R] (x : V → R),
  (((Matrix.toLinearMap₂' R) (SimpleGraph.lapMatrix R G)) x) x =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
-- Mathlib.Algebra.Group.End
Equiv.permCongrHom_coe_equiv : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β), ↑e.permCongrHom = e.permCongr
-- Mathlib.Data.List.Forall2
List.left_unique_forall₂' : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.LeftUnique R → ∀ {a b : List α} {c : List β}, List.Forall₂ R a c → List.Forall₂ R b c → a = b
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.derivative_succ_aux : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from an `AddMonoid` to its quotient by a congruence
relation is surjective.  -/
AddCon.mk'_surjective : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M}, Function.Surjective ⇑c.mk'
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instAlgebra_1 : {K : Type v} → [inst : Field K] → (f : Polynomial K) → Algebra K f.SplittingField
-- Mathlib.MeasureTheory.Covering.OneDim
Real.tendsto_Icc_vitaliFamily_right : ∀ (x : ℝ),
  Filter.Tendsto (fun y => Set.Icc x y) (nhdsWithin x (Set.Ioi x))
    ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.instReprSign : Repr Float.Model.UnpackedFloat.Sign
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (h : k ∈ m), (m.getKey k h == k) = true
-- Init.Prelude
/-- Retrieves the local value whose type is `ρ`.  This is useful when a monad supports reading more than
one type of value.

Use `read` for a version that expects the type `ρ` to be inferred from `m`.
 -/
readThe : (ρ : Type u) → {m : Type u → Type v} → [MonadReaderOf ρ m] → m ρ
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- Let `M` and `M'` be manifolds with the same model-with-corners, `I`.  Then `f : M → M'`
is a local structomorphism for `I`, if and only if it is manifold-`C^n` on the domain of definition
in both directions.  -/
isLocalStructomorphOn_contDiffGroupoid_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_5}
  [inst_6 : TopologicalSpace M'] [IsManifold I n M] [inst_8 : ChartedSpace H M'] [IsM' : IsManifold I n M']
  (f : OpenPartialHomeomorph M M'),
  ChartedSpace.LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source ↔
    ContMDiffOn I I n (↑f) f.source ∧ ContMDiffOn I I n (↑f.symm) f.target
-- Init.Data.Vector.Lemmas
/-- Variant of `all_eq` in terms of membership rather than an array index.  -/
Vector.all_eq' : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, xs.all p = decide (∀ x ∈ xs, p x = true)
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `AddCommGrpCat.{u}`
to `AddCommMonCat.{u}` preserves limits of shape `J`.  -/
AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_map_snd : ∀ (X Y : SSet) {m n : SimplexCategoryᵒᵖ} (f : m ⟶ n) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj m),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) z).2 =
    (CategoryTheory.ConcreteCategory.hom (Y.map f)) z.2
-- Init.Data.Array.Lemmas
Array.all_empty : ∀ {α : Type u_1} [BEq α] {p : α → Bool}, #[].all p = true
-- Init.Data.SInt.Lemmas
ISize.ofInt_int8ToInt : ∀ (x : Int8), ISize.ofInt x.toInt = x.toISize
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] (t : Set ((i : ι) → α i)),
  t ∈ MeasureTheory.measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = MeasureTheory.cylinder s S
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.mul_one : {R : Type u} → [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (a.mul Rack.PreEnvelGroup.unit) a
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.sin : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.sin (f x)
-- Mathlib.CategoryTheory.Category.Basic
/-- A morphism `f` is an epimorphism if it can be cancelled when precomposed:
`f ≫ g = f ≫ h` implies `g = h`. 

[Stacks Tag 003B](https://stacks.math.columbia.edu/tag/003B) -/
CategoryTheory.Epi : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.Order.Monotone.Basic
strictAntiOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid_default : default.Valid
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
  I.ideal V ≤ Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (I.ideal U)
-- Mathlib.Condensed.Light.Explicit
LightCondensed.ofSheafForgetLightProfinite_obj : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {FA : A → A → Type u_2} {CA : A → Type u_3}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [inst_3 : CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)]
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ A)
  [inst_4 : CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))]
  (hF : CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A))),
  (LightCondensed.ofSheafForgetLightProfinite F hF).obj = F
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).H = h.H
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- Big pro-étale site: the pro-étale precoverage on the category of schemes given
by fpqc covers of weakly étale morphisms.
[Definition 4.1.1][proetale2015]
 -/
AlgebraicGeometry.Scheme.proetalePrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.FGModuleCatCoevaluation_apply_one : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K),
  (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatCoevaluation K V).hom) 1 =
    ∑ i, (Module.Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K ↑V).coord i
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_of_le_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ (x : S.obj (Opposite.op { len := n + 1 })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.castSucc))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j.succ)) x) =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i)) x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Real.sin_eq_tsum : ∀ (r : ℝ), Real.sin r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial
-- Mathlib.Tactic.WLOG
Mathlib.Tactic.WLOGResult.mk.inj : ∀ {reductionGoal : Lean.MVarId} {reductionFVarIds : Lean.FVarId × Lean.FVarId} {hypothesisGoal : Lean.MVarId}
  {hypothesisFVarId : Lean.FVarId} {revertedFVarIds : Array Lean.FVarId} {reductionGoal_1 : Lean.MVarId}
  {reductionFVarIds_1 : Lean.FVarId × Lean.FVarId} {hypothesisGoal_1 : Lean.MVarId} {hypothesisFVarId_1 : Lean.FVarId}
  {revertedFVarIds_1 : Array Lean.FVarId},
  { reductionGoal := reductionGoal, reductionFVarIds := reductionFVarIds, hypothesisGoal := hypothesisGoal,
        hypothesisFVarId := hypothesisFVarId, revertedFVarIds := revertedFVarIds } =
      { reductionGoal := reductionGoal_1, reductionFVarIds := reductionFVarIds_1, hypothesisGoal := hypothesisGoal_1,
        hypothesisFVarId := hypothesisFVarId_1, revertedFVarIds := revertedFVarIds_1 } →
    reductionGoal = reductionGoal_1 ∧
      reductionFVarIds = reductionFVarIds_1 ∧
        hypothesisGoal = hypothesisGoal_1 ∧ hypothesisFVarId = hypothesisFVarId_1 ∧ revertedFVarIds = revertedFVarIds_1
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyIrreducibleOfGeometricallyIntegral : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.GeometricallyIrreducible f
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Algebra.adjoin.powerBasis'_dim : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), (Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix).  -/
Matrix.mem_range_scalar_of_commute_transvectionStruct : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n] {M : Matrix n n R},
  (∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M) → M ∈ Set.range ⇑(Matrix.scalar n)
-- Init.Try
/-- Configuration for `try?`.
 -/
Lean.Try.Config : Type
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.Quotient.torsionBy_eq_span_singleton : ∀ {R : Type w} [inst : CommRing R] (a b : R),
  a ∈ nonZeroDivisors R → Submodule.torsionBy R (R ⧸ R ∙ a * b) a = R ∙ (Ideal.Quotient.mk (R ∙ a * b)) b
-- Init.Data.List.Lemmas
List.foldr_append : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {l l' : List α},
  List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_1.eq_3 : ∀ (motive : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Sort u_1) (k₁ : ℕ) (v₁ : Nat.Internal.Linear.Var)
  (m₁ : List (ℕ × Nat.Internal.Linear.Var)) (k₂ : ℕ) (v₂ : Nat.Internal.Linear.Var)
  (m₂ : List (ℕ × Nat.Internal.Linear.Var)) (h_1 : (m₁ : Nat.Internal.Linear.Poly) → motive m₁ [])
  (h_2 : (m₂ : Nat.Internal.Linear.Poly) → motive [] m₂)
  (h_3 :
    (k₁ : ℕ) →
      (v₁ : Nat.Internal.Linear.Var) →
        (m₁ : List (ℕ × Nat.Internal.Linear.Var)) →
          (k₂ : ℕ) →
            (v₂ : Nat.Internal.Linear.Var) →
              (m₂ : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k₁, v₁) :: m₁) ((k₂, v₂) :: m₂)),
  (match (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ with
    | m₁, [] => h_1 m₁
    | [], m₂ => h_2 m₂
    | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ => h_3 k₁ v₁ m₁ k₂ v₂ m₂) =
    h_3 k₁ v₁ m₁ k₂ v₂ m₂
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_ofWithBot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))}
  {le_of_mem : ∀ J ∈ boxes, J ≤ ↑I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint},
  (∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') → π ≤ BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.instNonempty : ∀ {L : FirstOrder.Language} (T : L.Theory) (M : T.ModelType), Nonempty ↑M
-- Mathlib.Analysis.Complex.ReImTopology
/-- `Complex.im` turns `ℂ` into a trivial topological fiber bundle over `ℝ`.  -/
Complex.isHomeomorphicTrivialFiberBundle_im : IsHomeomorphicTrivialFiberBundle ℝ Complex.im
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_unitIso_inv_app_hom_toFun : ∀ (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X),
  (TwoP.swapEquiv.unitIso.inv.app X).hom.toFun a = a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {motive : (Std.ExtDHashMap α fun x => β) → Prop}
  (m : Std.ExtDHashMap α fun x => β) (l : ρ),
  motive m →
    (∀ (m : Std.ExtDHashMap α fun x => β) (a : α) (b : β), motive m → motive (m.insert a b)) →
      motive (Std.ExtDHashMap.Const.insertMany m l)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
      (S₂.mapRightHomologyIso F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom
      (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
-- Mathlib.Analysis.BoundedVariation
/-- A bounded variation function into a finite-dimensional product vector space is differentiable
almost everywhere. Superseded by `ae_differentiableWithinAt_of_mem`.  -/
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {f : ℝ → ι → ℝ} {s : Set ℝ},
  LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.one : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop} (j : J),
  MonCat.Colimits.Relation.below ⋯
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.stalkClosedPointTo f))
      (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (f (IsLocalRing.closedPoint ↑R))) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Std.Http.Data.URI.Basic
/-- Sets the fragment identifier. The fragment will be automatically percent-encoded when building.
 -/
Std.Http.URI.Builder.setFragment : Std.Http.URI.Builder → String → Std.Http.URI.Builder
-- Mathlib.Topology.Separation.PerfectlyNormal
/-- **Alias** of `Topology.IsInducing.perfectlyNormalSpace`. -/
Topology.IsEmbedding.perfectlyNormalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PerfectlyNormalSpace Y]
  {e : X → Y}, Topology.IsInducing e → PerfectlyNormalSpace X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_get?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.cocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A), P.cocone.pt = A
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.ofMonComon C).obj M = CategoryTheory.Bimon.ofMonComonObj M
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (i : ℕ) (h : u = w) (h' : v = x),
  (p.copy h h').getVert i = p.getVert i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
generateFrom_Ico_mem_le_borel : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] (s t : Set α),
  MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S} ≤ borel α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Order.MinMax
min_lt_max : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b < max a b ↔ a ≠ b
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.mk.inj : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst_1 : TopologicalSpace Y}
  {Z : Type v'} {inst_2 : TopologicalSpace Z} {toFun : Y → Z} {prop : Topology.ContinuousGeneratedBy X toFun}
  {toFun_1 : Y → Z} {prop_1 : Topology.ContinuousGeneratedBy X toFun_1},
  { toFun := toFun, prop := prop } = { toFun := toFun_1, prop := prop_1 } → toFun = toFun_1
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaEquivSigmaPLift_apply : ∀ {α : Sort u_2} (β : α → Sort u_1) (a : (i : α) ×' β i),
  (Equiv.psigmaEquivSigmaPLift β) a = ⟨{ down := a.fst }, { down := a.snd }⟩
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.vsub_self_eq_iff_zero_mem : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : AffineSubspace k V}
  [Nonempty ↥s], ↑s -ᵥ ↑s = ↑s ↔ 0 ∈ s
-- Mathlib.Topology.PartitionOfUnity
/-- If `f` is a partition of unity that is subordinate to a family of open sets `U i` and
`g : ι → X → E` is a family of functions such that each `g i` is continuous on `U i`, then the sum
`fun x ↦ ∑ᶠ i, f i x • g i x` is a continuous function.  -/
PartitionOfUnity.IsSubordinate.continuous_finsum_smul : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
  [inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X}
  {f : PartitionOfUnity ι X s} [ContinuousAdd E] {U : ι → Set X},
  (∀ (i : ι), IsOpen (U i)) →
    f.IsSubordinate U →
      ∀ {g : ι → X → E}, (∀ (i : ι), ContinuousOn (g i) (U i)) → Continuous fun x => ∑ᶠ (i : ι), (f i) x • g i x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Zero loci of minimal prime ideals over `I` are irreducible components in `zeroLocus I` and any
irreducible component is a zero locus of some minimal prime ideal.  -/
Ideal.minimalPrimes.equivIrreducibleComponents : {R : Type u} →
  [inst : CommSemiring R] →
    (I : Ideal R) → ↑I.minimalPrimes ≃o (↑(irreducibleComponents ↑(PrimeSpectrum.zeroLocus ↑I)))ᵒᵈ
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mem_ker : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (v : V₁), v ∈ f.ker ↔ f v = 0