mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.nonneg_addConst_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G}, A.Nonempty → 1 ≤ A.addConst A
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.liftQ.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f f_1 : M →ₛₗ[τ₁₂] M₂) (e_f : f = f_1) (h : p ≤ f.ker), p.liftQ f h = p.liftQ f_1 ⋯
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_sub_eq_of_lt_right : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v y < v x → v (x - y) = v y
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.directedAffineCover_f : ∀ (X : AlgebraicGeometry.Scheme) (U : ↑X.affineOpens), X.directedAffineCover.f U = (↑U).ι
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.pow.eq_1 : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k) (n : ℕ),
  f.pow n = Nat.rec (ModularForm.mcast ⋯ 1 ⋯) (fun n g => ModularForm.mcast ⋯ (g.mul f) ⋯) n
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.HasSplitEqualizer.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y},
  (∃ W h, Nonempty (CategoryTheory.IsSplitEqualizer f g h)) → CategoryTheory.HasSplitEqualizer f g
-- Batteries.Util.ProofWanted
/-- Internal bracket syntax `❰foo❱` for referencing an earlier `theorem_wanted` or
`def_wanted`. Only meaningful inside the statement or body of one of those commands;
the term elaborator errors everywhere else.  -/
wantedRef : Lean.ParserDescr
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mk.inj : ∀ {R : Type u_2} {M : Type u_4} {inst : Semiring R} {inst_1 : PartialOrder R} {inst_2 : AddCommMonoid M}
  {inst_3 : SMul R M} {carrier : Set M} {smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier}
  {add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier} {carrier_1 : Set M}
  {smul_mem'_1 : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier_1 → c • x ∈ carrier_1}
  {add_mem'_1 : ∀ ⦃x : M⦄, x ∈ carrier_1 → ∀ ⦃y : M⦄, y ∈ carrier_1 → x + y ∈ carrier_1},
  { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } =
      { carrier := carrier_1, smul_mem' := smul_mem'_1, add_mem' := add_mem'_1 } →
    carrier = carrier_1
-- Mathlib.Data.List.Nodup
List.nodup_map_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {l : List α}, Function.Injective f → ((List.map f l).Nodup ↔ l.Nodup)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The inverse of the distance from one vertex to the opposite face is less than the sum of that
quantity for the other vertices. This implies the existence of the excenter opposite that vertex;
it also gives information about the location of the incenter (see
`excenterWeights_empty_lt_inv_two`).  -/
Affine.Simplex.inv_height_lt_sum_inv_height : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), (s.height i)⁻¹ < ∑ j with j ≠ i, (s.height j)⁻¹
-- Init.Data.Nat.Lemmas
/-- Tail-recursive runtime replacement for `decidableExistsLT'`.  -/
Nat.decidableExistsLT'TR : {k : ℕ} →
  {p : (m : ℕ) → m < k → Prop} → [(m : ℕ) → (h : m < k) → Decidable (p m h)] → Decidable (∃ m, ∃ (h : m < k), p m h)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_bot : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus ↑⊥ = Set.univ
-- Mathlib.Order.Category.Frm
Frm.ext : ∀ {X Y : Frm} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_eq_of_preservesColimit_coyoneda_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} [CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone D} (hc : CategoryTheory.Limits.IsColimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D (CategoryTheory.coyoneda.obj (Opposite.op X))] {i : J} (f g : X ⟶ D.obj i),
  CategoryTheory.CategoryStruct.comp f (c.ι.app i) = CategoryTheory.CategoryStruct.comp g (c.ι.app i) →
    ∃ j a, CategoryTheory.CategoryStruct.comp f (D.map a) = CategoryTheory.CategoryStruct.comp g (D.map a)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.Generators.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : IsFreeGroup G], IsFreeGroup.Generators G = ⋯.choose
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_inverse_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Under X)ᵒᵖ} (f : Z ⟶ Y),
  (CategoryTheory.Over.opEquivOpUnder X).inverse.map f =
    CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csInf_iff'' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
  s.Nonempty → (a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b)
