mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The underlying cocone of a cokernel cofork is mapped to a colimit cocone if and only if
the mapped cokernel cofork is colimit.  -/
CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                (c : CategoryTheory.Limits.CokernelCofork f) →
                  (G : CategoryTheory.Functor C D) →
                    [inst_4 : G.PreservesZeroMorphisms] →
                      CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_multiset_prod : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (s : Multiset (Polynomial R)) (x : S), Polynomial.eval₂ f x s.prod = (Multiset.map (Polynomial.eval₂ f x) s).prod
-- Mathlib.LinearAlgebra.Matrix.Trace
/-- Matrices `A` and `B` are equal iff `(A * x).trace = (B * x).trace` for all `x`.  -/
Matrix.ext_iff_trace_mul_right : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring R]
  {A B : Matrix m n R}, A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff f ∈ nonZeroDivisors R → g ≠ 0 → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_succ : ∀ {x y : NNReal} {n : ℕ}, x.agmSequences y (n + 1) = (NNReal.sqrt (x * y)).agmSequences ((x + y) / 2) n
-- Aesop.Stats.Basic
Aesop.Stats.search : Aesop.Stats → Aesop.Nanos
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.tensorFunc.eq_1 : ∀ (C : Type u),
  CategoryTheory.FreeMonoidalCategory.tensorFunc C =
    {
      obj := fun X =>
        CategoryTheory.Discrete.functor fun n =>
          CategoryTheory.MonoidalCategoryStruct.tensorObj
            (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n }) X,
      map := fun {X Y} f =>
        CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.MonoidalCategoryStruct.whiskerLeft
            (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := x.as }) f,
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- A lifting of a morphism `f : X ⟶ Y` on fibrant resolutions.
(This is functorial only up to homotopy, see `HoCat.resolution`.)  -/
HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        (X ⟶ Y) →
          (HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X ⟶
            HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj Y)
-- Mathlib.Combinatorics.Colex
/-- If `s ⊂ t`, then `s < t` in the colex order. Note the converse does not hold, as inclusion does
not form a linear order.  -/
Finset.Colex.toColex_lt_toColex_of_ssubset : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α}, s ⊂ t → toColex s < toColex t
-- Mathlib.RepresentationTheory.Basic
Representation.smul_one_tprod_asModule : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρW : Representation k G W) (r : MonoidAlgebra k G) (x : V) (y : W),
  (r •
      have this := x ⊗ₜ[k] y;
      this) =
    x ⊗ₜ[k]
      (r •
        have this := y;
        this)
