mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerRight.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ≅ Gₗ)
  (H : CategoryTheory.Functor D E'),
  CategoryTheory.Join.mapIsoWhiskerRight α H =
    CategoryTheory.Join.mkNatIso
      (CategoryTheory.Join.mapPairLeft Fₗ H ≪≫
        CategoryTheory.Functor.isoWhiskerRight α (CategoryTheory.Join.inclLeft E E') ≪≫
          (CategoryTheory.Join.mapPairLeft Gₗ H).symm)
      (CategoryTheory.Join.mapPairRight Fₗ H ≪≫
        CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Iso.refl H) (CategoryTheory.Join.inclRight E E') ≪≫
          (CategoryTheory.Join.mapPairRight Gₗ H).symm)
      ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of limits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsLimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.continuous_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ],
  Continuous (MeasureTheory.charFun μ)
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- Two points in a projective space are independent if and only if the points are not equal.  -/
Projectivization.independent_pair_iff_ne : ∀ {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (u v : Projectivization K V), Projectivization.Independent ![u, v] ↔ u ≠ v
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.iSup_def : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α),
  ⨆ i, s i = { carrier := ⋃ i, ↑(s i), is_open' := ⋯ }
-- Mathlib.GroupTheory.Coset.Basic
mem_own_leftCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a • ↑s
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.ofLex_degree_snd : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} {e : ChevalleyThm.PolynomialC.InductionObj✝ R n},
  (ofLex (ChevalleyThm.PolynomialC.InductionObj.degree✝ e)).2 ↔
    ¬∃ i,
        (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).Monic ∧
          ∀ (j : Fin n),
            ChevalleyThm.PolynomialC.InductionObj.val✝ e j ≠ 0 →
              (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).degree ≤
                (ChevalleyThm.PolynomialC.InductionObj.val✝ e j).degree
-- Init.Data.Vector.Lemmas
Vector.toList_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {start stop : ℕ},
  (xs.extract start stop).toList = List.take (stop - start) (List.drop start xs.toList)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.isoMk_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} (e : X.obj ≅ Y.obj) (h₁ : P e.hom)
  (h₂ : P e.inv), (CategoryTheory.WideSubcategory.isoMk e h₁ h₂).inv.hom = e.inv
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.head_eq_head : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op →
    ∀ {x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
      x.head = y.head → (op x).head = (op y).head
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fintypeEdgeSet : {V : Type u} → (G : SimpleGraph V) → [Fintype (Sym2 V)] → [DecidableRel G.Adj] → Fintype ↑G.edgeSet
-- Mathlib.Topology.Algebra.ProperAction.Basic
properVAdd_iff : ∀ (G : Type u_1) (X : Type u_2) [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup G]
  [inst_3 : AddAction G X], ProperVAdd G X ↔ IsProperMap fun gx => (gx.1 +ᵥ gx.2, gx.2)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.max?_eq_toList_getLast? : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.max? = t.toList.getLast?
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.toConvexCone_inf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C₁ C₂ : Submodule R M), (C₁ ⊓ C₂).toConvexCone = C₁.toConvexCone ⊓ C₂.toConvexCone
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitMonoMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f] (F : CategoryTheory.Functor C D),
  CategoryTheory.IsSplitMono (F.map f)
-- Init.Prelude
/-- Decides whether two Booleans are equal.

This function should normally be called via the `DecidableEq Bool` instance that it exists to
support.
 -/
Bool.decEq : (a b : Bool) → Decidable (a = b)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.zpow_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A B : Matrix n' n' R}, Commute A B → ∀ (m n : ℤ), Commute (A ^ m) (B ^ n)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.CartesianMonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} [inst_9 : F.Braided]
  {G : CategoryTheory.Functor D E} [inst_10 : G.Braided] (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Functor.mapCommGrpCompIso.hom.app X).hom.hom.hom =
    CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- The inverse rotation of triangles gives an endofunctor on the category of triangles in `C`.
 -/
CategoryTheory.Pretriangulated.invRotate : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_monomial_same : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), (PowerSeries.coeff n) ((PowerSeries.monomial n) a) = a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iic.inj : ∀ {n n_1 : Lean.Term}, BigOperators.FinsetResult.Iic✝ n = BigOperators.FinsetResult.Iic✝ n_1 → n = n_1
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.contains : ∀ {l m r : List Char} (c : Char) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → (Substring.Raw.Legacy.contains s c = true ↔ c ∈ m)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_addConst : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (k : ℤ), Lean.Grind.CommRing.Poly.denote ctx (p.addConst k) = Lean.Grind.CommRing.Poly.denote ctx p + ↑k
-- Mathlib.Algebra.BigOperators.Associated
Multiset.prod_primes_dvd : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] [inst_2 : (a : M₀) → DecidablePred (Associated a)]
  {s : Multiset M₀} (n : M₀),
  (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), Multiset.countP (Associated a) s ≤ 1) → s.prod ∣ n
