mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
PartialHomeomorph.mk.congr_simp : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (toPartialEquiv toPartialEquiv_1 : PartialEquiv X Y) (e_toPartialEquiv : toPartialEquiv = toPartialEquiv_1)
  (continuousOn_toFun : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source)
  (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target),
  { toPartialEquiv := toPartialEquiv, continuousOn_toFun := continuousOn_toFun,
      continuousOn_invFun := continuousOn_invFun } =
    { toPartialEquiv := toPartialEquiv_1, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inl_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (x : α), (OrderAddMonoidHom.inl α β) x = (x, 0)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.mapConeToUnder_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.mapConeToUnder.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
  {v : β k} {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true},
  Std.Internal.List.getEntry a (Std.Internal.List.insertEntry k v l) h =
    if h' : (k == a) = true then ⟨k, v⟩ else Std.Internal.List.getEntry a l ⋯
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atBot_atTop : ∀ {α : Type u_3} [inst : PartialOrder α] [Nontrivial α], Disjoint Filter.atBot Filter.atTop
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The `k`-th shadow of a family of `r`-sets is a family of `r - k`-sets.  -/
Set.Sized.shadow_iterate : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {k r : ℕ},
  Set.Sized r ↑𝒜 → Set.Sized (r - k) ↑(Finset.shadow^[k] 𝒜)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.subtype_mk : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → ∀ {s : Set β} {hfs : ∀ (x : α), f x ∈ s}, AEMeasurable (Set.codRestrict f s hfs) μ
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.ext : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {x y : DiscreteTiling.Protoset G X ιₚ}, ↑x = ↑y → x = y
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.instQuasiIsoAtπTruncGEF : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i : ι), QuasiIsoAt (K.πTruncGE e) (e.f i)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.toLp_apply : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) (x : (i : ι) → α i) (i : ι), (WithLp.toLp p x).ofLp i = x i
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inr_comp_pushoutObjIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D)
  {Z : C} (h : (CategoryTheory.Limits.pushout f g).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (f.app d) (g.app d))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutObjIso f g d).inv h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inr f g).app d) h
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.functor_unfold : ∀ {basis : Tactic.ComputeAsymptotics.Basis} (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis),
  ms.Approximates =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor
      (@Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates) ms
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density_le_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ}, κ.fst ≤ ν → ∀ (a : α) (x : γ) (s : Set β), κ.density ν a x s ≤ 1
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumLeft_symm_lof_tmul : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  [inst_3 : DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i : ι₁) (x : M₁ i)
  (y : M₂'),
  (TensorProduct.directSumLeft R S M₁ M₂').symm
      ((DirectSum.lof S ι₁ (fun i => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)) =
    (DirectSum.lof S ι₁ M₁ i) x ⊗ₜ[R] y
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.Equiv.trans : ∀ {m : Type w → Type w'} {α₁ α₂ α₃ β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [inst_4 : Std.Iterator α₃ m β] {ita : Std.IterM m β} {itb : Std.IterM m β}
  {itc : Std.IterM m β}, ita.Equiv itb → itb.Equiv itc → ita.Equiv itc
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaCongrRight_apply : ∀ {α : Sort u} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) ×' β₁ a),
  (Equiv.psigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.of_ne_zero : ∀ {α : Type u} (x : α), FreeAbelianGroup.of x ≠ 0
-- Lean.Meta.Tactic.Grind.Finish
Lean.Meta.Grind.Action.maxIterationsDefault : ℕ
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.balLeft.match_4.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b with
    | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
    | l => h_2 l) =
    h_1 a x b
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {X Y : G.Coalgebra}
  {f g : X ⟶ Y}, f = g ↔ f.f = g.f
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_toArray_rcc : ∀ {m n : ℤ}, (m<...=n).toArray = ((m + 1)...=n).toArray
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.zero_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] (B : Matrix n p β), Matrix.kroneckerMap (TensorProduct.tmul R) 0 B = 0
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_ofNat : ∀ (n : ℕ) (h : System.Platform.numBits = 32), (OfNat.ofNat n).toBitVec32 h = BitVec.ofNat 32 n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t₁ t₂ : Finset α}, s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.surj : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {S : Submonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ (z : N), ∃ x, z * f ↑x.2 = f x.1
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_left_convexCombPair : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist x (Convexity.convexCombPair s t hs ht h x y) = t * dist x y
-- Mathlib.Topology.Defs.Induced
WithTopology.instTopologicalSpace : (X : Type u_1) → (t : TopologicalSpace X) → TopologicalSpace (WithTopology X t)
-- Mathlib.Data.Finset.Union
Finset.disjoint_disjiUnion_right : ∀ {α : Type u_1} {β : Type u_2} (s : Finset β) (t : Finset α) (f : α → Finset β) (hf : (↑t).PairwiseDisjoint f),
  Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instLECastInt : {d : ℕ} → LE (ℤ√↑d)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `SeminormedGroup` structure from a `GroupSeminormClass` on a `Group`.  -/
GroupSeminormClass.toSeminormedGroup : {F : Type u_1} →
  {α : Type u_2} → [inst : FunLike F α ℝ] → [inst_1 : Group α] → [GroupSeminormClass F α ℝ] → F → SeminormedGroup α
-- Init.Data.UInt.Bitwise
UInt64.and_eq_neg_one_iff : ∀ {a b : UInt64}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Mathlib.Data.Finset.PImage
Finset.pimage_union : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s t : Finset α} [inst_2 : DecidableEq α], Finset.pimage f (s ∪ t) = Finset.pimage f s ∪ Finset.pimage f t
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.const_eq_id : { len := 0 }.const { len := 0 } 0 = CategoryTheory.CategoryStruct.id { len := 0 }
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  (AddMonoid.Coprod.map f g).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inl.comp f
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.one_vle_inv : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {x : K}, x ≠ 0 → (1 ≤ᵥ x⁻¹ ↔ x ≤ᵥ 1)
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.add_eq_max_of_ne' : ∀ {α : Type u_2} {S : Type u_3} [inst : LinearOrder S] [inst_1 : AddCommGroup α] (f : α → S),
  IsNonarchimedean f → (∀ (a : α), f a = f (-a)) → ∀ {a b : α}, f a ≠ f b → f (a + b) = max (f a) (f b)
-- Init.Data.Array.Lemmas
Array.map_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β},
  Array.map f xs = ys ↔ ∀ (i : ℕ), ys[i]? = Option.map f xs[i]?