-- Init.Internal.Order.Basic
Lean.Order.fun_csup_is_sup : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CCPO (β x)] (c : ((x : α) → β x) → Prop)
  (hc : Lean.Order.chain c), Lean.Order.is_sup c (Lean.Order.fun_csup c hc)
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Icc_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Icc c d ↔ b ∈ Set.Icc (a - d) (a - c)
-- Mathlib.Topology.Order.OrderClosed
Filter.tendsto_nhds_max_left : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α},
  Filter.Tendsto f l (nhdsWithin a (Set.Ioi a)) → Filter.Tendsto (fun i => max (f i) a) l (nhdsWithin a (Set.Ioi a))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.inter_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S)
  [inst_2 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_3 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))],
  (E.inter F).toPreOneHypercover = E.inter F.toPreOneHypercover
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.lt_iff : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LT α] [inst_2 : LT N] {a b : Lex (α →₀ N)},
  a < b ↔ ∃ i, (∀ j < i, (ofLex a) j = (ofLex b) j) ∧ (ofLex a) i < (ofLex b) i
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H), groupCohomology.mapShortComplexH1 f 0 = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_get_eq : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {k : α} {v : β k} {w : k ∈ m}, m.get k w = v → k ∈ m
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero : ∀ (K : Type u_2) [inst : Field K] {D : WithZero (Multiplicative ℤ)},
  D ≠ 0 → ∀ {f : LaurentSeries K}, Valued.v f ≤ D ↔ ∀ n < -D.log, f.coeff n = 0
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.mk.sizeOf_spec : ∀ (equalMVarIds : Std.HashMap Lean.MVarId Lean.MVarId) (equalLMVarIds : Std.HashMap Lean.LMVarId Lean.LMVarId)
  (leftUnassignedMVarValues rightUnassignedMVarValues : Std.HashMap Lean.MVarId Lean.Expr),
  sizeOf
      { equalMVarIds := equalMVarIds, equalLMVarIds := equalLMVarIds,
        leftUnassignedMVarValues := leftUnassignedMVarValues, rightUnassignedMVarValues := rightUnassignedMVarValues } =
    1 + sizeOf equalMVarIds + sizeOf equalLMVarIds + sizeOf leftUnassignedMVarValues + sizeOf rightUnassignedMVarValues
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.op.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N],
  MulHom.op =
    { toFun := fun f => { toFun := MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop, map_mul' := ⋯ },
      invFun := fun f => { toFun := MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op, map_mul' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturalityₗ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n m' : M}
  (f : m ⟶ m') (X : C) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X))
      ((CategoryTheory.Functor.LaxMonoidal.μ F m' n).app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f n)).app X)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj P Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.inv Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q) h
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.image : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] {s : Set M}, IsLinearSet s → ∀ (f : F), IsLinearSet (⇑f '' s)
-- Init.Data.String.Basic
String.Pos.Raw.utf8SetAux : Char → List Char → String.Pos.Raw → String.Pos.Raw → List Char
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_union_closure_left_eq : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α), M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y)
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- Information about the argument of interest of a structurally recursive function.

The `Expr`s in this data structure expect the fixed parameters to be in scope, but not the other
parameters of the function. This ensures that this data structure makes sense in the other functions
of a mutually recursive group.
 -/
Lean.Elab.Structural.RecArgInfo : Type
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_apply_of : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β} {x : α}, (FreeAddGroup.lift f) (FreeAddGroup.of x) = f x
-- Mathlib.Data.Set.UnionLift
/-- `iUnionLift_binary` is useful for proving that `iUnionLift` is a homomorphism
of algebraic structures when defined on the Union of algebraic subobjects.
For example, it could be used to prove that the lift of a collection
of group homomorphisms on a union of subgroups preserves `*`.  -/
Set.iUnionLift_binary : ∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  (hT' : T = Set.iUnion S),
  Directed (fun x1 x2 => x1 ⊆ x2) S →
    ∀ (op : ↑T → ↑T → ↑T) (opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)),
      (∀ (i : ι) (x y : ↑(S i)), Set.inclusion ⋯ (opi i x y) = op (Set.inclusion ⋯ x) (Set.inclusion ⋯ y)) →
        ∀ (opβ : β → β → β),
          (∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)) →
            ∀ (x y : ↑T),
              Set.iUnionLift S f hf T ⋯ (op x y) = opβ (Set.iUnionLift S f hf T ⋯ x) (Set.iUnionLift S f hf T ⋯ y)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.kind.injEq : ∀ (val val_1 : Lean.SyntaxNodeKind),
  (Lean.Parser.ParserExtension.Entry.kind val = Lean.Parser.ParserExtension.Entry.kind val_1) = (val = val_1)
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_not : ∀ (a : UInt32), (~~~a).toUInt16 = ~~~a.toUInt16
-- Init.Internal.Order.Basic
/-- The “less-or-equal-to” or “approximates” relation is reflexive.  -/
Lean.Order.PartialOrder.rel_refl : ∀ {α : Sort u} [self : Lean.Order.PartialOrder α] {x : α}, Lean.Order.PartialOrder.rel x x
-- Mathlib.Order.RelSeries
/-- Relation series of `r` and nonempty list of `α` satisfying `r`-chain condition bijectively
corresponds to each other.  -/
RelSeries.Equiv : {α : Type u_1} → {r : SetRel α α} → RelSeries r ≃ ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x}
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ofIsClopen.congr_simp : ∀ {X : Type u_5} [inst : TopologicalSpace X] {U U_1 : Set X} (e_U : U = U_1) {inst_1 : (x : X) → Decidable (x ∈ U)}
  [inst_2 : (x : X) → Decidable (x ∈ U_1)] (hU : IsClopen U),
  LocallyConstant.ofIsClopen hU = LocallyConstant.ofIsClopen ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.core_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = (lhs.sub rhs).toPoly_k.beq' p
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelVAdd.le_of_vadd_le_vadd_left : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : VAdd G P} [self : IsOrderedCancelVAdd G P]
  (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_1.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_2 t ×' Lean.Doc.Block.below_1 t
-- Init.Data.Float.Float
/-- Computes the arc tangent (inverse tangent) of `y / x` in radians, in the range `-π`–`π`. The signs
of the arguments determine the quadrant of the result.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atan2`.
 -/
Float.atan2 : Float → Float → Float
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableConstVAdd` if for each `c` the map
`x ↦ c +ᵥ x` is a measurable function.  -/
MeasurableConstVAdd : (M : Type u_2) → (α : Type u_3) → [VAdd M α] → [MeasurableSpace α] → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.toArray → k ∈ t
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.Hom.ext_one_left : ∀ {n : SimplexCategory} (f g : { len := 1 } ⟶ n),
  autoParam ((SimplexCategory.Hom.toOrderHom f) 0 = (SimplexCategory.Hom.toOrderHom g) 0)
      SimplexCategory.Hom.ext_one_left._auto_1 →
    autoParam ((SimplexCategory.Hom.toOrderHom f) 1 = (SimplexCategory.Hom.toOrderHom g) 1)
        SimplexCategory.Hom.ext_one_left._auto_3 →
      f = g
-- Std.Data.HashSet.Raw
/-- Hash sets without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `HashSet`
over `HashSet.Raw`. Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the
module `Std.Data.HashSet.RawLemmas`.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
and an array of buckets, where each bucket is a linked list of keys. The number of buckets
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
avoid expensive copies.

The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
 -/
Std.HashSet.Raw : Type u → Type u
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Version of `LinearIndepOn.insert` that works when the scalars are not a field.  -/
LinearIndepOn.insert' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {s : Set ι} {i : ι},
  LinearIndepOn R v s → (∀ (r : R), r • v i ∈ Submodule.span R (v '' s) → r = 0) → LinearIndepOn R v (insert i s)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.mk.inj : ∀ {binders : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)} {argNames targetNames : Array Lean.Name}
  {targetType : Lean.Term} {binders_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)}
  {argNames_1 targetNames_1 : Array Lean.Name} {targetType_1 : Lean.Term},
  { binders := binders, argNames := argNames, targetNames := targetNames, targetType := targetType } =
      { binders := binders_1, argNames := argNames_1, targetNames := targetNames_1, targetType := targetType_1 } →
    binders = binders_1 ∧ argNames = argNames_1 ∧ targetNames = targetNames_1 ∧ targetType = targetType_1
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.support_vaddAntidiagonal_subset_vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P}
  (hst : ∀ (a : P), (s.vaddAntidiagonal t a).Finite), {a | (Finset.VAddAntidiagonal a ⋯).Nonempty} ⊆ s +ᵥ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.toClass_apply : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (P : W.Point),
  WeierstrassCurve.Affine.Point.toClass P =
    match P with
    | WeierstrassCurve.Affine.Point.zero => 0
    | WeierstrassCurve.Affine.Point.some x y h =>
      (ClassGroup.mk W.FunctionField) (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toArray_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} {f : α → β → Bool},
  t.WF →
    Std.DTreeMap.Raw.Const.toArray (Std.DTreeMap.Raw.filter f t) =
      Array.filter (fun p => f p.1 p.2) (Std.DTreeMap.Raw.Const.toArray t)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂)[k] = m₁[k]
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal_map_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], ↑((Ideal.associatesEquivIsPrincipal R) 1) = 1
-- Mathlib.RingTheory.Ideal.Maps
/-- Special case of the correspondence theorem for isomorphic rings  -/
Ideal.relIsoOfBijective : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : FunLike F R S] → (f : F) → [RingHomClass F R S] → Function.Bijective ⇑f → Ideal S ≃o Ideal R
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k k' : α}, (k == k') = true → m.get? k = m.get? k'
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.surjective_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M}, solution.IsPresentation → Function.Surjective ⇑solution.π
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_2.eq : ∀ {α : Type} {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u}
  {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u}
  (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α))
  (F_1 : (t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
      Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) → Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t)
  (F_4 : (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t),
  Lean.Meta.DiscrTree.Trie.brecOn_2 t F_1 F_2 F_3 F_4 = F_3 t (Lean.Meta.DiscrTree.Trie.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe : ∀ {J : Type w} (f : J → AddCommGrpCat), ↑(AddCommGrpCat.HasLimit.productLimitCone f).cone.pt = ((j : J) → ↑(f j))
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_right_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y * z) → IsCoprime x z
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ico a b).Nonempty ↔ a < b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The bijection
`(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F))`
which is part of the universal property of the sheafification of the presheaf of modules `M₀`,
for any sheaf of modules `F`, see `PresheafOfModules.sheafificationAdjunction`  -/
PresheafOfModules.sheafifyHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          [J.WEqualsLocallyBijective AddCommGrpCat] →
                            {F : SheafOfModules R} →
                              (PresheafOfModules.sheafify α φ ⟶ F) ≃
                                (M₀ ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `degree d < n`.  -/
MvPowerSeries.nat_le_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {n : ℕ},
  (∀ (d : σ →₀ ℕ), Finsupp.degree d < n → (MvPowerSeries.coeff d) f = 0) → ↑n ≤ f.order