mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.auxEquiv_mul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ),
  (GradedTensorProduct.auxEquiv R 𝒜 ℬ) (x * y) =
    ((TensorProduct.gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x))
      ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) y)
-- Mathlib.Analysis.Convex.PartitionOfUnity
/-- Let `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be
a topological real vector space. Let `t : X → Set E` be a family of convex sets. Suppose that for
each point `x : X`, there exists a neighborhood `U ∈ 𝓝 X` and a function `g : X → E` that is
continuous on `U` and sends each `y ∈ U` to a point of `t y`. Then there exists a continuous map
`g : C(X, E)` such that `g x ∈ t x` for all `x`. See also
`exists_continuous_forall_mem_convex_of_local_const`.  -/
exists_continuous_forall_mem_convex_of_local : ∀ {X : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [NormalSpace X] [ParacompactSpace X] [inst_5 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
  {t : X → Set E},
  (∀ (x : X), Convex ℝ (t x)) →
    (∀ (x : X), ∃ U ∈ nhds x, ∃ g, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y) → ∃ g, ∀ (x : X), g x ∈ t x
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instSup : Max ℚ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_sum : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → AddMonoidAlgebra R ℕ),
  { toFinsupp := ∑ i ∈ s, f i } = ∑ i ∈ s, { toFinsupp := f i }
-- Init.Data.String.Basic
String.Slice.Pos.prevAuxGo_le_self : ∀ {s : String.Slice} {p : ℕ} {h : p < s.utf8ByteSize}, String.Slice.Pos.prevAux.go p h ≤ { byteIdx := p }
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.mk : {α : Type u} → Option α → α → Std.Rxo.Iterator α
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mdifferentiableAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → s ∈ nhds x → MDiffAt f x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instNegHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → Neg (M₁ ⟶ M₂)
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_ne_zero_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [IsDomain R] [IsDomain S]
  [Module.Free R S] [Module.Finite R S] {x : S}, (Algebra.norm R) x ≠ 0 ↔ x ≠ 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey.mk.injEq : ∀ (constName constName_1 : Lean.Name),
  ({ constName := constName } = { constName := constName_1 }) = (constName = constName_1)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.topology_eq_upperTopology : ∀ {α : Type u_3} {t : TopologicalSpace α} {inst : Preorder α} [self : Topology.IsUpper α], t = Topology.upper α
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The functor `pointwiseLeftKanExtension L F` is a left Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.pointwiseLeftKanExtensionIsUniversal : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] →
                  CategoryTheory.StructuredArrow.IsUniversal
                    (CategoryTheory.Functor.LeftExtension.mk (L.pointwiseLeftKanExtension F)
                      (L.pointwiseLeftKanExtensionUnit F))
-- Mathlib.Order.Fin.Basic
Fin.coe_max : ∀ {n : ℕ} (a b : Fin n), ↑(max a b) = max ↑a ↑b
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.preservesLimitsOfShape_eq_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_3 : Small.{w, u'} J],
  CategoryTheory.ObjectProperty.preservesLimitsOfShape J =
    (⨆ F, CategoryTheory.MorphismProperty.ofHoms (CategoryTheory.Presheaf.preservesLimitHomFamily F)).isLocal
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multiequalizer of `I : MulticospanIndex J C`.  -/
CategoryTheory.Limits.multiequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) → [CategoryTheory.Limits.HasMultiequalizer I] → C
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuous_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  {X Y : CategoryTheory.Sheaf K A} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuous A J K).map f).hom.app X_1 = f.hom.app (Opposite.op (F.obj (Opposite.unop X_1)))
-- Mathlib.CategoryTheory.Galois.Basic
/-- An object is initial if and only if its fiber is empty.  -/
CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty (F.obj X).obj
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_sum : ∀ {ι : Type u} (f : ι → Cardinal.{v}),
  Cardinal.lift.{w, max v u} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w, v} (f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep.eq_2 : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x_1 y : R) (h : W'.Nonsingular x_1 y),
  (WeierstrassCurve.Affine.Point.some x_1 y h).xRep = ![x_1, 1]
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.of_eq_top : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P = ⊤ → ∀ {X Y : C} (f : X ⟶ Y), P f
-- Mathlib.Algebra.Ring.Parity
Nat.div_two_mul_two_add_one_of_odd : ∀ {n : ℕ}, Odd n → n / 2 * 2 + 1 = n
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_inv_mul_self_nhdsGE : ∀ {E : Type u_4} [inst : SeminormedGroup E] (x : E),
  Filter.Tendsto (fun a => ‖a⁻¹ * x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_triangle : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E] [StarOrderedRing A] (x y : E),
  ‖x + y‖ ≤ ‖x‖ + ‖y‖
-- Init.Data.String.FindPos
/-- Obtains the smallest valid position that is greater than or equal to the given byte position.
 -/
String.Slice.posGE : (s : String.Slice) → (offset : String.Pos.Raw) → offset ≤ s.rawEndPos → s.Pos
-- Mathlib.Order.SuccPred.Tree
/-- A subtree is represented by its root, therefore this is a type synonym.
 -/
SubRootedTree : RootedTree → Type u_2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P ≈ Q → W'.add P Q = W'.dblXYZ P
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism of additive module objects.  -/
CategoryTheory.AddMod.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] → CategoryTheory.AddMod D A → CategoryTheory.AddMod D A → Type v₂
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.FirstObj.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C}
  {R : CategoryTheory.Presieve X} (z₁ z₂ : CategoryTheory.Equalizer.FirstObj P R),
  (∀ (Y : C) (f : Y ⟶ X) (hf : R f),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩))
          z₂) →
    z₁ = z₂
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.PreservesInjectiveObjects.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X : C}, CategoryTheory.Injective X → CategoryTheory.Injective (F.obj X)) → F.PreservesInjectiveObjects
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The colimit of `F ⋙ forget₂ CommRingCat RingCat` in the category `RingCat`.
In the following, we will show that this has the structure of a _commutative_ ring.
 -/
CommRingCat.FilteredColimits.R : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommRingCat → RingCat
-- Mathlib.Algebra.Notation.Support
Function.support_fun_curry : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Zero M] (f : ι × κ → M),
  (Function.support fun i j => f (i, j)) = Prod.fst '' Function.support f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ),
  (FreeGroup.freeGroupCongr e).trans (FreeGroup.freeGroupCongr f) = FreeGroup.freeGroupCongr (e.trans f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.deriv_cosh : deriv Complex.cosh = Complex.sinh
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.contains_char_eq : ∀ {c : Char} {s : String}, s.contains c = decide (c ∈ s.toList)
-- Lean.Meta.Tactic.Simp.Rewrite
/-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates.  -/
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.rewriteUsingIndex? : Lean.Expr →
  Lean.Meta.SimpTheoremTree →
    Lean.PHashSet Lean.Meta.Origin → String → Bool → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Lean.ExtraModUses
Lean.IndirectModUse.kind : Lean.IndirectModUse → String
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The composition of an open partial homeomorphism from `H` to `M` and its inverse belongs to
the `C^n` groupoid.  -/
symm_trans_mem_contDiffGroupoid : ∀ {n : WithTop ℕ∞} {𝕜 : 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] (e : OpenPartialHomeomorph M H), e.symm.trans e ∈ contDiffGroupoid n I
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- The product over `univ` of a sum can be written as a sum over the product of sets,
`Fintype.piFinset`. `Finset.prod_sum` is an alternative statement when the product is not
over `univ`.  -/
Finset.prod_univ_sum : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {κ : ι → Type u_5} [inst_2 : Fintype ι]
  (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R), ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ Fintype.piFinset t, ∏ i, f i (x i)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.setLIntegral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ]
  {f : α × β → StieltjesFunction ℝ},
  ProbabilityTheory.IsCondKernelCDF f κ ν →
    ∀ (a : α) {s : Set β},
      MeasurableSet s → ∀ (x : ℝ), ∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Set.Iic x)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma : ∀ (N M : ℤ), N ∣ M → ModularGroup.T ^ M ∈ CongruenceSubgroup.Gamma N.natAbs
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.mk.inj : ∀ {parents parents_1 : List Lean.Expr}, { parents := parents } = { parents := parents_1 } → parents = parents_1
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_germ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type u_2} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [inst_3 : CategoryTheory.ConcreteCategory C FC] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X)
  (hx : x ∈ U) (f : F ⟶ G) (s : CC (F.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))
      ((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) =
    (CategoryTheory.ConcreteCategory.hom (G.germ U x hx))
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) s)
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Icc a b) = Set.Icc a b
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_reflectionPerm_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainTopCoeff i ((P.reflectionPerm j) j) = RootPairing.chainBotCoeff i j
-- Mathlib.Control.ULift
ULift.instLawfulFunctor_mathlib : LawfulFunctor ULift.{u_2, u_1}
-- Mathlib.Tactic.Linarith.Preprocessing
/-- If `h` is an equality or inequality between NNReals, `nnrealToReal` lifts this inequality to the
Reals. It also adds the facts that the reals involved are nonnegative. To avoid adding the same
nonnegativity facts many times, it is a global preprocessor. This preprocessor does nothing unless
`Mathlib.Tactic.Linarith.NNRealPreprocessor` is imported  -/
Mathlib.Tactic.Linarith.nnrealToReal : Mathlib.Tactic.Linarith.GlobalPreprocessor
-- Mathlib.Topology.Instances.Real.Lemmas
/-- The limit of an antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` is a least
upper bound of the sequence.  -/
Real.isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici : ∀ {f : ℕ → ℝ} {k : ℕ} {x : ℝ},
  Filter.Tendsto f Filter.atTop (nhds x) →
    MonotoneOn f (Set.Ici k) → BddAbove (f '' Set.Ici k) → IsLUB (f '' Set.Ici k) x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The short complex which expresses `X.opcycles` as the cokernel of `X.δ`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles : {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] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (n₀ n₁ : ℤ) →
                    autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1 →
                      CategoryTheory.ShortComplex C
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.cast_apply : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_14} {M : ι → Type u_15} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {i j : ι} (h : i = j) (a : M i), (LinearEquiv.cast h) a = cast ⋯ a
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.all.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n.succ → Bool), n.succ.all f = ((n.all fun i h => f i ⋯) && f n ⋯)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle.hcongr_7 : ∀ (ι ι' : Type u_1),
  ι = ι' →
    ∀ (M : ι → Type u_6) (M' : ι' → Type u_6),
      M ≍ M' →
        ∀ (inst : (i : ι) → One (M i)) (inst' : (i : ι') → One (M' i)),
          inst ≍ inst' →
            ∀ (inst_1 : DecidableEq ι) (inst'_1 : DecidableEq ι'),
              inst_1 ≍ inst'_1 →
                ∀ (i : ι) (i' : ι'),
                  i ≍ i' →
                    ∀ (x : M i) (x' : M' i'),
                      x ≍ x' → ∀ (j : ι) (j' : ι'), j ≍ j' → Pi.mulSingle i x j ≍ Pi.mulSingle i' x' j'
-- Mathlib.Topology.MetricSpace.Gluing
/-- Mapping each `X n` to the inductive limit.  -/
Metric.toInductiveLimit : {X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    {f : (n : ℕ) → X n → X (n + 1)} → (I : ∀ (n : ℕ), Isometry (f n)) → (n : ℕ) → X n → Metric.InductiveLimit I
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.insert k m p =
    bif k == 0 then p
    else bif m == Lean.Grind.CommRing.Mon.unit then p.addConst k else Lean.Grind.CommRing.Poly.insert.go k m p
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_maxKey_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} (hc : Std.Internal.List.containsKey k l = true), (compare k (Std.Internal.List.maxKey l ⋯)).isLE = true
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.arg : Lean.Meta.Grind.CanonArgKey → Lean.Expr
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk'_X_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0),
  (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 0 = X₀
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp.eq_1 : ∀ (n : ℕ),
  UInt16.ofNatClamp n =
    if h : n < UInt16.size then UInt16.ofNatLT n h else UInt16.ofNatLT (UInt16.size - 1) UInt16.ofNatClamp._proof_1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_vaddConst : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] {p : P₁}, ↑(ContinuousAffineEquiv.vaddConst k p) = AffineEquiv.vaddConst k p
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.writingBodyFixed.inj : ∀ {n n_1 : ℕ},
  Std.Http.Protocol.H1.Writer.State.writingBodyFixed n = Std.Http.Protocol.H1.Writer.State.writingBodyFixed n_1 →
    n = n_1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.bdd_at_cusps : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : ModularFormClass F Γ k] (f : F) {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt (⇑f) k
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_of_not_isPrime`. -/
Ideal.inertiaDeg'_of_not_isPrime : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S],
  ¬q.IsPrime → q.inertiaDeg R = 0
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.addCommMonoid : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → AddCommMonoid ↥p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  t.isEmpty = true → t.get! a = default
-- Mathlib.Data.List.MinMax
List.foldr_min_of_ne_nil : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] {l : List α}, l ≠ [] → ↑(List.foldr min ⊤ l) = l.minimum
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (W : C)
  (k : (a : J.L) → W ⟶ I.left a)
  (h :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b))
  (a : J.L),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h)
      (CategoryTheory.Limits.Multiequalizer.ι I a) =
    k a
-- Mathlib.RingTheory.Perfection
Perfection.ext_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f g : Perfection R p},
  f = g ↔ ∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_pos : ∀ (x : ℤ) (m : ℕ), x % ↑m < (↑m + 1) / 2 → x.bmod m = x % ↑m
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Topology.IsInducing.withSeminorms : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] [inst_7 : TopologicalSpace F]
  {q : SeminormFamily 𝕜₂ F ι},
  WithSeminorms q →
    ∀ [inst_8 : TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F}, Topology.IsInducing ⇑f → WithSeminorms (q.comp f)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_algebraMap : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {r : ℝ},
  CFC.log ((algebraMap ℝ A) r) = (algebraMap ℝ A) (Real.log r)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Replacing a set by its closure does not change the Hausdorff edistance.  -/
Metric.hausdorffEDist_closure_right : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist s (closure t) = Metric.hausdorffEDist s t
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_prod_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α) (b : β),
  Set.Ici a ×ˢ Set.Ici b = Set.Ici (a, b)
-- Mathlib.Data.TwoPointing
TwoPointing.mk : {α : Type u_3} → (toProd : α × α) → toProd.1 ≠ toProd.2 → TwoPointing α
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_core : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_of_core_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = Int.Internal.Linear.Poly.denote' ctx p₂ →
      Int.Internal.Linear.Poly.denote' ctx p₃ = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F},
  WeierstrassCurve.Projective.Point.toAffine W ![0, 1, 0] = 0