mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Lemmas
Vector.getElem_push_eq : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x)[n] = x
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.tendsto_nhds_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {a : α} {b : β},
  Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_obj_right_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X : C),
  (CategoryTheory.WithInitial.equivComma.functor.obj F).right.obj X = F.obj (CategoryTheory.WithInitial.incl.obj X)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_lt_nsmul_iff_left : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ},
  0 < a → (m • a < n • a ↔ m < n)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Type synonym to equip an ordered group with a new `Preorder` defined by the infinitesimal order
of elements. `a` is said less than `b` if `b` is infinitesimal comparing to `a`, or more precisely,
`∀ n, |b|ₘ ^ n < |a|ₘ`. If `a` and `b` are neither infinitesimal to each other, they are equivalent
in this order.  -/
MulArchimedeanOrder : Type u_1 → Type u_1
-- Std.Sat.CNF.Basic
Std.Sat.CNF.not_unsat_empty : ∀ {α : Type u_1}, ¬Std.Sat.CNF.empty.Unsat
-- Init.Grind.Config
/-- When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
Finally, note that congruence closure is less effective on terms containing many binders such as
`lambda` and `let` expressions.
 -/
Lean.Grind.Config.zetaDelta : Lean.Grind.Config → Bool
-- Init.Grind.Order
Lean.Grind.Order.le_eq_false_of_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α},
  a < b → (b ≤ a) = False
