mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given a one-preserving morphism `f`,
`f⁻¹` is the one-preserving morphism sending `x` to `(f x)⁻¹`.  -/
OneHom.instInv : {M : Type u_2} → {N : Type u_3} → [inst : One M] → [inst_1 : InvOneClass N] → Inv (OneHom M N)
-- Std.Http.Data.Headers.Name
/-- Standard User-Agent header name
 -/
Std.Http.Header.Name.userAgent : Std.Http.Header.Name
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
LinearMap.compMultilinearMap.eq_1 : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂),
  g.compMultilinearMap f = { toFun := ⇑g ∘ ⇑f, map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Ioc : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.Ioc i j = Set.Ioc ↑i ↑j
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimitsOfShape.of_essentiallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.EssentiallySmall.{u₁, v₂, u₂} J]
  [CategoryTheory.LocallySmall.{v₁, v₂, u₂} J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Init.Data.Array.Count
Array.count_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, Array.count a #[b] = if (b == a) = true then 1 else 0
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instStarModule : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing 𝕜]
  [inst_6 : StarRing A] [inst_7 : StarModule 𝕜 A] [inst_8 : NormedStarGroup A], StarModule 𝕜 (DoubleCentralizer 𝕜 A)
-- Init.Data.Vector.Lex
Vector.le_refl : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [i₀ : Std.Irrefl fun x1 x2 => x1 < x2] (xs : Vector α n), xs ≤ xs
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_zero : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {N : ι}, MeasureTheory.lowerCrossingTime a b f N 0 = MeasureTheory.hittingBtwn f (Set.Iic a) ⊥ N
-- Mathlib.Order.SuccPred.Basic
Order.succ_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a b : α),
  Order.succ (max a b) = max (Order.succ a) (Order.succ b)
