mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.comp_id : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →⋆* B),
  f.comp (StarMonoidHom.id A) = f
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.image_Ici_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  AntitoneOn f (Set.Ici a) → f '' Set.Ici a ⊆ Set.Iic (f a)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_toSubgroup_symm_apply : ∀ {A : Type u_2} [inst : AddGroup A] (S : Subgroup (Multiplicative A)),
  ↑((RelIso.symm AddSubgroup.toSubgroup) S) = ⇑Additive.toMul ⁻¹' ↑S
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkHCongrWithArity.mkProof : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  ContDiffAt 𝕜 n Φ x ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => Φ x i) x
-- Mathlib.Order.RelIso.Basic
Subtype.wellFoundedGT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedGT α] (p : α → Prop), WellFoundedGT (Subtype p)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.insertMany_array_eq_insertMany_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  (a : Array (α × β)),
  Std.DHashMap.Internal.Raw₀.Const.insertMany m a = Std.DHashMap.Internal.Raw₀.Const.insertMany m a.toList
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.inr_strictMono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : GroupWithZero M₀] [inst_1 : PartialOrder M₀]
  [inst_2 : LinearOrderedCommGroupWithZero N₀] [inst_3 : DecidablePred fun x => x = 0],
  StrictMono ⇑(MonoidWithZeroHom.inr M₀ N₀)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β} {b : β},
  b ∈ s +ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x +ᵥ y = b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (θ : G ⟶ H) {a : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp
      ((θ.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.mapId a).hom.toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) =
    (θ.app a).toFunctor.map ((G.mapId a).hom.toNatTrans.app (f.toFunctor.obj X))
-- Batteries.Data.UInt
UInt32.toUInt64_toNat : ∀ (x : UInt32), x.toUInt64.toNat = x.toNat
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.coeff_modOf_add_self : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g d : G),
  (x.modOf g).coeff (d + g) = 0
-- Init.Data.List.MinMaxOn
/-- Returns an element of the non-empty list `l` that minimizes `f`. If `x`, `y` are
such that `f x = f y`, it returns whichever comes first in the list.

The correctness of this function assumes `β` to be linearly pre-ordered.
The property that `List.minOn` is the first minimizer in the list is guaranteed by the lemma
`List.getElem_minIdxOn`.
 -/
List.minOn : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → (l : List α) → l ≠ [] → α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_left_assoc : ∀ {Z : CategoryTheory.Limits.WalkingReflexivePair} (h : CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.left h) =
    h
-- Mathlib.Topology.NhdsKer
nhdsKer_pair : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y),
  nhdsKer {(x, y)} = nhdsKer {x} ×ˢ nhdsKer {y}
-- Mathlib.Data.Vector.Basic
List.Vector.tail_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n.succ → α), (List.Vector.ofFn f).tail = List.Vector.ofFn fun i => f i.succ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The natural transformation `S.X₂ ⟶ S.opcycles` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.pOpcyclesNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.π₂ ⟶ CategoryTheory.ShortComplex.opcyclesFunctor C
-- Mathlib.Order.Heyting.Basic
GeneralizedHeytingAlgebra.toOrderTop : {α : Type u_4} → [self : GeneralizedHeytingAlgebra α] → OrderTop α
-- Mathlib.Algebra.Star.Basic
isUnit_star : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] {a : R}, IsUnit (star a) ↔ IsUnit a
-- Mathlib.Computability.Reduce
ManyOneEquiv.le_congr_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv q r → (p ≤₀ q ↔ p ≤₀ r)
-- Mathlib.Order.Category.CompleteLat
CompleteLat.Iso.mk_inv : ∀ {α β : CompleteLat} (e : ↑α ≃o ↑β),
  (CompleteLat.Iso.mk e).inv =
    CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filterM : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : MonadAttach n] [inst_4 : LawfulMonad n] [inst_5 : Std.Iterator α₁ m β]
  [inst_6 : Std.Iterator α₂ m β] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift.{w, 0} Bool)}
  {ita : Std.IterM m β} {itb : Std.IterM m β}, ita.Equiv itb → (Std.IterM.filterM f ita).Equiv (Std.IterM.filterM f itb)