-- Init.Data.BitVec.Bitblast
BitVec.neg_sdiv_neg : ∀ {w : ℕ} {x y : BitVec w}, x ≠ BitVec.intMin w → (-x).sdiv (-y) = x.sdiv y
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.vaddCommClass : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {α : Type u_1} {β : Type u_2} [inst_2 : VAdd M β] [inst_3 : VAdd α β] [VAddCommClass M α β], VAddCommClass (↥p) α β
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- As normal subgroups are closed under conjugation, they inherit the conjugation action
of the underlying group.  -/
ConjAct.Subgroup.conjAction : {G : Type u_3} → [inst : Group G] → {H : Subgroup G} → [hH : H.Normal] → SMul (ConjAct G) ↥H
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.levelParams : Lean.Elab.PartialFixpoint.EqnInfo → List Lean.Name
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_ne_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) [Nontrivial R], φ.polyCharpoly b ≠ 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_X_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ),
  (MvPowerSeries.coeff m) (MvPowerSeries.X s ^ n) = if m = fun₀ | s => n then 1 else 0
-- Mathlib.Data.List.ModifyLast
_private.Mathlib.Data.List.ModifyLast.0.List.modifyLast.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : α) (xs : List α) (acc : Array α)
  (h_1 : (x : Array α) → motive [] x) (h_2 : (x : α) → (acc : Array α) → motive [x] acc)
  (h_3 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (xs = [] → False) →
    (match x :: xs, acc with
      | [], x => h_1 x
      | [x], acc => h_2 x acc
      | x :: xs, acc => h_3 x xs acc) =
      h_3 x xs acc
-- Mathlib.Analysis.Matrix.Normed
Matrix.instNormedStarGroup : ∀ {m : Type u_3} {α : Type u_5} [inst : Fintype m] [inst_1 : SeminormedAddCommGroup α] [inst_2 : StarAddMonoid α]
  [NormedStarGroup α], NormedStarGroup (Matrix m m α)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- The cardinality required for a given `ε`.  -/
AbsoluteValue.IsAdmissible.card : {R : Type u_1} → [inst : EuclideanDomain R] → {abv : AbsoluteValue R ℤ} → abv.IsAdmissible → ℝ → ℕ
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.lift_genericMonicPoly : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : Nontrivial K] {n : ℕ} (v : Fin (n + 1) → K),
  (FreeCommRing.lift v) (FirstOrder.Field.genericMonicPoly n) =
    Polynomial.eval (v (Fin.last n))
      ↑(((Polynomial.monicEquivDegreeLT n).trans (Polynomial.degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.ofContinuousOpenRestrict_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) (hs : IsOpen e.source),
  (OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs).toPartialHomeomorph =
    PartialHomeomorph.ofContinuousOpenRestrict e hc ho
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_pos_lt_iff : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ}, 0 < n → ((⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instHasZeroObject : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.AddGrp C)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) (X : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).functor.obj X).pt = X.pt
-- Mathlib.Control.Monad.Writer
WriterT.ext_iff : ∀ {M : Type u → Type v} {α ω : Type u} {x x' : WriterT ω M α}, x = x' ↔ x.run = x'.run
-- Mathlib.RingTheory.Ideal.Maps
/-- An element is in the kernel if and only if it maps to zero.  -/
RingHom.mem_ker : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] {f : F} {r : R}, r ∈ RingHom.ker f ↔ f r = 0
-- Mathlib.Data.Nat.Log
Nat.le_pow_clog : ∀ {b : ℕ}, 1 < b → ∀ (x : ℕ), x ≤ b ^ Nat.clog b x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A `SubAddAction` of an `AddAction` is an `AddAction`.  -/
SubAddAction.SMulMemClass.toAddAction : {R : Type u} →
  {M : Type v} →
    [inst : AddMonoid R] →
      [inst_1 : AddAction R M] →
        {A : Type u_1} → [inst_2 : SetLike A M] → [hA : VAddMemClass A R M] → (S' : A) → AddAction R ↥S'
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.homotopyEquivalences_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  HomologicalComplex.homotopyEquivalences V c f.hom
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y)
  (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) ⦃Y'' : C⦄ (g' : Y'' ⟶ Y') (g'f₁ : Y'' ⟶ X₁) (g'f₂ : Y'' ⟶ X₂)
  (hgf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom._auto_1)
  (hgf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₂ = gf₂)
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom._auto_3)
  (hg'f₁ :
    autoParam (CategoryTheory.CategoryStruct.comp g' gf₁ = g'f₁)
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom._auto_5)
  (hg'f₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' gf₂ = g'f₂)
      CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom._auto_7),
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ =
    CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ (CategoryTheory.CategoryStruct.comp g' g) g'f₁ g'f₂ ⋯
      ⋯
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (h_1 : (x x_1 : ℕ) → motive [] x x_1)
  (h_2 : (a : α) → (xs : List α) → motive (a :: xs) 0 0)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ),
  (match a :: xs, 0, 0 with
    | [], x, x_1 => h_1 x x_1
    | a :: xs, 0, 0 => h_2 a xs
    | a :: xs, 0, i.succ => h_3 a xs i
    | a :: xs, i.succ, 0 => h_4 a xs i
    | a :: xs, i.succ, j.succ => h_5 a xs i j) =
    h_2 a xs