-- Mathlib.ModelTheory.Definability
Set.definable_iInter_of_finite : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2} [Finite ι]
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → A.Definable L (⋂ i, f i)
-- Lean.Meta.Basic
/-- `whnf` with at most instances transparency.  -/
Lean.Meta.whnfAtMostI : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ), hτ.measurableSpace ≤ m
-- Mathlib.Algebra.Notation.Support
Set.image_inter_mulSupport_eq : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set κ} {g : κ → ι},
  g '' s ∩ Function.mulSupport f = g '' (s ∩ Function.mulSupport (f ∘ g))
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_subAt : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x y : List A), y ∈ Descriptive.Tree.subAt T x ↔ x ++ y ∈ T
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_add_C_pow : ∀ {R : Type u} [inst : Semiring R] (r : R) (n k : ℕ),
  ((Polynomial.X + Polynomial.C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α}, m₁.getKey? k = m₂.getKey? k
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.instIsRelationalGraph : FirstOrder.Language.graph.IsRelational
-- Mathlib.Algebra.Notation.Support
Pi.subsingleton_mulSupport_mulSingle : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i : ι} {a : M},
  (Function.mulSupport (Pi.mulSingle i a)).Subsingleton
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_one : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.basicOpen 𝒜 1 = ⊤
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_even : ∀ {α : Type u_4} {f : α → α} {n : ℕ}, Function.Involutive f → Even n → f^[n] = id
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.toLocalizationMap_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R),
  (IsLocalization.toLocalizationMap M S) x = (algebraMap R S) x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.mk.sizeOf_spec : ∀ (term? : Option Lean.Term) (phase? : Option Aesop.PhaseName) (priority? : Option Aesop.Frontend.Priority)
  (builder? : Option Aesop.Frontend.DBuilderName) (builderOptions : Aesop.RuleBuilderOptions)
  (ruleSets : Aesop.Frontend.RuleSets),
  sizeOf
      { term? := term?, phase? := phase?, priority? := priority?, builder? := builder?,
        builderOptions := builderOptions, ruleSets := ruleSets } =
    1 + sizeOf term? + sizeOf phase? + sizeOf priority? + sizeOf builder? + sizeOf builderOptions + sizeOf ruleSets
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instInfSet : {R : Type u} → [inst : NonAssocSemiring R] → InfSet (Subsemiring R)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.Functor.faithful_of_comp_of_hasLeftCalculusOfFractions : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {E : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [W.HasLeftCalculusOfFractions],
  (∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g) → F.Faithful
-- Mathlib.Order.Filter.CardinalInter
/-- Construct a filter with cardinal `c` intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the cardinal `c` intersection property.  -/
Filter.ofCardinalInter : {α : Type u} →
  {c : Cardinal.{u}} →
    (l : Set (Set α)) →
      2 < c →
        (∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ l → ⋂₀ S ∈ l) →
          (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
-- Mathlib.Data.Matrix.Mul
single_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
  (v : m → α) (x : α) (i : m), Pi.single i x ⬝ᵥ v = x * v i
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_ne_zero : ∀ {n : ℕ} [inst : NeZero n] {a : Fin (n + 1)} {b : Fin n}, a ≠ 0 → b ≠ 0 → a.succAbove b ≠ 0
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableOn_extChartAt : ∀ {𝕜 : 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] [IsManifold I 1 M] {x : M},
  MDiff[(chartAt H x).source] ↑(extChartAt I x)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m₁ m₂ : ι},
  m₁ ≤ m₂ →
    (∃ j ∈ Set.Icc n m₁, u j ω ∈ s) → MeasureTheory.hittingBtwn u s n m₁ ω = MeasureTheory.hittingBtwn u s n m₂ ω
-- Mathlib.Data.Finset.Sym
Finset.sym2_singleton : ∀ {α : Type u_1} (a : α), {a}.sym2 = {Sym2.diag a}
-- Mathlib.Order.InitialSeg
/-- Composition of an order isomorphism with a principal segment embedding, as a principal
segment embedding  -/
PrincipalSeg.relIsoTrans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≃r s → PrincipalSeg s t → PrincipalSeg r t
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_zero : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)), SimplexCategory.II.map' f 0 = 0
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_add_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd α α] {s t : Set α},
  s + interior t ⊆ interior (s + t)
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ContinuousLinearMap.IsPositive 0
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.mkQ_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  Function.Surjective ⇑p.mkQ
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.OneStep.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (M N : Multiset α),
  Multiset.OneStep✝ M N = ∃ X Y a, M = X + Y ∧ N = X + {a} ∧ ∀ y ∈ Y, y < a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.le_degree : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} [inst : Fintype ↑(G.neighborSet u)],
  G.IsEdgeReachable k u v → u ≠ v → k ≤ G.degree u
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.reflection_coweightEquiv : ∀ {ι : 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) (i : ι),
  RootPairing.Equiv.coweightEquiv P P (RootPairing.Equiv.reflection P i) = P.coreflection i
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.homology 0 ≅ K.opcycles 0` for a chain complex `K`
indexed by `ℕ`.  -/
ChainComplex.isoHomologyι₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : ChainComplex C ℕ) →
        [inst_2 : HomologicalComplex.HasHomology K 0] →
          HomologicalComplex.homology K 0 ≅ HomologicalComplex.opcycles K 0
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal_carrier : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (Φ : LinearMap.BilinForm R M)
  (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M),
  ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = {y | ∀ x ∈ N, (Φ x) y = 0}
-- Init.Data.Array.Count
Array.filter_beq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} (a : α),
  Array.filter (fun x => x == a) xs = Array.replicate (Array.count a xs) a
-- Mathlib.CategoryTheory.Limits.Cones
/-- A natural transformation from the constant functor at `X` to `F`  -/
CategoryTheory.Limits.Cone.π : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (self : CategoryTheory.Limits.Cone F) → (CategoryTheory.Functor.const J).obj self.pt ⟶ F
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_nonempty_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, (connectedComponentIn F x).Nonempty ↔ x ∈ F
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_ofHom : ∀ {M N : Type u} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N), MonCat.Hom.hom (MonCat.ofHom f) = f
-- Mathlib.Order.Filter.IndicatorFunction
mulIndicator_biUnion_finset_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : One β] (s : ι → Set α) (f : α → β) (a : α),
  (fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (Set.iUnion s).mulIndicator f a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentColorParams : Lean.FromJson Lean.Lsp.DocumentColorParams
-- Mathlib.Data.Fintype.Card
Finset.compl_eq_of_disjoint_of_card_add_eq : ∀ {ι : Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι] {S₁ S₂ : Finset ι},
  Disjoint S₁ S₂ → S₁.card + S₂.card = Finset.univ.card → S₁ᶜ = S₂
-- Mathlib.NumberTheory.Harmonic.Int
/-- The 2-adic valuation of the n-th harmonic number is the negative of the logarithm of n.  -/
padicValRat_two_harmonic : ∀ (n : ℕ), padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.obj X_1 =
    ψ.right.obj (S.snd.obj X_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).minKey? = t.minKey?
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {Z : Type u_3} [inst_2 : MetricSpace Z]
  (D : Delone.DeloneSet X) (f : X ≃ᵢ Y) (g : Y ≃ᵢ Z),
  (Delone.DeloneSet.mapIsometry (f.trans g)) D = (Delone.DeloneSet.mapIsometry g) ((Delone.DeloneSet.mapIsometry f) D)
-- Mathlib.Data.DFinsupp.BigOperators
MonoidHom.dfinsuppProd_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : MulOneClass R] [inst_4 : CommMonoid S]
  (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) (r : R), (f.prod g) r = f.prod fun a b => (g a b) r
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The map of a cokernel cofork is a colimit iff
the cokernel cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `CokernelCofork.ofπ` with `Functor.mapCocone`.

This is a variant of `isColimitMapCoconeCoforkEquiv` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
 -/
CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  {f : X ⟶ Y} →
                    {h : Y ⟶ Z} →
                      (w : CategoryTheory.CategoryStruct.comp f h = 0) →
                        CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ h w)) ≃
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (G.map h) ⋯)
-- Mathlib.Logic.Encodable.Basic
/-- Explicit decoding function for the sum of two encodable types.  -/
Encodable.decodeSum : {α : Type u_1} → {β : Type u_2} → [Encodable α] → [Encodable β] → ℕ → Option (α ⊕ β)
-- Lean.Meta.Basic
Lean.Meta.FunInfoCache : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.negY P = -P 1 - W'.a₁ * P 0 - W'.a₃ * P 2
-- Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
/-- If `C` has (small) products and a small weakly initial set of objects, then it has a weakly initial
object.
 -/
CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {ι : Type v} {B : ι → C},
  (∀ (A : C), ∃ i, Nonempty (B i ⟶ A)) → ∃ T, ∀ (X : C), Nonempty (T ⟶ X)