-- Mathlib.FieldTheory.Normal.Closure
normalClosure_eq_iSup_adjoin' : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L],
  IntermediateField.normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
-- Mathlib.Topology.UrysohnsLemma
/-- By assumption, for each `c : CU P` there exists an open set `u`
such that `c.C ⊆ u` and `closure u ⊆ c.U`. `c.left` is the pair `(c.C, u)`.  -/
Urysohns.CU.left : {X : Type u_1} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Urysohns.CU P
-- Mathlib.Analysis.Normed.Group.InfiniteSum
tsum_enorm_ne_top_iff_summable_nnnorm : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {ι : Type u_6} {f : ι → E},
  ∑' (i : ι), ‖f i‖ₑ ≠ ⊤ ↔ Summable fun i => ‖f i‖₊
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_modByMonic_le_left : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, (p %ₘ q).degree ≤ p.degree
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M) (t : Submonoid N),
  ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Algebra.Group.Subgroup.Ker
MulEquiv.map_range_powMonoidHom : ∀ {M : Type u_5} {N : Type u_6} [inst : CommGroup M] [inst_1 : CommGroup N] (e : M ≃* N) (n : ℕ),
  Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_eq_sSup : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] (s : Set X), Metric.ediam s = sSup (Set.image2 edist s s)
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_eq_agm_agmSequences_fst_agmSequences_snd : ∀ {x y : NNReal} (n : ℕ), x.agm y = (x.agmSequences y n).1.agm (x.agmSequences y n).2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_add_eq_toReal_add_toReal : ∀ {θ ψ : Real.Angle},
  θ ≠ ↑Real.pi → ψ ≠ ↑Real.pi → θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign → (θ + ψ).toReal = θ.toReal + ψ.toReal