-- Init.Data.Array.Lemmas
Array.foldl_congr : ∀ {α : Type u_1} {β : Type u_2} {as bs : Array α},
  as = bs →
    ∀ {f g : β → α → β},
      f = g →
        ∀ {a b : β},
          a = b →
            ∀ {start start' stop stop' : ℕ},
              start = start' → stop = stop' → Array.foldl f a as start stop = Array.foldl g b bs start' stop'
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.insert_ae_eq_self : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] (a : α)
  (s : Set α), insert a s =ᵐ[μ] s
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkYoneda` at the morphism universe level is `yoneda`.  -/
CategoryTheory.shrinkYonedaIsoYoneda : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.shrinkYoneda.{v, v, u} ≅ CategoryTheory.yoneda
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedENode.default : Lean.Meta.Grind.ENode
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule : Type
-- Mathlib.Logic.Basic
eq_equivalence : ∀ {α : Sort u_1}, Equivalence Eq
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newDepHyp.sizeOf_spec : ∀ (goal : Lean.Meta.Grind.Goal), sizeOf (Lean.Meta.Grind.IntroResult.newDepHyp✝ goal) = 1 + sizeOf goal
-- Init.Data.BitVec.Lemmas
BitVec.add_sub_cancel : ∀ {w : ℕ} (x y : BitVec w), x + y - y = x
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instInhabited : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Inhabited (WittVector p R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.ext : ∀ {Δ : SimplexCategoryᵒᵖ} (A₁ A₂ : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (h₁ : A₁.fst = A₂.fst),
  CategoryTheory.CategoryStruct.comp A₁.e (CategoryTheory.eqToHom ⋯) = A₂.e → A₁ = A₂
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B` over a
linearly ordered base `B` and a point `a ∈ e.baseSet ∩ e'.baseSet`, `e.piecewise_le e' a He He'`
is the bundle trivialization over `Set.ite (Iic a) e.baseSet e'.baseSet` that is equal to `e` on
points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
`h = e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
`h (e' p).2 = (e p).2` whenever `e p = a`.  -/
Bundle.Trivialization.piecewiseLe : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              [inst_3 : LinearOrder B] →
                [OrderTopology B] →
                  (e e' : Bundle.Trivialization F proj) →
                    (a : B) → a ∈ e.baseSet → a ∈ e'.baseSet → Bundle.Trivialization F proj
-- Mathlib.Analysis.Complex.Harmonic.Liouville
_private.Mathlib.Analysis.Complex.Harmonic.Liouville.0.InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant_aux : ∀ (f : ℂ → ℝ), InnerProductSpace.HarmonicOnNhd f Set.univ → Bornology.IsBounded (Set.range f) → ∀ (z w : ℂ), f z = f w
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReflBEqPower : ReflBEq Lean.Grind.CommRing.Power
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isUnit_coe : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s : Finset α}, IsUnit ↑s ↔ IsUnit s
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_integral_norm_uIoc : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ ∫ (x : ℝ) in Set.uIoc a b, ‖f x‖ ∂μ
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_ofNat : ∀ (x w : ℕ), (BitVec.ofNat w x).toNat = x % 2 ^ w
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_zero : ∀ {α : Type u_1} (M : Type u_3) [inst : Zero M] (s : Set α), (s.indicator fun x => 0) = fun x => 0
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.rel_add : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [c.TensorSigns] {p q : I},
  c.Rel p q → ∀ (r : I), c.Rel (p + r) (q + r)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModuleHierarchyImportedByParams : Lean.FromJson Lean.Lsp.LeanModuleHierarchyImportedByParams
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod.inr_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (x : C),
  CategoryTheory.FunctorToTypes.coprod.inr.app x = TypeCat.ofHom fun x_1 => Sum.inr x_1
-- Mathlib.FieldTheory.Separable
/-- Transfer `IsSeparable` across an `AlgEquiv`.  -/
AlgEquiv.isSeparable_iff : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {E : Type u_4}
  [inst_3 : Ring E] [inst_4 : Algebra F E] (e : K ≃ₐ[F] E) {x : K}, IsSeparable F (e x) ↔ IsSeparable F x
-- Init.Data.List.Lemmas
List.map_const : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {b : β}, List.map (Function.const α b) l = List.replicate l.length b
-- Mathlib.Topology.NhdsKer
nhdsKer_singleton_pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] (p : (i : ι) → X i),
  nhdsKer {p} = Set.univ.pi fun i => nhdsKer {p i}
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.instIsometryClass : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β], IsometryClass (α ≃ᵢ β) α β
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.IciBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α],
  OrderIso.IciBot =
    {
      toEquiv :=
        (let __src := Equiv.subtypeUnivEquiv ⋯;
          { toEquiv := __src, map_rel_iff' := ⋯ }).toEquiv,
      map_rel_iff' := ⋯ }
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.mk.inj : ∀ {α β : Type} {socket : Option α} {expect : Option ℕ}
  {response : Option (Std.Channel (Except IO.Error (Std.Http.Response β)))} {responseBody : Option β}
  {requestBody : Option Std.Http.Body.Stream} {timeout : Std.Time.Millisecond.Offset}
  {keepAliveTimeout : Option Std.Time.Millisecond.Offset} {headerTimeout : Option Std.Time.Timestamp}
  {connectionContext : Std.CancellationContext} {socket_1 : Option α} {expect_1 : Option ℕ}
  {response_1 : Option (Std.Channel (Except IO.Error (Std.Http.Response β)))} {responseBody_1 : Option β}
  {requestBody_1 : Option Std.Http.Body.Stream} {timeout_1 : Std.Time.Millisecond.Offset}
  {keepAliveTimeout_1 : Option Std.Time.Millisecond.Offset} {headerTimeout_1 : Option Std.Time.Timestamp}
  {connectionContext_1 : Std.CancellationContext},
  { socket := socket, expect := expect, response := response, responseBody := responseBody, requestBody := requestBody,
        timeout := timeout, keepAliveTimeout := keepAliveTimeout, headerTimeout := headerTimeout,
        connectionContext := connectionContext } =
      { socket := socket_1, expect := expect_1, response := response_1, responseBody := responseBody_1,
        requestBody := requestBody_1, timeout := timeout_1, keepAliveTimeout := keepAliveTimeout_1,
        headerTimeout := headerTimeout_1, connectionContext := connectionContext_1 } →
    socket = socket_1 ∧
      expect = expect_1 ∧
        response = response_1 ∧
          responseBody = responseBody_1 ∧
            requestBody = requestBody_1 ∧
              timeout = timeout_1 ∧
                keepAliveTimeout = keepAliveTimeout_1 ∧
                  headerTimeout = headerTimeout_1 ∧ connectionContext = connectionContext_1
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.instUniquePaths : (V : Type u₁) → [Unique V] → Unique (CategoryTheory.Paths V)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioo_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioo a b)), Subtype.val '' Set.Iic c = Set.Ioc a ↑c
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects.  -/
CategoryTheory.Adjunction.mapMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (a : F ⊣ G) → [inst_4 : F.Monoidal] → [inst_5 : G.LaxMonoidal] → [a.IsMonoidal] → F.mapMon ⊣ G.mapMon
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.mk : {m : Type → Type} →
  ({α : Type} → Array Lean.Expr → m α → m α) →
    (Lean.Expr → m Lean.Expr) → (Lean.Expr → m Lean.Meta.MonadSimp.Result) → Lean.Meta.MonadSimp m
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ (l₁ l₂ : (i : ι) → G i) (s : Finset ι),
      inner 𝕜 (∑ i ∈ s, (V i) (l₁ i)) (∑ j ∈ s, (V j) (l₂ j)) = ∑ i ∈ s, inner 𝕜 (l₁ i) (l₂ i)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  {x : V → ℝ}, (SimpleGraph.lapMatrix ℝ G).mulVec x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection from the total space of a fiber bundle core, on its base.  -/
FiberBundleCore.proj : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → Z.TotalSpace → B
-- Mathlib.Order.Fin.Basic
Fin.instCoheytingAlgebra : {n : ℕ} → [NeZero n] → CoheytingAlgebra (Fin n)
-- Mathlib.Order.RelSeries
RelSeries.toList_getElem_zero_eq_head : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.toList[0] = p.head
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_4 : ∀ (p : PosNum) (n : ℕ), p.bit0.testBit n.succ = p.testBit n
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The `CommMonCat`-valued coyoneda embedding.  -/
CommMonCat.coyoneda : CategoryTheory.Functor CommMonCatᵒᵖ (CategoryTheory.Functor CommMonCat CommMonCat)
-- Lean.Elab.Coinductive
_private.Lean.Elab.Coinductive.0.Lean.Elab.Command.rewriteGoalUsingEq : Lean.MVarId → Lean.Expr → optParam Bool false → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsMonHom.monoidHom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N)
  [inst_4 : CategoryTheory.IsMonHom f] (X : C) (x : X ⟶ M),
  (CategoryTheory.IsMonHom.monoidHom f X) x = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.cos_lt_one_div_sqrt_sq_add_one : ∀ {x : ℝ}, -(3 * Real.pi / 2) ≤ x → x ≤ 3 * Real.pi / 2 → x ≠ 0 → Real.cos x < 1 / √(x ^ 2 + 1)
