mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRicSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Ric.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RicSlice α β)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.mk : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i : ι} → M i → (tail : Monoid.CoprodI.Word M) → tail.fstIdx ≠ some i → Monoid.CoprodI.Word.Pair M i
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.smul_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : A}, x ∈ S → ∀ (r : R), r • x ∈ S
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtTreeSet.ofList l cmp = ∅.insertMany l
-- Init.Data.Nat.Lemmas
Nat.mul_ne_zero : ∀ {n m : ℕ}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.coe_copy : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = ↑p), ↑(p.copy s hs) = s
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instFaithfulPushforward : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Modules.pushforward f).Faithful
-- Mathlib.Analysis.Complex.Norm
Complex.sq_norm_sub_sq_im : ∀ (z : ℂ), ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hom_ext : ∀ {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} {E : L.LeftExtension F}
  (h : E.IsPointwiseLeftKanExtension) {G : L.LeftExtension F} {f₁ f₂ : E ⟶ G}, f₁ = f₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_injective : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Function.Injective ⇑(cfcₙHom ha)
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitorEquivalence_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.leftUnitorEquivalence C).functor = CategoryTheory.prod.leftUnitor C
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.const_smul` -/
AEMeasurable.fun_const_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstSMul M X],
  AEMeasurable g μ → ∀ (c : M), AEMeasurable (fun i => c • g i) μ
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.topology_eq : ∀ (α : Type u_1) (D : Set (Set α)) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsScott α D],
  inst_1 = Topology.scott α D
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.toENNRealVectorMeasure.ennrealToMeasure = μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool} {k : α}, t.WF → (Std.DTreeMap.Raw.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.dExt_iff : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : Module.Baer.ExtensionOf i f},
  a = b ↔
    ∃ (_ : a.domain = b.domain), ∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.beq_eq_beqModel : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Hashable α] [LawfulHashable α] [inst_4 : BEq β]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ =
        Std.Internal.List.Const.beqModel (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
          (Std.DHashMap.Internal.toListModel (↑m₂).buckets)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelZeroIsoTarget_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.cokernelZeroIsoTarget.inv = CategoryTheory.Limits.cokernel.π 0
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.sliceTo_startPos : ∀ {s : String.Slice} {p : s.Pos}, p.sliceTo s.startPos ⋯ = (s.sliceTo p).startPos
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Millisecond.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toMilliseconds : Std.Time.WallTime → Std.Time.Millisecond.Offset
-- Mathlib.SetTheory.Cardinal.Finite
Nat.bijective_iff_injective_and_card : ∀ {α : Type u_1} {β : Type u_2} [Finite β] (f : α → β),
  Function.Bijective f ↔ Function.Injective f ∧ Nat.card α = Nat.card β
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  (a :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))))
  (x : CategoryTheory.Limits.WalkingMulticospan J),
  (I.multiforkEquivPiFork.inverse.obj a).π.app x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left a_1 =>
      CategoryTheory.CategoryStruct.comp a.ι
        (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1)
    | CategoryTheory.Limits.WalkingMulticospan.right a_1 =>
      CategoryTheory.CategoryStruct.comp a.ι
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
            (J.fst a_1))
          (I.fst a_1))
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.mkContinuousOfExistsBound.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f f_1 : E →ₛₗ[σ] F) (e_f : f = f_1) (h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖),
  f.mkContinuousOfExistsBound h = f_1.mkContinuousOfExistsBound ⋯
-- Init.Data.Fin.Lemmas
Fin.coe_mul : ∀ {n : ℕ} (a b : Fin n), ↑(a * b) = ↑a * ↑b % n
-- Mathlib.Order.Bounds.Basic
isLUB_Ioo : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] [DenselyOrdered γ] {a b : γ}, b < a → IsLUB (Set.Ioo b a) a
-- Mathlib.GroupTheory.Index
AddSubgroup.card_map_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (f : G →+ G'),
  Nat.card ↥(AddSubgroup.map f H) ∣ Nat.card ↥H
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_snd : ∀ {𝕜 : 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'] {s : Set (M × M')}, MDiff[s] Prod.snd
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.limitCompYonedaIsoCocone_inv : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (X : C),
  (CategoryTheory.Limits.limitCompYonedaIsoCocone F X).inv =
    TypeCat.ofHom fun t =>
      (CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.limit.lift (F.op.comp (CategoryTheory.yoneda.obj X))
            (CategoryTheory.Limits.Types.coneOfSection ⋯)))
        PUnit.unit
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn?.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β), List.minIdxOn? f [] = none
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.IntegrationParams.Riemann.eq_1 : BoxIntegral.IntegrationParams.Riemann = { bRiemann := true, bHenstock := true, bDistortion := false }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X_1).hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).hom
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.isIrreducible : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.IrreducibleCloseds α), IsIrreducible ↑s
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.id_apply : ∀ (R : Type u_1) {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜] (x : A),
  (GradedAlgHom.id R 𝒜) x = x
-- Mathlib.Analysis.BoxIntegral.Basic
/-- Suppose that there exists a nonnegative box-additive function `B` with the following property.

For every `c : ℝ≥0`, a point `x ∈ I.Icc`, and a positive `ε` there exists `δ > 0` such that for any
box `J ≤ I` such that

- `J.Icc ⊆ Metric.closedBall x δ`;
- if `l.bDistortion` (i.e., `l = ⊥`), then the distortion of `J` is less than or equal to `c`,

the distance between the term `vol J (f x)` of an integral sum corresponding to `J` and `g J` is
less than or equal to `ε * B J`.

Then `f` is McShane integrable on `I` with integral `g I`.  -/
BoxIntegral.HasIntegral.mcShane_of_forall_isLittleO : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (B : BoxIntegral.BoxAdditiveMap ι ℝ ↑I),
  (∀ (J : BoxIntegral.Box ι), 0 ≤ B J) →
    ∀ (g : BoxIntegral.BoxAdditiveMap ι F ↑I),
      (∀ (x : NNReal),
          ∀ x ∈ BoxIntegral.Box.Icc I,
            ∀ ε > 0,
              ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J) →
        BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.McShane f vol (g I)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddGroupUniformFun : {α : Type u_1} → {β : Type u_2} → [AddGroup β] → AddGroup (UniformFun α β)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Lean.Elab.Task
/-- Given a monadic value in `TermElabM`, creates a task that runs it in the current state,
returning a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Elab.Term.TermElabM.asTask' : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM (Task (Lean.Elab.TermElabM α))
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_eq_zero_iff : ∀ {K : Type u_2} [inst : Field K] {f g : Polynomial K}, f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : F.rightDerived 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom
      (CategoryTheory.CategoryStruct.comp F.toRightDerivedZero h) =
    h
-- Mathlib.Topology.Order.ScottTopology
TopologicalSpace.mk.congr_simp : ∀ {X : Type u} (IsOpen IsOpen_1 : Set X → Prop) (e_IsOpen : IsOpen = IsOpen_1) (isOpen_univ : IsOpen Set.univ)
  (isOpen_inter : ∀ (s t : Set X), IsOpen s → IsOpen t → IsOpen (s ∩ t))
  (isOpen_sUnion : ∀ (s : Set (Set X)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)),
  { IsOpen := IsOpen, isOpen_univ := isOpen_univ, isOpen_inter := isOpen_inter, isOpen_sUnion := isOpen_sUnion } =
    { IsOpen := IsOpen_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
-- Mathlib.Order.InitialSeg
PrincipalSeg.mem_range_of_rel_top : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) {b : β},
  s b f.top → b ∈ Set.range ⇑f.toRelEmbedding
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.evalEquiv_apply : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u)
  (s : S.obj (Opposite.op α)), (CategoryTheory.evalEquiv S hs α) s = CategoryTheory.eval S α s
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_of_mem_tangentsFrom : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P} {p : P},
  as ∈ s.tangentsFrom p → p ∈ as
-- Mathlib.Tactic.Linter.TextBased
/-- All text-based linters registered in this file.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.allLinters : Array Mathlib.Linter.TextBased.TextbasedLinter✝
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.mk : Bool → Lean.Lsp.TextDocumentSyncKind → Bool → Bool → Option Lean.Lsp.SaveOptions → Lean.Lsp.TextDocumentSyncOptions
-- Mathlib.Order.Atoms
/-- **Alias** of the forward direction of `isCoatom_compl`. -/
IsCoatom.of_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsCoatom aᶜ → IsAtom a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_Inv_of_Inv : ∀ {w : ℕ} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig input.cache →
    Std.Tactic.BVDecide.BVExpr.Cache.Inv assign (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig
      (Std.Tactic.BVDecide.BVExpr.bitblast aig input).cache
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.snd : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {x : α × β}, IsOfFinOrder x → IsOfFinOrder x.2
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote : Int.Internal.Linear.Context → Int.Internal.Linear.Expr → ℤ
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- If `A` is graded by a canonically ordered additive monoid, then the projection map `x ↦ x₀`
is a ring homomorphism.
 -/
GradedRing.projZeroRingHom : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddCommMonoid ι] →
            [inst_3 : PartialOrder ι] →
              [CanonicallyOrderedAdd ι] →
                [inst_5 : SetLike σ A] → [inst_6 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [GradedRing 𝒜] → A →+* A
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_factors : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X),
  CategoryTheory.CategoryStruct.comp h f = 0 → (CategoryTheory.Limits.kernelSubobject f).Factors h
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprodEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] [inst_3 : DecidableEq ι],
  AddMonoidHom.noncommPiCoprodEquiv =
    { toFun := fun ϕ => AddMonoidHom.noncommPiCoprod ↑ϕ ⋯,
      invFun := fun f => ⟨fun i => f.comp (AddMonoidHom.single N i), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₁_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] {i₁ i₁' : ι₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
      HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
        (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) •
          CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃))
            (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.mk.injEq : ∀ (toContext : Lean.Elab.Tactic.Context) (ctx : Lean.Meta.Grind.Context) (sctx : Lean.Meta.Sym.Context)
  (methods : Lean.Meta.Grind.Methods) (params : Lean.Meta.Grind.Params) (sym : Bool)
  (toContext_1 : Lean.Elab.Tactic.Context) (ctx_1 : Lean.Meta.Grind.Context) (sctx_1 : Lean.Meta.Sym.Context)
  (methods_1 : Lean.Meta.Grind.Methods) (params_1 : Lean.Meta.Grind.Params) (sym_1 : Bool),
  ({ toContext := toContext, ctx := ctx, sctx := sctx, methods := methods, params := params, sym := sym } =
      { toContext := toContext_1, ctx := ctx_1, sctx := sctx_1, methods := methods_1, params := params_1,
        sym := sym_1 }) =
    (toContext = toContext_1 ∧ ctx = ctx_1 ∧ sctx = sctx_1 ∧ methods = methods_1 ∧ params = params_1 ∧ sym = sym_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match hkky : compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLED k r (ky, y)
      | Ordering.eq => (ky, y)
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryLE k l ⋯ ⋯
-- Mathlib.Algebra.Module.ZLattice.Basic
instDiscreteTopologySubtypeMemSubmoduleIntComap : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  [DiscreteTopology ↥L] (e : F ≃L[K] E), DiscreteTopology ↥(ZLattice.comap K L ↑↑e)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.ramifiedPlacesOver.eq_1 : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.ramifiedPlacesOver L v = {w | w.LiesOver v ∧ NumberField.InfinitePlace.IsRamified K w}
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace_div : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (f : Module.End K V)
  (a b : K), b ≠ 0 → f.eigenspace (a / b) = LinearMap.ker (b • f - (algebraMap K (Module.End K V)) a)
-- Mathlib.LinearAlgebra.Lagrange
/-- Two polynomials, with the same degree and leading coefficient, which have the same evaluation
on a set of distinct values with cardinality equal to the degree, are equal.
 -/
Polynomial.eq_of_degree_le_of_eval_finset_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R),
  f.degree ≤ ↑s.card →
    f.degree = g.degree → f.leadingCoeff = g.leadingCoeff → (∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) → f = g
-- Lean.Level
Lean.LevelMVarId.mk.inj : ∀ {name name_1 : Lean.Name}, { name := name } = { name := name_1 } → name = name_1
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.ExtTreeSet.getGED : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α → α