mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MinMaxOn
List.maxOn?_eq_minOn? : ∀ {β : Type u_1} {α : Type u_2} {le : LE β} {dle : DecidableLE β} {xs : List α} {f : α → β},
  List.maxOn? f xs = List.minOn? f xs
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instNeg.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  AddMonoid.Coprod.instNeg =
    {
      neg :=
        Quotient.map'
          (fun w => FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse) ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.degree_pos_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : Fintype ↑(G.neighborSet u)],
  u ≠ v → G.Reachable u v → 0 < G.degree u
-- Mathlib.Algebra.Group.Defs
zero_sub : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 0 - a = -a
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.length_rowLens : ∀ {μ : YoungDiagram}, μ.rowLens.length = μ.colLen 0
-- Lean.Environment
Lean.ConstantKind.ofConstantInfo : Lean.ConstantInfo → Lean.ConstantKind
-- Mathlib.MeasureTheory.Measure.Hausdorff
IsometryEquiv.map_hausdorffMeasure : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ),
  MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.hausdorffMeasure d) = MeasureTheory.Measure.hausdorffMeasure d
-- Mathlib.Order.WithBot
WithTop.eq_top_iff_forall_ge : ∀ {α : Type u_1} [inst : Preorder α] {x : WithTop α} [NoTopOrder α], x = ⊤ ↔ ∀ (b : α), ↑b ≤ x
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Given a weight `W : J ⥤ Type w` and `F : J ⥤ C`, we say that
the `W`-weighted limit of `F` exists if the functor
`CategoryOfElements.π W ⋙ F : W.Elements ⥤ C` has a limit.  -/
CategoryTheory.Limits.HasWeightedLimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor J (Type w) → CategoryTheory.Functor J C → Prop
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatOfNatInst : Lean.Meta.Simp.DSimproc
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentHighlightParams : Lean.ToJson Lean.Lsp.DocumentHighlightParams
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_mulHom_mk : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x)
  (h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y),
  ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := ⇑f, map_mul' := h₄ }
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- Extension for `ArithmeticFunction.sigma`.  -/
Mathlib.Meta.Positivity.evalArithmeticFunctionSigma : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.nsmul : ∀ {α : Type u_2} [inst : AddCancelMonoid α] {s : Set α}, s.Nontrivial → ∀ {n : ℕ}, n ≠ 0 → (n • s).Nontrivial
-- Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
/-- If the identity operator of a Banach space over a nontrivially normed field is compact,
then the space is finite dimensional.  -/
FiniteDimensional.of_isCompactOperator_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E],
  IsCompactOperator id → FiniteDimensional 𝕜 E
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centralizer_centralizer_centralizer : ∀ {R : Type u_1} [inst : Semiring R] {s : Set R},
  Subsemiring.centralizer s.centralizer.centralizer = Subsemiring.centralizer s
-- Std.Sat.AIG.CNF
/-- The key invariant about the `State` itself (without cache): The CNF we produce is always satisfiable
at `cnfSatAssignment`.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv : Std.Sat.AIG ℕ → Std.Sat.CNF ℕ → Prop
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.mk : Lean.NameMap Lean.Meta.SimpTheorem →
  Lean.NameMap (Lean.Name × Lean.Name) → Lean.NameSet → Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.zpow_eq_zpow_on_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) {m n : ℤ} {x : α},
  g x ≠ x → ((g ^ m) x = (g ^ n) x ↔ m % ↑(g.cycleOf x).support.card = n % ↑(g.cycleOf x).support.card)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.comap_mk.symm_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.comap (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk x)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizers : CategoryTheory.Limits.HasCoequalizers AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots_zero_right : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ), Polynomial.nthRoots n 0 = Multiset.replicate n 0
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv_id : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁],
  (CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.id F₁) =
    CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.sphere.instCommGroup : {𝕜 : Type u_1} → [inst : NormedField 𝕜] → CommGroup ↑(Metric.sphere 0 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.of_isBilimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPushout 0 0 b.inl b.inr
-- Mathlib.LinearAlgebra.Ray
/-- The images of two vectors under an injective linear map are on the same ray if and only if the
original vectors are on the same ray.  -/
Function.Injective.sameRay_map_iff : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {x y : M} {F : Type u_6} [inst_7 : FunLike F M N] [LinearMapClass F R M N] {f : F},
  Function.Injective ⇑f → (SameRay R (f x) (f y) ↔ SameRay R x y)
-- Mathlib.Order.Defs.Unbundled
symm : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Symm r], r a b → r b a
-- Mathlib.Topology.Instances.Int
Int.preimage_ball : ∀ (x : ℤ) (r : ℝ), Int.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instCharZero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], CharZero ℤ_[p]
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.FixedTermElabRef.toFixedTermElab : Lean.Elab.Term.FixedTermElabRef → Lean.Elab.Term.FixedTermElab
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- `PowerSeries` on a `T2Space` form a `T2Space`  -/
PowerSeries.WithPiTopology.instT2Space : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R], T2Space (PowerSeries R)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
/-- Construction of the binary biproduct data for functors `F` and `G`  -/
CategoryTheory.Limits.pointwiseBinaryBiproductData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {D : Type u_2} →
          [inst_3 : CategoryTheory.Category.{v_2, u_2} D] →
            (F G : CategoryTheory.Functor D C) → CategoryTheory.Limits.BinaryBiproductData F G
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
SSet.StrictSegal.spineToDiagonal.eq_1 : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n),
  sx.spineToDiagonal f =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.diagonal X)) (sx.spineToSimplex f)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- If `x` is an adherent (cluster) point for a Cauchy filter `f`, then it is a limit point