-- Mathlib.Topology.Instances.Sign
continuousAt_sign_of_ne_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : TopologicalSpace α] [inst_2 : LinearOrder α] [OrderTopology α] {a : α},
  a ≠ 0 → ContinuousAt (⇑SignType.sign) a
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- A `n + 1`-simplex  -/
SSet.PtSimplex.MulStruct.map : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g fg : X.PtSimplex n x} → {i : Fin n} → f.MulStruct g fg i → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
-- Mathlib.Data.PNat.Prime
PNat.Coprime.symm : ∀ {m n : ℕ+}, m.Coprime n → n.Coprime m
-- Mathlib.Algebra.Order.Field.Basic
/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`.  -/
Mathlib.Meta.Positivity.evalPowZeroInt : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.wideInducedFunctor_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative] (a : C),
  (CategoryTheory.wideInducedFunctor F P).obj a = F a
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDerivWithin`.  -/
iteratedFDerivWithin_clm_apply_const_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E},
  UniqueDiffOn 𝕜 s →
    ∀ {c : E → F →L[𝕜] G},
      ContDiffOn 𝕜 n c s →
        ∀ {i : ℕ},
          ↑i ≤ n →
            ∀ {x : E},
              x ∈ s →
                ∀ {u : F} {m : Fin i → E},
                  (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
-- Lean.Level
Lean.Level.Data.hasMVar : Lean.Level.Data → Bool
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instFintype : {p n : ℕ} → {R : Type u_2} → [Fintype R] → Fintype (TruncatedWittVector p n R)
-- Init.Sym.Lemmas
Lean.Sym.UInt16.le_eq_true : ∀ (a b : UInt16), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of the forward direction of `wellFounded_liftOn₂'_iff`. -/
WellFounded.of_quotient_liftOn₂' : ∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂},
  (WellFounded fun x y => x.liftOn₂' y r H) → WellFounded r
-- Mathlib.RingTheory.LocalRing.Defs
/-- A semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.
Note that `IsLocalRing` is a predicate.  -/
IsLocalRing : (R : Type u_1) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {T : CategoryTheory.Monad C} {of of_1 : C},
  { of := of } = { of := of_1 } → of = of_1
-- Mathlib.Order.Defs.Unbundled
Minimal.prop : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} {x : α}, Minimal P x → P x
-- Mathlib.Algebra.BigOperators.Finprod
AddMonoidHom.map_finsum_of_preimage_zero : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N),
  (∀ (x : M), f x = 0 → x = 0) → ∀ (g : α → M), f (∑ᶠ (i : α), g i) = ∑ᶠ (i : α), f (g i)
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.toLawfulMonad : ∀ (σ : semiOutParam (Type u_1)) {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m], LawfulMonad m
-- Mathlib.Order.Basic
exists_between : ∀ {α : Type u_2} [inst : LT α] [DenselyOrdered α] {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
-- Init.GrindInstances.ToInt
Lean.Grind.instDivUInt64UintOfNatNat : Lean.Grind.ToInt.Div UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily_image_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.nonMemberSubfamily a (Finset.image (insert a) 𝒜) = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_eq_zero_mul' : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M},
  (Multipliable fun n => f (n + 1)) → ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
-- Mathlib.Data.TypeVec
/-- stitch two bits of a vector back together  -/
TypeVec.fromAppend1DropLast : {n : ℕ} → {α : TypeVec.{u_1} (n + 1)} → (α.drop ::: α.last).Arrow α
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_ofNat : ∀ {α : Type u_3} [inst : DivisionSemiring α] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {E₁ : ι → Type u_4} {F : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : (i : ι) → TopologicalSpace (E₁ i)]
  [inst_5 : (i : ι) → AddCommGroup (E₁ i)] [inst_6 : (i : ι) → Module 𝕜 (E₁ i)] [inst_7 : AddCommGroup F]
  [inst_8 : Module 𝕜 F] [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F]
  [inst_11 : ContinuousConstSMul 𝕜 F] (f : (i : ι) → E i ≃L[𝕜] E₁ i),
  (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft F f).symm =
    ContinuousLinearEquiv.continuousMultilinearMapCongrLeft F fun i => (f i).symm
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_injective : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] [Nonempty n],
  Function.Injective (RingCon.matrix n)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMergeWith : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ t₃ t₄ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  (f : α → β → β → β),
  t₁.Equiv t₂ → t₃.Equiv t₄ → (Std.DTreeMap.Const.mergeWith f t₁ t₃).Equiv (Std.DTreeMap.Const.mergeWith f t₂ t₄)
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.hasLiftingProperty_of_wfs : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [W₁.IsWeakFactorizationSystem W₂] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y),
  W₁ i → W₂ p → CategoryTheory.HasLiftingProperty i p
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termT : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.instIsEllipticMap : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), (W.map f).IsElliptic
-- Mathlib.RingTheory.Artinian.Module
isArtinianRing_range : ∀ {R : Type u_1} [inst : Ring R] {S : Type u_2} [inst_1 : Ring S] (f : R →+* S) [IsArtinianRing R],
  IsArtinianRing ↥f.range
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The alternating face complex of the constant complex is the alternating constant complex.  -/
AlgebraicTopology.alternatingFaceMapComplexConst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).comp (AlgebraicTopology.alternatingFaceMapComplex C) ≅
        ChainComplex.alternatingConst
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkAuxConstructions : Array Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Lie.Weights.Basic
/-- Until we define `LieModule.genWeightSpaceOf`, it is useful to have some notation as follows:  -/
_private.Mathlib.Algebra.Lie.Weights.Basic.0.LieModule.«term𝕎(_,_,_)» : Lean.ParserDescr
-- Mathlib.Order.RelIso.Basic
RelEmbedding.instRelHomClass : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, RelHomClass (r ↪r s) r s
-- Mathlib.RingTheory.Ideal.Maps
Pi.ker_ringHom : ∀ {S : Type v} [inst : Semiring S] {ι : Type u_3} {R : ι → Type u_4} [inst_1 : (i : ι) → Semiring (R i)]
  (φ : (i : ι) → S →+* R i), RingHom.ker (RingHom.pi φ) = ⨅ i, RingHom.ker (φ i)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.mk.sizeOf_spec : ∀ (x optType : Lean.Syntax) (codeBlock : Lean.Elab.Term.Do.CodeBlock),
  sizeOf { x := x, optType := optType, codeBlock := codeBlock } = 1 + sizeOf x + sizeOf optType + sizeOf codeBlock
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.bot_factors_iff_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {A B : C} (f : A ⟶ B), ⊥.Factors f ↔ f = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.notMem : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (self : SSet.relativeCellComplexOfMono.Cell i d),
  self.simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))