-- Mathlib.GroupTheory.PGroup
/-- If `G` is a `p`-group acting on a finite set `α`, then the number of fixed points
of the action is congruent mod `p` to the cardinality of `α`  -/
IsPGroup.card_modEq_card_fixedPoints : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] (α : Type u_2) [inst_1 : MulAction G α] [Finite α],
      Nat.card α ≡ Nat.card ↑(MulAction.fixedPoints G α) [MOD p]
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  ¬MeasurableSet i → v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i
-- Mathlib.Topology.LocallyFinite
LocallyFinite.eventually_smallSets : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → ∀ (x : X), ∀ᶠ (s : Set X) in (nhds x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_3 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Tactic.GRewrite.Core
/-- The rewrite lemma has unified with something.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matched : Mathlib.Tactic.GRewrite.Progress✝
-- Mathlib.Order.Hom.Basic
OrderIso.map_bot' : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] (f : α ≃o β) {x : α} {y : β},
  (∀ (x' : α), x ≤ x') → (∀ (y' : β), y ≤ y') → f x = y
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. This version
only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`.  -/
HasDerivAt.le_of_lip' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x₀ : 𝕜},
  HasDerivAt f f' x₀ → ∀ {C : ℝ}, 0 ≤ C → (∀ᶠ (x : 𝕜) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖f'‖ ≤ C
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ext : ∀ {n : ℕ} {x y : Composition n}, x.blocks = y.blocks → x = y
-- Mathlib.Data.Prod.Basic
Function.LeftInverse.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ},
  Function.LeftInverse f₁ f₂ → Function.LeftInverse g₁ g₂ → Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
-- Batteries.Data.List.Basic
List.zipWithLeft'.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.zipWithLeft' f (a :: as) (b :: bs) =
    (f a (some b) :: (List.zipWithLeft' f as bs).1, (List.zipWithLeft' f as bs).2)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying type.  -/
CommGrpCat.carrier : CommGrpCat → Type u
-- Std.Data.DTreeMap.Internal.Balancing
/-- A double right rotation.  -/
Std.DTreeMap.Internal.Impl.doubleR : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (lk : α) →
          β lk →
            Std.DTreeMap.Internal.Impl α β →
              (lrk : α) →
                β lrk →
                  Std.DTreeMap.Internal.Impl α β →
                    Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndepOn_singleton_iff : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] {v : ι → M} {i : ι}, LinearIndepOn R v {i} ↔ v i ≠ 0
-- Mathlib.SetTheory.ZFC.PSet
PSet.instSep : Sep PSet.{u_1} PSet.{u_1}
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{max u u_1, u, u} k K} {B : Rep.{max u u_1, u, u} k H} {C : Rep.{max u u_1, u, u} k G} (f : H →* K)
  (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)}
  (h : groupCohomology.shortComplexH1 C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 g ψ) h)
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent_map_mem : ∀ {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module A M₁] [inst_4 : Module A M₂] (φ : M₁ →ₗ[A] M₂)
  (c : ↥(Ideal.primaryComponent M₁ I)), φ ↑c ∈ Ideal.primaryComponent M₂ I
-- Mathlib.Data.Finset.Basic
Equiv.piCongrLeft.eq_1 : ∀ {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β), Equiv.piCongrLeft P e = (Equiv.piCongrLeft' P e.symm).symm
-- Mathlib.RepresentationTheory.Action
/-- This a type-changing equivalence to avoid abusing defeq.  -/
Representation.linearizeOfMulActionIso : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (H : Type w) →
          [inst_2 : MulAction G H] →
            (Representation.linearize k G (Action.ofMulAction G H)).Equiv (Representation.ofMulAction k G H)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.functoriality`.

---

A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially.  -/
CategoryTheory.Limits.Cones.functoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (G : CategoryTheory.Functor C D) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (F.comp G))
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk''_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
      CategoryTheory.Grp.homMk''._auto_1)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
          CategoryTheory.MonObj.mul)
      CategoryTheory.Grp.homMk''._auto_3),
  (CategoryTheory.Grp.homMk'' f one_f mul_f).hom.hom = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_negPolynomial : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S),
  (W'.map f).negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W'.negPolynomial
-- Mathlib.Analysis.Normed.Lp.Finsupp
/-- The L^1 metric on `ι`-many copies of a metric space `X`  -/
Finsupp.instMetricSpaceWithLpOfNNReal : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : Zero X] → {p : NNReal} → [Fact (1 ≤ p)] → [MetricSpace X] → MetricSpace (WithLp (↑p) (ι →₀ X))
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_two_mul : ∀ {n a b n' a' b' : ℕ},
  Mathlib.Meta.NormNum.IsFibAux n a b →
    2 * n = n' → a * (2 * b - a) = a' → a * a + b * b = b' → Mathlib.Meta.NormNum.IsFibAux n' a' b'
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_subset_sym2_iff : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, G.edgeSet ⊆ s.sym2 ↔ G.support ⊆ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey?.get ⋯ = kmi → (compare k kmi).isLE = true
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.locallyOfFinitePresentation_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyOfFinitePresentation f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation
-- Mathlib.Data.Set.Card
Set.ncard_eq_zero : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.ncard_eq_zero._auto_1 → (s.ncard = 0 ↔ s = ∅)
-- Batteries.Data.List.Basic
List.any.eq_def : ∀ {α : Type u} (x : List α) (x_1 : α → Bool),
  x.any x_1 =
    match x, x_1 with
    | [], x => false
    | h :: t, p => p h || t.any p
-- Init.Core
Sum.inl.injEq : ∀ {α : Type u} {β : Type v} (val val_1 : α), (Sum.inl val = Sum.inl val_1) = (val = val_1)
-- Init.MetaTypes
Lean.instInhabitedNameGenerator : Inhabited Lean.NameGenerator
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.instCommSemigroup.eq_1 : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : IsMulCommutative M],
  IsMulCommutative.instCommSemigroup = { toSemigroup := inst, mul_comm := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.comp_assoc : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {Y : Type u_4} {G : SimpleGraph V} {G' : SimpleGraph W}
  {G'' : SimpleGraph X} {G''' : SimpleGraph Y} (f : G'' ↪g G''') (g : G' ↪g G'') (h : G ↪g G'),
  f.comp (g.comp h) = (f.comp g).comp h
-- Mathlib.Algebra.Homology.Opposite
/-- Given a category of complexes with objects in `Vᵒᵖ`, there is a natural equivalence between its
opposite category and a category of complexes with objects in `V`.  -/
HomologicalComplex.unopEquivalence : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≌ HomologicalComplex V c.symm
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioi_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Ioi a = Set.Iio (a / c)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.eq_top_iff' : ∀ {R : Type u} [inst : NonAssocRing R] (A : Subring R), A = ⊤ ↔ ∀ (x : R), x ∈ A
-- Init.Data.Slice.List.Basic
/-- Returns a slice of a list with the given lower bound.

If `start` is not a valid bound for a sublist, then they are clamped to the list's length.

This function is linear in `start` because it stores `as.drop start` in the slice.
 -/
List.toUnboundedSlice : {α : Type u} → List α → ℕ → ListSlice α
-- Mathlib.Algebra.DirectSum.Ring
/-- The `NonUnitalNonAssocSemiring` structure on the grade zero part
of a `GNonUnitalNonAssocSemiring`.  -/
DirectSum.instNonUnitalNonAssocSemiringOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : AddZeroClass ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [DirectSum.GNonUnitalNonAssocSemiring A] → NonUnitalNonAssocSemiring (A 0)
-- Mathlib.Order.Category.Semilat
SemilatSupCat.instLargeCategory : CategoryTheory.LargeCategory SemilatSupCat
-- Init.Data.List.Lemmas
List.mem_iff_getElem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ i, ∃ (h : i < l.length), l[i] = a
-- Init.Data.BitVec.Lemmas
BitVec.toInt_intCast : ∀ {w : ℕ} (x : ℤ), (↑x).toInt = x.bmod (2 ^ w)
-- Mathlib.RingTheory.Kaehler.Basic
/-- The quotient map `I → Ω[S⁄R]` with `I` being the kernel of `S ⊗[R] S → S`.  -/
KaehlerDifferential.fromIdeal : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → ↥(KaehlerDifferential.ideal R S) →ₗ[TensorProduct R S S] Ω[S⁄R]
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_and : ∀ (a b : UInt8), (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
-- Mathlib.Tactic.Ring.Basic
/-- `lift` is an injective function  -/
Mathlib.Tactic.Ring.CSLift.inj : ∀ {α : Type u} {β : outParam (Type u)} [self : Mathlib.Tactic.Ring.CSLift α β],
  Function.Injective Mathlib.Tactic.Ring.CSLift.lift
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubalgebra.unitization_injective : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Field R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S),
  1 ∉ s → Function.Injective ⇑(NonUnitalSubalgebra.unitization s)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : MeasureTheory.MeasureSpace X]
  [MeasureTheory.volume.IsOpenPosMeasure] [inst_3 : TopologicalSpace Y] [inst_4 : MeasureTheory.MeasureSpace Y]
  [MeasureTheory.volume.IsOpenPosMeasure] [MeasureTheory.SFinite MeasureTheory.volume],
  MeasureTheory.volume.IsOpenPosMeasure
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_of_finite_type : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  (∀ (t : Set ι), t.Finite → AlgebraicIndependent R fun i => x ↑i) → AlgebraicIndependent R x
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology : ∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite} {s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))},
  CategoryTheory.Sieve.generate (U.presieveOfSections s) ∈
      (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X) U ↔
    Ideal.span s = ⊤
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsLocallyNoetherian X]
  [AlgebraicGeometry.LocallyOfFiniteType g], AlgebraicGeometry.IsLocallyNoetherian (CategoryTheory.Limits.pullback f g)