for `f`.  -/
le_nhds_of_cauchy_adhp : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α}, Cauchy f → ClusterPt x f → f ≤ nhds x
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.id_mapComp : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.OplaxFunctor.id B).mapComp f g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.dualProd_apply : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Module.Dual R M × M), (QuadraticForm.dualProd R M) p = p.1 p.2
-- Lean.Data.Lsp.Extra
/-- Always build dependencies.  -/
Lean.Lsp.DependencyBuildMode.always : Lean.Lsp.DependencyBuildMode
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_rci : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rci α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₃ : CategoryTheory.MorphismProperty C₃} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence]
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₃) [Ψ.IsLocalizedEquivalence], (Φ.comp Ψ).IsLocalizedEquivalence
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_range_zero : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M), ∏ k ∈ Finset.range 0, f k = 1
-- Mathlib.LinearAlgebra.TensorProduct.Basic
LinearMap.compr₂ₛₗ.congr_simp : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f f_1 : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P),
  f = f_1 → ∀ (g g_1 : P →ₛₗ[σ₃₄] Q), g = g_1 → f.compr₂ₛₗ g = f_1.compr₂ₛₗ g_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {Z : C} (h : G.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v j j ⋯) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (φ.f j) +
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v i i ⋯) (G.d i j))
      h
-- Mathlib.GroupTheory.Nilpotent
/-- A nilpotent subgroup is solvable  -/
IsNilpotent.to_isSolvable : ∀ {G : Type u_1} [inst : Group G] [h : Group.IsNilpotent G], Group.IsSolvable G
-- Mathlib.RingTheory.Polynomial.Pochhammer
Nat.cast_ascFactorial : ∀ (S : Type u_1) [inst : Semiring S] (a b : ℕ), ↑(a.ascFactorial b) = Polynomial.eval (↑a) (ascPochhammer S b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.congr_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Logic.Function.Coequalizer
Function.Coequalizer.Rel.intro : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} (x : α), Function.Coequalizer.Rel f g (f x) (g x)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- The value wrapped into a term of `PreQuasiregular`.  -/
PreQuasiregular.val : {R : Type u_1} → PreQuasiregular R → R
-- Init.Data.Array.Attach
Array.pmap_attach : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {p : { x // x ∈ xs } → Prop} {f : (a : { x // x ∈ xs }) → p a → β}
  (H : ∀ a ∈ xs.attach, p a), Array.pmap f xs.attach H = Array.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) xs ⋯
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.withBotCoe_subset_iff : ∀ {ι : Type u_1} {I J : WithBot (BoxIntegral.Box ι)}, ↑I ⊆ ↑J ↔ I ≤ J
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
TopCat.Presheaf.pushforwardEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f g : X ⟶ Y} (h : f = g)
  (ℱ : TopCat.Presheaf C X), TopCat.Presheaf.pushforwardEq h ℱ = TopCat.Presheaf.pushforwardEq h ℱ
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n : ℤ),
  CategoryTheory.Projective (R.cochainComplex.X n)