-- Init.Data.List.Attach
List.mem_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a} {b : β},
  b ∈ List.pmap f l H ↔ ∃ a, ∃ (h : a ∈ l), f a ⋯ = b
-- Lean.Meta.Constructions.CasesOnSameCtor
/-- Helper for `mkCasesOnSameCtor` that constructs a heterogeneous matcher (indices may differ)
and does not include the equality proof in the motive (so it's not a the shape of a matcher) yet.
 -/
Lean.mkCasesOnSameCtorHet : Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Ensure that `forget₂ CommMonCat MonCat` automatically reflects isomorphisms.  -/
Semigrp.forget₂_full : (CategoryTheory.forget₂ Semigrp MagmaCat).Full
-- Mathlib.Data.Set.NAry
/-- **Alias** of `Set.subset_image2_sdiff_left`. -/
Set.subset_image2_diff_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Set.image2 f s t \ Set.image2 f s' t ⊆ Set.image2 f (s \ s') t
-- Mathlib.Data.Multiset.Bind
Multiset.bind_cons : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) (g : α → Multiset β),
  (s.bind fun a => f a ::ₘ g a) = Multiset.map f s + s.bind g
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ofHom_apply : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : Fintype X] [inst_3 : DistribLattice Y]
  [inst_4 : BoundedOrder Y] [inst_5 : Fintype Y] (f : BoundedLatticeHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (FinBddDistLat.ofHom f)) x = f x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (hl : t.Balanced) (n n_1 : ℕ)
  (e_n : n = n_1) (h : n < t.size), t.keyAtIdx hl n h = t_1.keyAtIdx ⋯ n_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The limit kernel fork of `(K.extend e).d j' k'` that is deduced from a limit