-- Mathlib.Algebra.Ring.Rat
Rat.natCast_eq_divInt : ∀ (n : ℕ), ↑n = Rat.divInt (↑n) 1
-- Init.Data.OfScientific
/-- Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite
floating-point value if the range of `Float` is exceeded.
 -/
Float.ofNat : ℕ → Float
-- Init.Data.Dyadic.Round
Dyadic.precision_roundUp : ∀ {x : Dyadic} {prec : ℤ}, (x.roundUp prec).precision ≤ some prec
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.isoForkOfι_inv_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g),
  c.isoForkOfι.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Order.Basic
Decidable.eq_iff_ge_not_gt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], a = b ↔ b ≤ a ∧ ¬b < a
-- Init.Data.Vector.Zip
Vector.zipWith_foldl_eq_zip_foldl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {n : ℕ} {as : Vector α n} {bs : Vector β n}
  {g : δ → γ → δ} {f : α → β → γ} {i : δ},
  Vector.foldl g i (Vector.zipWith f as bs) = Vector.foldl (fun r p => g r (f p.1 p.2)) i (as.zip bs)
-- Mathlib.Algebra.Group.Center
Set.addCenter_subset_addCentralizer : ∀ {M : Type u_1} [inst : Add M] (S : Set M), Set.addCenter M ⊆ S.addCentralizer
-- Mathlib.Data.ULift
ULift.down_bijective : ∀ {α : Type u}, Function.Bijective ULift.down
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits an infimum.  -/
BooleanSubalgebra.instInfCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → Min ↥L
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instSubQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → Sub (Lean.Grind.Ring.OfSemiring.Q α)
-- Init.Data.SInt.Lemmas
ISize.le_or_lt : ∀ (a b : ISize), a ≤ b ∨ b < a
-- Aesop.Forward.State
/-- Get the `InstMap` associated with a variable.  -/
Aesop.VariableMap.find? : Aesop.VariableMap → Aesop.PremiseIndex → Option Aesop.InstMap
-- Std.Data.ExtDTreeMap.Lemmas
/-- Variant of `get?_map` that holds without `LawfulEqCmp`.  -/
Std.ExtDTreeMap.Const.get?_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.map f t) k =
    Option.pmap (fun v h' => f (t.getKey k h') v) (Std.ExtDTreeMap.Const.get? t k) ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mk.sizeOf_spec : ∀ (ω₁ ω₂ : ℂ) (indep : LinearIndependent ℝ ![ω₁, ω₂]),
  sizeOf { ω₁ := ω₁, ω₂ := ω₂, indep := indep } = 1 + sizeOf ω₁ + sizeOf ω₂
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.coe_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective DFunLike.coe
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.keys_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯))
        t.keys.attach).unattach