-- Init.Data.String.TakeDrop
String.takeRight : String → ℕ → String
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype.match_1.eq_1 : ∀
  (motive :
    (x : ℕ) →
      (x_1 : TypeVec.{u_1} x) →
        (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
          (x_3 : Fin2 x) → { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) } → Sort u_2)
  (n : ℕ) (x : TypeVec.{u_1} n.succ) (p : x.Arrow (TypeVec.repeat n.succ Prop)) (i : Fin2 n)
  (x_1 : { x // TypeVec.ofRepeat (p i.fs x) })
  (h_1 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (p : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (i : Fin2 n) → (x_2 : { x // TypeVec.ofRepeat (p i.fs x) }) → motive n.succ x p i.fs x_2)
  (h_2 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (x_2 : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (x_3 : { x // TypeVec.ofRepeat (x_2 Fin2.fz x) }) → motive n.succ x x_2 Fin2.fz x_3),
  (match n.succ, x, p, i.fs, x_1 with
    | n.succ, x, p, i.fs, x_2 => h_1 n x p i x_2
    | n.succ, x, x_2, Fin2.fz, x_3 => h_2 n x x_2 x_3) =
    h_1 n x p i x_1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `pullbackCone f g pb` is a pullback.  -/
CategoryTheory.Limits.FormalCoproduct.isLimitPullbackCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : CategoryTheory.Limits.FormalCoproduct C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (pb :
              (i : Function.Pullback f.f g.f) →
                CategoryTheory.Limits.PullbackCone
                  (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) →
            ((i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- Given a cocone `t` of `F`, the induced monoid linear map from the colimit to the cocone point.
We already know that this is a morphism between additive groups. The only thing left to see is that
it is a linear map, i.e. preserves scalar multiplication.
 -/
ModuleCat.FilteredColimits.colimitDesc : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) →
            (t : CategoryTheory.Limits.Cocone F) → ModuleCat.FilteredColimits.colimit F ⟶ t.pt
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leIdeal_zero : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u_1) [inst_1 : Field K] (v : Valuation K Γ₀),
  v.leIdeal 0 = ⊥
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more
generally, on `MulOneClass` type) is reflexive.  -/
SemiconjBy.refl : ∀ {M : Type u_2} [inst : MulOneClass M], Std.Refl fun a b => ∃ c, SemiconjBy c a b
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α),
  eVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) = eVariationOn f s
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, ⊤.arrows = ⊤
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton' : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K]
  (α : LieModule.Weight K (↥H) L),
  ↑(LieAlgebra.corootSpace ⇑α) =
    K ∙ (LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion : CategoryTheory.Limits.WalkingReflexivePair.one.Hom CategoryTheory.Limits.WalkingReflexivePair.one
-- Mathlib.Topology.Instances.Shrink
Shrink.instTopologicalSpace : (X : Type u) → [TopologicalSpace X] → [inst : Small.{v, u} X] → TopologicalSpace (Shrink.{v, u} X)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_mono : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ}, a < b → Monotone fun N ω => MeasureTheory.upcrossingsBefore a b f N ω
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α}
  (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → ⟨k, v⟩ ∈ l → (t.insertMany l).get? k' = some (cast ⋯ v)
-- Init.Data.Array.MinMax
Array.isSome_min?_of_ne_empty : ∀ {α : Type u_1} [inst : Min α] (xs : Array α), xs ≠ #[] → xs.min?.isSome = true
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If a function is continuous outside of a countable set, it is measurable.  -/
ContinuousOn.measurable_of_countable_compl : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] [MeasurableSingletonClass α] {f : α → γ}
  {s : Set α}, ContinuousOn f s → sᶜ.Countable → Measurable f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) {s : Set ι},
  s.Finite → (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.getRuleSet : Lean.MVarId → Aesop.Frontend.TacticConfig → Lean.Elab.TermElabM Aesop.LocalRuleSet
-- Mathlib.Data.Set.Sigma
/-- **Alias** of `Set.sigma_sdiff_sigma`. -/
Set.sigma_diff_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
-- Init.System.IOError
/-- An operation failed due to insufficient permissions.

This corresponds to the POSIX errors `EACCES`, `EROFS`, `ECONNABORTED`, `EFBIG`, and `EPERM`.
 -/
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {h' : a ∈ t.erase k},
  Std.DTreeMap.Raw.Const.get (t.erase k) a h' = Std.DTreeMap.Raw.Const.get t a ⋯
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_toAdditive_ker : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'),
  (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.le_weightedOrder_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (w : τ → ℕ),
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R),
      ⨅ d, ⨅ (_ : (MvPowerSeries.coeff d) f ≠ 0), (Finsupp.weight (MvPowerSeries.weightedOrder w ∘ a)) d ≤
        MvPowerSeries.weightedOrder w (MvPowerSeries.subst a f)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize : ByteArray.utf8DecodeChar?.FirstByte → ℕ
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.addEquivOp_apply_coe : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (a : ↥S.toSubmonoid), ↑(S.addEquivOp a) = MulOpposite.op ↑a
-- Std.Time.DateTime.WallTime
Std.Time.instReprWallTime : Repr Std.Time.WallTime
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg c_1) =
    (c = c_1)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instPartialOrder : {K : Type u} → [inst : Field K] → PartialOrder (ValuationSubring K)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.symm : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y → IsCoprime y x