mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks]
  (z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π),
  (∀ (ij : I × I),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π
              (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π
              (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij))
          z₂) →
    z₁ = z₂
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.coe_uniqueProd : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X],
  ⇑(Homeomorph.uniqueProd X Y) = Prod.snd
-- Mathlib.Order.OrderDual
OrderDual.instLinearOrder.dual_dual : ∀ (α : Type u_2) [H : LinearOrder α], OrderDual.instLinearOrder αᵒᵈ = H
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The rescaling homeomorphism between additive circles with different periods.  -/
AddCircle.homeomorphAddCircle : {𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    (p q : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst_3 : TopologicalSpace 𝕜] → [OrderTopology 𝕜] → p ≠ 0 → q ≠ 0 → AddCircle p ≃ₜ AddCircle q
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagram_map : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] {X Y : CategoryTheory.Pairwise ι} (x : X ⟶ Y),
  (CategoryTheory.Pairwise.diagram U).map x = CategoryTheory.Pairwise.diagramMap U x
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
/-- Special case of the sandwich lemma; see `tendsto_of_tendsto_of_tendsto_of_le_of_le`
and `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the general case.  -/
squeeze_zero : ∀ {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α},
  (∀ (t : α), 0 ≤ f t) → (∀ (t : α), f t ≤ g t) → Filter.Tendsto g t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_const_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f : α → M} (C : M), Filter.Tendsto (fun x => C + f x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∪ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Algebra.Group.Irreducible.Lemmas
irreducible_mul_isUnit : ∀ {M : Type u_2} [inst : Monoid M] {x y : M}, IsUnit x → (Irreducible (y * x) ↔ Irreducible y)
-- Mathlib.Tactic.Explode.Datatypes
/-- Get the `line` for an `Entry` that has been added to the `Entries` structure.  -/
Mathlib.Explode.Entry.line! : Mathlib.Explode.Entry → ℕ
-- Mathlib.Tactic.Positivity.Core
/-- Gives a generic description of the `positivity` result.  -/
Mathlib.Meta.Positivity.Strictness.toString : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      {e : Q(«$α»)} → {pα? : Option Q(PartialOrder «$α»)} → Mathlib.Meta.Positivity.Strictness zα e pα? → String
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.tensorToSpan_apply_tmul : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M) (a : A) (x : ↥p), ↑((Submodule.tensorToSpan A p) (a ⊗ₜ[R] x)) = a • ↑x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap!.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a)) (size : ℕ) (k' : α)
  (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filterMap! f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match f k' v' with
    | none => (Std.DTreeMap.Internal.Impl.filterMap! f l').link2! (Std.DTreeMap.Internal.Impl.filterMap! f r')
    | some v' =>
      Std.DTreeMap.Internal.Impl.link! k' v' (Std.DTreeMap.Internal.Impl.filterMap! f l')
        (Std.DTreeMap.Internal.Impl.filterMap! f r')
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.zero_eq_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], 0 = ⊥
-- Mathlib.Order.Disjoint
Complementeds.coe_le_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂},
  x.f₀ = y.f₀ → x.f₁ = y.f₁ → x.f₂ = y.f₂ → x.f₃ = y.f₃ → x = y
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedSub : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R], BoundedSub R
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- A functor that preserves pullbacks and binary products also preserves equalizers.  -/
CategoryTheory.Limits.preservesEqualizers_of_preservesPullbacks_and_binaryProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_inj : ∀ {n : ℕ} {x y : BitVec n}, BitVec.Signed.rotate✝ x = BitVec.Signed.rotate✝ y ↔ x = y
-- Init.Data.List.MinMax
List.max?_cons' : ∀ {α : Type u_1} {x : α} [inst : Max α] {xs : List α}, (x :: xs).max? = some (List.foldl max x xs)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramMap.eq_2 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (i j : ι),
  CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.id_pair i j) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.pair i j))
-- Mathlib.Order.Defs.Unbundled
Std.Asymm.antisymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Antisymm r
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mem_nonneg : ∀ {T : Type u_1} [inst : Ring T] [inst_1 : PartialOrder T] [inst_2 : IsOrderedRing T] {a : T},
  a ∈ RingCone.nonneg T ↔ 0 ≤ a
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} P]
  [CategoryTheory.LocallySmall.{w, v_1, u_1} C] [Small.{w, u'} J] [CategoryTheory.LocallySmall.{w, v', u'} J],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} (P.limitsOfShape J)
-- Mathlib.Topology.Inseparable
Inseparable.nhds_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → nhds x = nhds y
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_le_mul_of_one_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : MulOneClass α] [MulLeftMono α] [MulRightMono α] {a b : α},
  1 ≤ a → 1 ≤ b → max a b ≤ a * b
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory E] →
              (L : CategoryTheory.Functor C D) →
                (W : CategoryTheory.MorphismProperty C) →
                  (F : CategoryTheory.Functor D E) →
                    (G : CategoryTheory.Functor C E) →
                      [CategoryTheory.Localization.Lifting L W G F] →
                        CategoryTheory.Localization.Lifting₂ L L W W
                          (CategoryTheory.MonoidalCategory.curriedTensorPre G)
                          (CategoryTheory.MonoidalCategory.curriedTensorPre F)
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.instAddMonoidHomClass : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Module S M₃] {σ : R →+* S} [inst_6 : FunLike F M M₃] [SemilinearMapClass F σ M M₃], AddMonoidHomClass F M M₃
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_2 size k v r
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- When lowered to a prop, `Matrix.invertibleEquivDetInvertible` forms an `iff`.  -/
Matrix.isUnit_iff_isUnit_det : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A ↔ IsUnit A.det
-- Lean.Meta.Tactic.Grind.EMatch
/-- Processes `continue` constraint used to implement multi-patterns.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processContinue : Lean.Meta.Grind.EMatch.Choice → Lean.Expr → Lean.Meta.Grind.EMatch.M Unit
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.symm : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'}, t.SameKeys t' → t'.SameKeys t
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_inf_sup_pi : ∀ {ι : Type u_2} [inst : Fintype ι] (x y : ι → ℝ), dist (x ⊓ y) (x ⊔ y) = dist x y
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.mk.sizeOf_spec : ∀ (toSemiring : Lean.Meta.Sym.Arith.Semiring) (ringId : ℕ) (commSemiringInst : Lean.Expr)
  (addRightCancelInst? : Option (Option Lean.Expr)) (toQFn? : Option Lean.Expr),
  sizeOf
      { toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
    1 + sizeOf toSemiring + sizeOf ringId + sizeOf commSemiringInst + sizeOf addRightCancelInst? + sizeOf toQFn?
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `c` is a limit kernel fork for `g : X ⟶ Y`, `e : X ≅ X'` and `g' : X' ⟶ Y` is a morphism,
then there is a limit kernel fork for `g'` with the same point as `c` if for any
morphism `φ : W ⟶ X`, there is an equivalence `φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0`.  -/
CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {g : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork g} →
            CategoryTheory.Limits.IsLimit c →
              {X' Y' : C} →
                (g' : X' ⟶ Y') →
                  (e : X ≅ X') →
                    (iff :
                        ∀ ⦃W : C⦄ (φ : W ⟶ X),
                          CategoryTheory.CategoryStruct.comp φ g = 0 ↔
                            CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp e.hom g') = 0) →
                      CategoryTheory.Limits.IsLimit
                        (CategoryTheory.Limits.KernelFork.ofι
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) e.hom) ⋯)
-- Init.Data.Nat.Gcd
Nat.gcd_pow_left_of_gcd_eq_one : ∀ {k n m : ℕ}, n.gcd m = 1 → (n ^ k).gcd m = 1
-- Mathlib.Data.TypeVec
TypeVec.id_eq_nilFun : ∀ {α : TypeVec.{u_1} 0}, TypeVec.id = TypeVec.nilFun
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.l_iSup₂ : ∀ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {f : (i : ι) → κ i → α}, l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- **Alias** of `HahnSeries.orderTop_mul_of_ne_zero`. -/
HahnSeries.orderTop_mul_of_nonzero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).orderTop = x.orderTop + y.orderTop
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.collectUsed : Lean.MVarId → Array Lean.FVarId → Bool → StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Lean.FVarIdSet
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.instHasDimensionLTHAddNat : ∀ (X : SSet) (n : ℕ) [X.HasDimensionLT n] (k : ℕ), X.HasDimensionLT (n + k)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withUserConfig : {α : Type} → (Lean.Options → Lean.Options) → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Order.Directed
isTop_iff_isMax : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [IsDirectedOrder α], IsTop a ↔ IsMax a
-- Mathlib.Order.RelIso.Basic
/-- Inverse map of a relation isomorphism is a relation isomorphism.  -/
RelIso.symm : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → s ≃r r
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α} {fallback v : β},
  Std.DHashMap.Const.getD (m.insert k v) a fallback =
    if (k == a) = true then v else Std.DHashMap.Const.getD m a fallback
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_singleton : ∀ {m n : ℕ}, n = m + 1 → (m<...=n).toArray = #[m + 1]
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsDedekindDomainDvr.isIntegrallyClosed : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [h : IsDedekindDomainDvr A], IsIntegrallyClosed A
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.le_of_add_le_add_left : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LE α] [AddLeftReflectLE α], x ≠ ⊤ → x + y ≤ x + z → y ≤ z
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ematch.injEq : ∀ (thm thm_1 : Lean.Meta.Grind.EMatchTheorem),
  (Lean.Meta.Grind.Entry.ematch thm = Lean.Meta.Grind.Entry.ematch thm_1) = (thm = thm_1)
-- Mathlib.Logic.Function.Basic
Function.Injective.bijective₂_of_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Injective f →
    Function.Injective g → Function.Surjective (f ∘ g) → Function.Bijective f ∧ Function.Bijective g
-- Mathlib.Data.Set.Prod
Set.prodMap_image_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (s : Set α) (t : Set γ),
  Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_getLast!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.max! = t.toList.getLast!
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_inv_comp_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).inv
      ((CategoryTheory.Limits.pullback.snd f g).app d) =
    CategoryTheory.Limits.pullback.snd (f.app d) (g.app d)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  W.φ n = Polynomial.C Polynomial.X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (x : E),
  ‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.map_le_map_iff' : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  f.ker = ⊥ → ∀ {p p' : Submodule R M}, Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p'
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.firstObjEqFamily_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X),
  (CategoryTheory.Equalizer.firstObjEqFamily P R).inv =
    CategoryTheory.Limits.Pi.lift fun f => TypeCat.ofHom fun x => x ↑f.snd ⋯
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIcoMod` is continuous on the right at every point.  -/
continuousWithinAt_toIcoMod_Ici : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x
-- Init.Data.Fin.Lemmas
Fin.val_zero : ∀ (n : ℕ) [inst : NeZero n], ↑0 = 0
-- Mathlib.NumberTheory.SmoothNumbers
/-- `smoothNumbers n` is the set of *`n`-smooth positive natural numbers*, i.e., the
positive natural numbers all of whose prime factors are less than `n`.  -/
Nat.smoothNumbers : ℕ → Set ℕ
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.nsmul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddCommGroup α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (n • c - x) = (-1) ^ n • f (-x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β}, m.isEmpty = true → Std.DHashMap.Const.getD m a fallback = fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.iSup_subcomplexOfSimplex_prod_eq_top : ∀ (X₁ X₂ : SSet), ⨆ x₁, ⨆ x₂, (SSet.Subcomplex.ofSimplex x₁.simplex).prod (SSet.Subcomplex.ofSimplex x₂.simplex) = ⊤
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.wInner_cWeight_eq_boole : ∀ {G : Type u_1} {R : Type u_3} [inst : AddCommGroup G] [inst_1 : RCLike R] [inst_2 : Fintype G] (ψ₁ ψ₂ : AddChar G R),
  ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.addCommGroup : {d : ℤ} → AddCommGroup (ℤ√d)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.fst_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (p₀ p₁ : P1 × P2) (c : k),
  ((AffineMap.lineMap p₀ p₁) c).1 = (AffineMap.lineMap p₀.1 p₁.1) c
-- Init.Omega.IntList
Lean.Omega.IntList.dot_smul_left : ∀ (xs ys : Lean.Omega.IntList) (i : ℤ), (i * xs).dot ys = i * xs.dot ys
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (p q : MvPolynomial σ R),
  MvPolynomial.coeff m (p + q) = MvPolynomial.coeff m p + MvPolynomial.coeff m q
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMono_toDual_comp_iff`. -/
StrictAnti.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → StrictMono (⇑OrderDual.toDual ∘ f)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.isIso_lanAdjunction_homEquiv_symm_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  {F : CategoryTheory.Functor C H} {G : CategoryTheory.Functor D H} (α : F ⟶ L.comp G),
  CategoryTheory.IsIso (((L.lanAdjunction H).homEquiv F G).symm α) ↔ G.IsLeftKanExtension α
-- Mathlib.Data.Complex.Basic
Complex.ofReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n