kernel fork of `K.d j k `.  -/
HomologicalComplex.extend.leftHomologyData.isLimitKernelFork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {j k : ι} →
                      {j' k' : ι'} →
                        (hj' : e.f j = j') →
                          (hk : c.next j = k) →
                            (hk' : c'.next j' = k') →
                              (cone : CategoryTheory.Limits.KernelFork (K.d j k)) →
                                CategoryTheory.Limits.IsLimit cone →
                                  CategoryTheory.Limits.IsLimit
                                    (HomologicalComplex.extend.leftHomologyData.kernelFork K e hj' hk hk' cone)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, (t.erase k).getD k fallback = fallback
-- Mathlib.GroupTheory.MonoidLocalization.Divisibility
Submonoid.LocalizationMap.map_dvd_map : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {m₁ m₂ : M}, f m₁ ∣ f m₂ ↔ ∃ s ∈ S, m₁ ∣ s * m₂
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f] (a b : X₁ ⊕ X₂),
  Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) a = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) b ↔
    CategoryTheory.Limits.Types.Pushout.Rel' f g a b
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- The inclusion `U ⊓ V ⟶ V` as a morphism in the category of open sets.  -/
TopologicalSpace.OpenNhds.infLERight : {X : TopCat} → {x : ↑X} → (U V : TopologicalSpace.OpenNhds x) → U ⊓ V ⟶ V
-- Init.Data.List.Sublist
List.sublist_append_right : ∀ {α : Type u_1} (l₁ l₂ : List α), l₂.Sublist (l₁ ++ l₂)
-- Mathlib.Algebra.Group.Defs
DivInvMonoid.toMonoid : {G : Type u} → [self : DivInvMonoid G] → Monoid G
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.smul_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroup β] [inst_1 : DistribSMul α β] (s : Set α) (t : Set β),
  s • -t = -(s • t)
-- Mathlib.Algebra.Group.Center
/-- The centralizer of a subset of an additive magma.  -/
Set.addCentralizer : {M : Type u_1} → Set M → [Add M] → Set M
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.notMem : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R}, f.IsEisensteinAt 𝓟 → f.coeff 0 ∉ 𝓟 ^ 2
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.inv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f : X ⟶ G) (g : G ⟶ H)
  [CategoryTheory.IsMonHom g], CategoryTheory.CategoryStruct.comp f⁻¹ g = (CategoryTheory.CategoryStruct.comp f g)⁻¹
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_opow : ∀ {a b c d : Ordinal.{u_1}}, a ≤ c → b ≤ d → 0 < c → a ^ b ≤ c ^ d
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_a₁ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).a₁ = ↑C.u⁻¹ * (W.a₁ + 2 * C.s)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_vadd_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (s : ι → Set α) (t : Set β),
  (⋂ i, s i) +ᵥ t ⊆ ⋂ i, s i +ᵥ t
-- Std.Data.HashMap.Lemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ},
  (Std.HashMap.map f m).getD k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).getD fallback
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.comp_measurePreserving : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε} {ν : MeasureTheory.Measure β},
  MeasureTheory.MemLp g p ν → MeasureTheory.MeasurePreserving f μ ν → MeasureTheory.MemLp (g ∘ f) p μ
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.elim_nhds_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s → ∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhds x) → ∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coeff_uniqueAlgEquiv_symm : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Subsingleton M] (a : A) (m : M), ((MonoidAlgebra.uniqueAlgEquiv R M).symm a).coeff m = a
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- A valuative commutative square over a morphism `f : X ⟶ Y` is a square
```
Spec K ⟶ Y
  |       |
  ↓       ↓
Spec R ⟶ X
```
where `R` is a valuation ring, and `K` is its ring of fractions.

We are interested in finding lifts `Spec R ⟶ Y` of this diagram.
 -/
AlgebraicGeometry.ValuativeCommSq : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Type (u + 1)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst_k : Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly
-- Lean.Data.LBool
Lean.LBool.and : Lean.LBool → Lean.LBool → Lean.LBool
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_ofSubmodule_iff : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {S : Submodule R E} {x : E}, x ∈ ↑S ↔ x ∈ S
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- The space `E` equipped with the weak topology induced by the bilinear form `B`.  -/
WeakBilin : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] → [inst_3 : AddCommMonoid F] → [inst_4 : Module 𝕜 F] → (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Type u_4
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientKerEquivOfRightInverse_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker),
  (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientGroup.kerLift φ) a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S =
    CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.le_cof_map_of_isNormal`. -/
Ordinal.cof_le_of_isNormal : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, Order.IsNormal f → ∀ (a : Ordinal.{u_1}), a.cof ≤ (f a).cof
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- An isomorphism of graphs gives rise to a homomorphism of graphs.  -/
SimpleGraph.Iso.toHom : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ≃g G' → G →g G'