-- Mathlib.Algebra.AddConstMap.Equiv
/-- An `AddConstMap` satisfies `f (x + a) = f x + b`. Use `map_add_const` instead.  -/
AddConstEquiv.map_add_const' : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (self : AddConstEquiv G H a b) (x : G),
  self.toFun (x + a) = self.toFun x + b
-- Init.Data.Nat.Basic
Nat.mul_sub : ∀ (n m k : ℕ), n * (m - k) = n * m - n * k
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {toPowerSeries : MvPowerSeries (Fin 2) R}
  {zero_constantCoeff : MvPowerSeries.constantCoeff toPowerSeries = 0}
  {lin_coeff_X : (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries = 1}
  {lin_coeff_Y : (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries = 1}
  {assoc :
    MvPowerSeries.subst ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries, MvPowerSeries.X 2]
        toPowerSeries =
      MvPowerSeries.subst
        ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries] toPowerSeries}
  {toPowerSeries_1 : MvPowerSeries (Fin 2) R} {zero_constantCoeff_1 : MvPowerSeries.constantCoeff toPowerSeries_1 = 0}
  {lin_coeff_X_1 : (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries_1 = 1}
  {lin_coeff_Y_1 : (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries_1 = 1}
  {assoc_1 :
    MvPowerSeries.subst
        ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries_1, MvPowerSeries.X 2]
        toPowerSeries_1 =
      MvPowerSeries.subst
        ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries_1]
        toPowerSeries_1},
  { toPowerSeries := toPowerSeries, zero_constantCoeff := zero_constantCoeff, lin_coeff_X := lin_coeff_X,
        lin_coeff_Y := lin_coeff_Y, assoc := assoc } =
      { toPowerSeries := toPowerSeries_1, zero_constantCoeff := zero_constantCoeff_1, lin_coeff_X := lin_coeff_X_1,
        lin_coeff_Y := lin_coeff_Y_1, assoc := assoc_1 } →
    toPowerSeries = toPowerSeries_1
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (carrier : Type v) [isRing : Ring carrier] [isAlgebra : Algebra R carrier]
  (carrier_1 : Type v) (isRing_1 : Ring carrier_1) (isAlgebra_1 : Algebra R carrier_1),
  ({ carrier := carrier, isRing := isRing, isAlgebra := isAlgebra } =
      { carrier := carrier_1, isRing := isRing_1, isAlgebra := isAlgebra_1 }) =
    (carrier = carrier_1 ∧ isRing ≍ isRing_1 ∧ isAlgebra ≍ isAlgebra_1)
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : αˢʸᵐ), SymAlg.unsym a = 0 ↔ a = 0
-- Mathlib.Data.Set.Sups
Set.infs_comm : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α), s ⊼ t = t ⊼ s