-- Mathlib.Analysis.Normed.Group.Bounded
isBounded_iff_forall_norm_le : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement'.symm : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsComplement' K → K.IsComplement' H
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulR : Nat.Internal.Linear.Expr → ℕ → Nat.Internal.Linear.Expr
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf.eq_1 : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)),
  AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf =
    {
      hom :=
        CategoryTheory.yonedaEquiv.symm
          ((AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).sheafValGluedMk
            (fun i => CategoryTheory.yonedaEquiv (f i)) ⋯) }
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.cgf_le : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ᵐ (ω' : Ω) ∂μ.trim hm,
      ∀ (t : ℝ), ProbabilityTheory.cgf X ((ProbabilityTheory.condExpKernel μ m) ω') t ≤ ↑c * t ^ 2 / 2
-- Mathlib.RingTheory.Ideal.Pure
injective_lTensor_quotient_iff_inf_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] (I J : Ideal R),
  Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_add_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n + 1) - Polynomial.Chebyshev.U R n
-- Batteries.Data.AssocList
Batteries.AssocList.foldlM.eq_def : ∀ {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ) (x : δ)
  (x_1 : Batteries.AssocList α β),
  Batteries.AssocList.foldlM f x x_1 =
    match x, x_1 with
    | d, Batteries.AssocList.nil => pure d
    | d, Batteries.AssocList.cons a b es => do
      let __do_lift ← f d a b
      Batteries.AssocList.foldlM f __do_lift es
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.substFVars : Lean.MVarId → Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.surj₂ : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (z w : S),
  ∃ z' w' d, z * (algebraMap R S) ↑d = (algebraMap R S) z' ∧ w * (algebraMap R S) ↑d = (algebraMap R S) w'
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the value `q ≥ 0` where
`β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.

In the absence of linear independence, it takes a junk value.  -/
RootPairing.chainBotCoeff : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : CommRing R] →
            [CharZero R] →
              [IsDomain R] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → {P : RootPairing ι R M N} → [P.IsCrystallographic] → ι → ι → ℕ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = CategoryTheory.Limits.pushoutComparison G f g
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- There is a unique additive monoid homomorphism between two additive monoids with
a unique element.  -/
ContinuousAddEquiv.instUnique : {M : Type u_3} →
  {N : Type u_4} →
    [Unique M] →
      [Unique N] →
        [inst : Add M] →
          [inst_1 : Add N] → [inst_2 : TopologicalSpace M] → [inst_3 : TopologicalSpace N] → Unique (M ≃ₜ+ N)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.sub_mem : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A) {x y : A},
  x ∈ S → y ∈ S → x - y ∈ S
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_trunc_pow : ∀ {R : Type u_2} [inst : CommSemiring R] (f : PowerSeries R) (n a : ℕ),
  (PowerSeries.trunc n) (↑((PowerSeries.trunc n) f) ^ a) = (PowerSeries.trunc n) (f ^ a)
-- Init.Data.SInt.Bitwise
Int16.toInt8_or : ∀ (a b : Int16), (a ||| b).toInt8 = a.toInt8 ||| b.toInt8
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.lt_univ' : ∀ {c : Cardinal.{max (u + 1) v}}, c < Cardinal.univ.{u, v} ↔ ∃ c', c = Cardinal.lift.{max (u + 1) v, u} c'
-- Mathlib.Algebra.Order.Antidiag.Pi
/-- The finset of functions `ι → μ` with support contained in `s` and sum `n`.  -/
Finset.piAntidiag : {ι : Type u_1} →
  {μ : Type u_2} →
    [DecidableEq ι] →
      [inst : AddCommMonoid μ] → [Finset.HasAntidiagonal μ] → [DecidableEq μ] → Finset ι → μ → Finset (ι → μ)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.hundred_div_ε_pow_five_le_m : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 → 100 / ε ^ 5 ≤ ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C]
  [inst_4 : CategoryTheory.FinitaryExtensive C]
  [h : ∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
  [CategoryTheory.Limits.ReflectsFiniteLimits s],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s) →
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F
-- Mathlib.Algebra.Lie.Basic
sum_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {ι : Type u_1}
  (s : Finset ι) (f : ι → L) (m : M), ⁅∑ i ∈ s, f i, m⁆ = ∑ i ∈ s, ⁅f i, m⁆
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, t.contains a = (t.get? a).isSome
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` factors through the equalizer of `f` and `g`
via `equalizer.lift : W ⟶ equalizer f g`.  -/
CategoryTheory.Limits.equalizer.lift : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasEqualizer f g] →
          {W : C} →
            (k : W ⟶ X) →
              CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
                (W ⟶ CategoryTheory.Limits.equalizer f g)