-- Std.Tactic.BVDecide.Syntax
/-- Enable preprocessing with the `int_toBitVec` simp set to reduce `UIntX`/`IntX` to `BitVec` and
thus make them accessible for `bv_decide`.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.fixedInt : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_finsum : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_3} {f : ι → R},
  (∀ (b : ι), IsNilpotent (f b)) → (∀ (i j : ι), Commute (f i) (f j)) → IsNilpotent (finsum f)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_isStableUnderComposition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) [F.Faithful] [F.Full]
  [P.IsStableUnderComposition], (CategoryTheory.MorphismProperty.relative F P).IsStableUnderComposition
-- Mathlib.RingTheory.SimpleModule.Isotypic
OrderIso.setIsotypicComponents_symm_apply : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsSemisimpleModule R M] (m : ↥(fullyInvariantSubmodule R M)),
  (RelIso.symm OrderIso.setIsotypicComponents) m = {c | ↑c ≤ ↑m}
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyReduced g]
  [AlgebraicGeometry.Flat g] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsLocallyNoetherian X],
  AlgebraicGeometry.IsReduced (CategoryTheory.Limits.pullback f g)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} [inst_1 : SizeOf C]
  (τ₁ : sq₁.X₁ ⟶ sq₂.X₁) (τ₂ : sq₁.X₂ ⟶ sq₂.X₂) (τ₃ : sq₁.X₃ ⟶ sq₂.X₃) (τ₄ : sq₁.X₄ ⟶ sq₂.X₄)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam)
  (comm₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam)
  (comm₂₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam)
  (comm₃₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam),
  sizeOf
      { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, τ₄ := τ₄, comm₁₂ := comm₁₂, comm₁₃ := comm₁₃, comm₂₄ := comm₂₄,
        comm₃₄ := comm₃₄ } =
    1 + sizeOf τ₁ + sizeOf τ₂ + sizeOf τ₃ + sizeOf τ₄ + sizeOf comm₁₂ + sizeOf comm₁₃ + sizeOf comm₂₄ + sizeOf comm₃₄
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.isNoetherianRing : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], IsNoetherianRing R → IsNoetherianRing S
-- Mathlib.Control.ULift
/-- Functorial action.  -/
ULift.map : {α : Type u} → {β : Type v} → (α → β) → ULift.{u', u} α → ULift.{v', v} β
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.plain.inj : ∀ {n n_1 : Lean.Name}, Batteries.Tactic.Alias.AliasInfo.plain n = Batteries.Tactic.Alias.AliasInfo.plain n_1 → n = n_1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.map_adjoin_singleton : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A →ₐ[R] B) (x : A), Subalgebra.map e R[x] = R[e x]
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeUnop_map : ∀ (J : Type w) {X Y : (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.widePushoutShapeUnop J).map f =
    (CategoryTheory.Limits.widePushoutShapeOpMap J (Opposite.unop Y) (Opposite.unop X) f.unop).unop
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instInhabitedUnitVal.default : {α : ℚ} → Std.Time.Internal.UnitVal α
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddAssocClass'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : DecidableEq β] [inst_2 : VAdd α β]
  [inst_3 : VAdd α γ] [inst_4 : VAdd β γ] [VAddAssocClass α β γ], VAddAssocClass (Finset α) (Finset β) (Finset γ)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) =
  CategoryTheory.Iso.refl (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)
-- Mathlib.Topology.IsClosedRestrict
Topology.continuous_reorderRestrictProd : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [inst : (i : ι) → TopologicalSpace (α i)],
  Continuous (Topology.reorderRestrictProd S s)
-- Mathlib.Order.Comparable
CompRel.of_antisymmRel_of_compRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → CompRel (fun x1 x2 => x1 ≤ x2) b c → CompRel (fun x1 x2 => x1 ≤ x2) a c
-- Lean.Environment
Lean.ImportM.Context.env : Lean.ImportM.Context → Lean.Environment
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).2.card + (Finset.mulETransformRight e x).2.card = 2 * x.2.card
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true →
      Std.Internal.List.getKeyD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is induced map `Z²(H, A) ⟶ Z²(G, B)`.  -/
groupCohomology.mapCocycles₂ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k H} →
          {B : Rep.{u_1, u, u} k G} →
            (f : G →* H) →
              (Rep.res f A ⟶ B) →
                (ModuleCat.of k ↥(groupCohomology.cocycles₂ A) ⟶ ModuleCat.of k ↥(groupCohomology.cocycles₂ B))
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.toLinearMap_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →L[𝕜] F),
  ↑(ContinuousLinearMap.lTensor G g) = LinearMap.lTensor G ↑g
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_eval_half_eq_zero : ∀ (k : ℕ), bernoulliFun (2 * k + 1) 2⁻¹ = 0
-- Lean.Data.Trie
Lean.Data.Trie.leaf.inj : ∀ {α : Type} {a a_1 : Option α}, Lean.Data.Trie.leaf a = Lean.Data.Trie.leaf a_1 → a = a_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.coe_support_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  ↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.tensorLeft_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C),
  (CategoryTheory.MonoidalCategory.tensorLeft X).Additive
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.inner_.norm_sq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E),
  ‖x‖ ^ 2 = RCLike.re (inner_✝ 𝕜 x x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKeyD_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKeyD fallback =
            if compare (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.instIsCocomm : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A], Coalgebra.IsCocomm R (ι →₀ A)