-- Std.Http.Data.Request
Std.Http.instInhabitedRequest : {a : Type} → [Inhabited a] → Inhabited (Std.Http.Request a)
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The von Mangoldt function restricted to the residue class `a` mod `q`.  -/
ArithmeticFunction.vonMangoldt.residueClass : {q : ℕ} → ZMod q → ℕ → ℝ
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The composition on `SmallShiftedHom W`.  -/
CategoryTheory.Localization.SmallShiftedHom.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            [W.IsCompatibleWithShift M] →
              {X Y Z : C} →
                {a b c : M} →
                  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                    [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] →
                      [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] →
                        [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] →
                          CategoryTheory.Localization.SmallShiftedHom W X Y a →
                            CategoryTheory.Localization.SmallShiftedHom W Y Z b →
                              b + a = c → CategoryTheory.Localization.SmallShiftedHom W X Z c
-- Mathlib.Data.List.AList
AList.entries_toAList : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (xs : List (Sigma β)), xs.toAList.entries = xs.dedupKeys
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mass_comap_le : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] (f : Ω → Ω')
  (μ : MeasureTheory.FiniteMeasure Ω'), (MeasureTheory.FiniteMeasure.comap f μ).mass ≤ μ.mass
-- Mathlib.Order.Filter.Basic
Filter.frequently_false : ∀ {α : Type u} (f : Filter α), ¬∃ᶠ (x : α) in f, False
-- Mathlib.Data.Matrix.Basic
Matrix.evalAddMonoidHom_comp_diagAddMonoidHom : ∀ {m : Type u_2} {α : Type u_11} [inst : AddZeroClass α] (i : m),
  (Pi.evalAddMonoidHom (fun i => α) i).comp (Matrix.diagAddMonoidHom m α) = Matrix.entryAddMonoidHom α i i
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- In a manifold `M`, given two preferred charts indexed by `x y : M`, `tangentCoordChange I x y`
is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values
outside the intersection of the sources of the two charts.

Note that this definition takes advantage of the fact that `tangentBundleCore` has the same base
sets as the preferred charts of the base manifold.  -/
tangentCoordChange : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_6} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → [IsManifold I 1 M] → M → M → M → E →L[𝕜] E
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_inv : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.conjugateEquiv
        ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction g).comp
          (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f))
        (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.comp f g)))
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv =
    (AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.apply_omega0_of_isNormal : ∀ {f : Ordinal.{u} → Ordinal.{v}}, Order.IsNormal f → ⨆ n, f ↑n = f Ordinal.omega0
-- Mathlib.Analysis.Normed.Field.UnitBall
unitSphereToUnits_apply_coe : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)), ↑((unitSphereToUnits 𝕜) x) = ↑x
-- Mathlib.Algebra.Group.AddChar
/-- Interpret an additive character as a monoid homomorphism.  -/
AddChar.toAddMonoidHom : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → AddChar A M → A →+ Additive M
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The partial derivative `W_Y(X, Y, Z)` with respect to `Y` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in Jacobian coordinates.  -/
WeierstrassCurve.Jacobian.polynomialY : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → MvPolynomial (Fin 3) R
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsClosedImmersionFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsClosedImmersion g],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Ring.Parity
Nat.odd_sub : ∀ {m n : ℕ}, n ≤ m → (Odd (m - n) ↔ (Odd m ↔ Even n))
-- Mathlib.MeasureTheory.Measure.Count
/-- `count` measure evaluates to infinity at infinite sets.  -/
MeasureTheory.Measure.count_apply_infinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, s.Infinite → MeasureTheory.Measure.count s = ⊤
-- Mathlib.Data.EReal.Inv
EReal.instPosMulMono : PosMulMono EReal
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅},
  (t.modify k f).minKey he = if cmp (t.minKey ⋯) k = Ordering.eq then k else t.minKey ⋯
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_eq : ∀ {n : ℕ} {x : BitVec n} {i : ℕ}, x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insert_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).size ≤ t.size + 1
-- Mathlib.Topology.Instances.CantorSet
/-- The infinite sequence obtained by repeatedly applying `cantorStep` to `x`.  -/
cantorSequence : ℝ → Stream' ℝ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
/-- **Uniqueness of the conditional expectation**  -/
MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq' : ∀ {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E']
  [inst : NormedSpace ℝ E'],
  m ≤ m0 →
    ∀ (f g : ↥(MeasureTheory.Lp E' p μ)),
      p ≠ 0 →
        p ≠ ⊤ →
          (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ) →
            (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑g) s μ) →
              (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ) →
                MeasureTheory.AEStronglyMeasurable (↑↑f) μ → MeasureTheory.AEStronglyMeasurable (↑↑g) μ → ↑↑f =ᵐ[μ] ↑↑g
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.uniqueIso : {A : Type u} → (x y : CategoryTheory.Codiscrete A) → Unique (x ≅ y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) [CategoryTheory.Epi f],
  CategoryTheory.Epi t.inr
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions of length three are reflected under `2`-Freiman homomorphisms.  -/
IsAddFreimanHom.threeAPFree : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Set α} {t : Set β} {f : α → β},
  IsAddFreimanHom 2 s t f → Set.InjOn f s → ThreeAPFree t → ThreeAPFree s
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.startAdd : ByteArray → ByteArray
-- Init.Data.Nat.Basic
Nat.pow_le_pow_right : ∀ {n : ℕ}, n > 0 → ∀ {i j : ℕ}, i ≤ j → n ^ i ≤ n ^ j
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.vecMul_conjTranspose_mul_self_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R)
  (v : n → R), Matrix.vecMul v (A.conjTranspose * A) = 0 ↔ Matrix.vecMul v A.conjTranspose = 0
-- Std.Time.Format.Modifier
/-- Any size (e.g., "19000000000000")
 -/
Std.Time.Year.any : Std.Time.Year
-- Mathlib.RingTheory.Ideal.Operations
Submodule.ideal_span_singleton_smul : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R)
  (N : Submodule R M), Ideal.span {r} • N = r • N
-- Init.Data.List.Perm
List.Perm.rfl : ∀ {α : Type u_1} {l : List α}, l.Perm l
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.le_chromaticNumber_iff_forall_surjective : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C
-- Mathlib.Order.Disjoint
Complementeds.instComplementedLattice : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α], ComplementedLattice (Complementeds α)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- **Alias** of `LinearMap.BilinForm.IsRefl.eq_iff`. -/
LinearMap.BilinForm.IsRefl.ortho_comm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsRefl → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Algebra.Group.Prod
AddHom.snd.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : Add M] [inst_1 : Add N], AddHom.snd M N = { toFun := Prod.snd, map_add' := ⋯ }
-- Mathlib.Order.Filter.CountablyGenerated
Filter.CountableFilterBasis.mk : {α : Type u_6} → (toFilterBasis : FilterBasis α) → toFilterBasis.sets.Countable → Filter.CountableFilterBasis α
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.ofLinearOrder_snd : ∀ (ι : Type w) [inst : LinearOrder ι] (x : ↑{x | x.1 < x.2}),
  (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).snd x = (↑x).2
-- Mathlib.Analysis.Normed.Module.RCLike.Real
frontier_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → frontier (Metric.ball x r) = Metric.sphere x r
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_trans` -/
ssubset_trans : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊂ b → b ⊂ c → a ⊂ c