-- Mathlib.GroupTheory.Index
Subgroup.inf_relIndex_right : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), (H ⊓ K).relIndex K = H.relIndex K
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyπ_inv_comp_homologyπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp (S.asIsoHomologyπ hf).inv S.homologyπ = CategoryTheory.CategoryStruct.id S.homology
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_le_of_forall_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s} {a o : α}, o ∈ s → (∀ b < a, ↑((Order.enum s hs) b) < o) → ↑((Order.enum s hs) a) ≤ o
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- The category of internal commutative monoid objects in `Type`
is equivalent to the category of "native" bundled commutative monoids.
 -/
commMonTypeEquivalenceCommMon : CategoryTheory.CommMon (Type u) ≌ CommMonCat
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instOne : {α : Type u} → One (WithOne α)
-- Init.Data.SInt.Basic
/-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`.  -/
Int16.ofBitVec : BitVec 16 → Int16
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ₁ μ₂ ν : MeasureTheory.Measure α) [μ₁.HaveLebesgueDecomposition ν]
  [μ₂.HaveLebesgueDecomposition ν], (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
-- Mathlib.RingTheory.NonUnitalSubring.Basic
RingEquiv.ofLeftInverse'_apply : ∀ {R : Type u} {S : Type v} [inst : NonUnitalRing R] [inst_1 : NonUnitalRing S] {g : S → R} {f : R →ₙ+* S}
  (h : Function.LeftInverse g ⇑f) (x : R), ↑((RingEquiv.ofLeftInverse' h) x) = f x
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mem : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {subS : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : MvPolynomial σ R} {s : subS},
  (∀ i ∈ p.support, f (MvPolynomial.coeff i p) ∈ s) → ∀ {v : σ → S}, (∀ (i : σ), v i ∈ s) → MvPolynomial.eval₂ f v p ∈ s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
/-- Turn a `BoolExpr` into an `Entrypoint`.
 -/
Std.Tactic.BVDecide.BVLogicalExpr.bitblast : Std.Tactic.BVDecide.BVLogicalExpr → Std.Sat.AIG.Entrypoint Std.Tactic.BVDecide.BVBit
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsVerdierRightLocalizingOppositeOpOfIsVerdierLeftLocalizing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [A.IsVerdierLeftLocalizing B], A.op.IsVerdierRightLocalizing B.op
-- Lean.Server.FileWorker.Utils
_private.Lean.Server.FileWorker.Utils.0.Lean.Server.FileWorker.mkCmdSnaps : Lean.Language.Lean.InitialSnapshot → Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot