mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The categorical binary coproduct of type-valued functors is `coprod F G`.  -/
CategoryTheory.FunctorToTypes.binaryCoproductIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → F ⨿ G ≅ CategoryTheory.FunctorToTypes.coprod F G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.ext : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Projective R} {x y : W'.Point}, x.point = y.point → x = y
-- Mathlib.Algebra.Ring.Pi
/-- Non-unital ring homomorphism between the function spaces `I → α` and `I → β`, induced by a
non-unital ring homomorphism `f` between `α` and `β`.  -/
NonUnitalRingHom.compLeft : {α : Type u_1} →
  {β : Type u_2} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → (I : Type u_3) → (I → α) →ₙ+* I → β
-- Mathlib.Tactic.Simps.Basic
/-- Linter to check that `simps!` is used when needed  -/
Lean.Parser.linter.simpsNoConstructor : Lean.Option Bool
-- Mathlib.Data.List.Sort
List.sortedLE_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedLE ↔ l.SortedGE
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.ofPairingInThree_long : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : CharZero R]
  [inst_6 : P.IsCrystallographic] [inst_7 : P.IsReduced] (long short : ι) (h : P.pairingIn ℤ long short = 3),
  RootPairing.EmbeddedG2.long P = (P.reflectionPerm long) long
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_updateFinset' : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [inst_1 : DecidableEq δ] {s : Finset δ},
  Measurable fun p => Function.updateFinset p.1 s p.2
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.IsReal.mult_eq_one : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, w.IsReal → w.mult = 1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The kernel of `zmultiplesHom G g` is equal to the additive subgroup generated by
`addOrderOf g`.  -/
zmultiplesHom_ker_eq : ∀ {G : Type u_2} [inst : AddGroup G] (g : G), ((zmultiplesHom G) g).ker = AddSubgroup.zmultiples ↑(addOrderOf g)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.Limits.WidePullback.base fun x => f.hom) =
    CategoryTheory.Limits.WidePullback.base fun x => f.hom
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.MonadSatisfying.instEStateM.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 :
    (a_1 : α) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.ok a_1 s'_1 → motive (EStateM.Result.ok a_1 s'_1))
  (h_2 :
    (e : ε) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.error e s'_1 → motive (EStateM.Result.error e s'_1)),
  (match w : EStateM.Result.ok a s' with
    | EStateM.Result.ok a_1 s'_1 => h_1 a_1 s'_1 w
    | EStateM.Result.error e s'_1 => h_2 e s'_1 w) =
    h_1 a s' ⋯
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_iff_isFiniteMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {c : β}, c ≠ 0 → (MeasureTheory.Integrable (fun x => c) μ ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.Data.Set.Basic
Set.ssubset_iff_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → (s ⊂ t ↔ ∃ x ∈ t, x ∉ s)
-- Mathlib.FieldTheory.Finite.Basic
ZMod.orderOf_units_dvd_card_sub_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (u : (ZMod p)ˣ), orderOf u ∣ p - 1
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_lid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.comm R R M') ∘ₗ ↑(TensorProduct.lid R M').symm ∘ₗ f = ↑(TensorProduct.rid R M').symm ∘ₗ f
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α Id β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β}
  {it₂ it₂' : Std.IterM m γ} {b : γ},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    (Std.Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.yield (Std.Iter.flatMapAfterM f it₁ (some it₂')) b)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instTop : {α : Type u_2} → [inst : TopologicalSpace α] → Top (TopologicalSpace.Clopens α)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_avg_sub : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) {a b c d : ℤ},
  d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2 →
    IsEllipticNet.atomRel W ((a + b + c + d) / 2 - d) ((a + b + c + d) / 2 - c) ((a + b + c + d) / 2 - b)
        ((a + b + c + d) / 2 - a) =
      IsEllipticNet.atomRel W a b c d
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_stringSlice : ∀ {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {s : String.Slice} {init : β} {f : Char → β → m (ForInStep β)}
  (inv : Std.Do.StringSliceInvariant s β ps),
  (∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
      ⦃inv.1 (pos, b)⦄
        f (pos.get h) b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 (pos.next h, b')
          | ForInStep.done b' => inv.1 (s.endPos, b'),
          inv.2)⦄) →
    ⦃inv.1 (s.startPos, init)⦄ forIn s init f ⦃(fun b => inv.1 (s.endPos, b), inv.2)⦄
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.mk.sizeOf_spec : ∀ (instType instVal : Lean.Expr),
  sizeOf { instType := instType, instVal := instVal } = 1 + sizeOf instType + sizeOf instVal
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ofValuation_symm_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀],
  AddValuation.ofValuation.symm = AddValuation.toValuation
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        (m₁.inter! m₂).get! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.get! k else default
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.range_mapRangeLinearMap : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearMap f).range =
    Submodule.comap (DFinsupp.coeFnLinearMap R) (Submodule.pi Set.univ fun x => (f x).range)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpenMap_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap OnePoint.some
-- Mathlib.Tactic.WithoutCDot
/-- A set of parentheses, supporting type ascriptions, which does not process `·`.

Primarily, this is useful when quoting user-provided syntax inside parentheses, as it prevents `·`s
from the caller being interpreted in the context of `()`s from the macro.  -/
Lean.Elab.Term.withoutCDot : Lean.Parser.Parser
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lift_cof : ∀ (o : Ordinal.{u}), Cardinal.lift.{v, u} o.cof = (Ordinal.lift.{v, u} o).cof
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.comp_eq_top_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C),
  W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂
-- Lean.Parser.Syntax
Lean.Parser.Command.optKind.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Localization.AsSubring
/-- Given a commutative ring `A` with fraction ring `K`, and a submonoid `S` of `A` which
contains no zero divisor, this is the localization of `A` at `S`, considered as
a subalgebra of `K` over `A`.

The carrier of this subalgebra is defined as the set of all `x : K` of the form
`IsLocalization.mk' K a ⟨s, _⟩`, where `s ∈ S`.
 -/
Localization.subalgebra : {A : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing A] →
      (S : Submonoid A) →
        [inst_1 : CommRing K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → S ≤ nonZeroDivisors A → Subalgebra A K
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.instDilationEquivClass : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y],
  DilationEquivClass (X ≃ᵈ Y) X Y
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.mulHom_of_of : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : Add ι] [inst_2 : (i : ι) → AddCommMonoid (A i)]
  [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j),
  ((DirectSum.mulHom A) ((DirectSum.of A i) a)) ((DirectSum.of A j) b) =
    (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul a b)
-- Lean.Meta.Basic
/-- Enable/Disable support for offset constraints such as `?x + 1 =?= e`  -/
Lean.Meta.Config.offsetCnstrs : Lean.Meta.Config → Bool
-- Mathlib.Data.Finset.Sups
Finset.card_diffs_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  (s.diffs t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 \ x.2) (↑s ×ˢ ↑t)
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.of_finite : ∀ {T : Type u_3} [inst : CommRing T] {S : Type u_5} [inst_1 : CommRing S] {f : S →+* T}, f.Finite → f.QuasiFinite
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
exists_le_add_iff_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α]
  [AddLeftMono α] [IsLeftCancelAdd α], (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_zero_hom_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (a : M) (X : C),
  (F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).hom.app X)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.le_annihilator_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {I : Ideal R}, I ≤ N.annihilator ↔ I • N = ⊥
-- Mathlib.FieldTheory.Separable
Polynomial.separable_prod_X_sub_C_iff : ∀ {F : Type u} [inst : Field F] {ι : Type u_1} [inst_1 : Fintype ι] {f : ι → F},
  (∏ i, (Polynomial.X - Polynomial.C (f i))).Separable ↔ Function.Injective f
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap_comp : ∀ {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d), (ZMod.unitsMap hm).comp (ZMod.unitsMap hd) = ZMod.unitsMap ⋯
-- Init.Data.List.TakeDrop
List.dropWhile_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : List α},
  List.dropWhile p (xs ++ ys) =
    if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_mul_I_antiperiodic : Function.Antiperiodic (fun x => Complex.exp (x * Complex.I)) ↑Real.pi
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_eq_eval : ∀ {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring S₁] (f : σ → S₁), ⇑(MvPolynomial.aeval f) = ⇑(MvPolynomial.eval f)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_id_add_one : ∀ (o : Ordinal.{u}), ((o + 1).bsup fun x x_1 => x) = o
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → Bool},
          (Std.DTreeMap.Internal.Impl.filter! f t₁).Equiv (Std.DTreeMap.Internal.Impl.filter! f t₂)
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isLittleOTVS_iff_isLittleO`. -/
Asymptotics.isLittleOTVS.isLittleO : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =o[𝕜; l] g → f =o[l] g
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.noConfusionType : Sort v✝ → Lean.Elab.Term.Do.ToTerm.Kind → Lean.Elab.Term.Do.ToTerm.Kind → Sort v✝
-- Mathlib.Order.RelClasses
instIsStrictTotalOrderOfIsWellOrder : ∀ {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r], IsStrictTotalOrder α r
-- Init.Data.Nat.Power2.Basic
/-- Returns the least power of two that's greater than or equal to `n`.

Examples:
* `Nat.nextPowerOfTwo 0 = 1`
* `Nat.nextPowerOfTwo 1 = 1`
* `Nat.nextPowerOfTwo 2 = 2`
* `Nat.nextPowerOfTwo 3 = 4`
* `Nat.nextPowerOfTwo 5 = 8`
 -/
Nat.nextPowerOfTwo : ℕ → ℕ
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite : lightToProfinite.PreservesEpimorphisms
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_finset_eq_card : ∀ {α : Type u_1} {n : ℕ}, ↑n ≤ Cardinal.mk α → ∃ s, n = s.card
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.isRed.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      ((c : RBTree.RBColor) →
          (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
        ((x : RBTree.RBNode α) →
            (∀ (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
                x = RBTree.RBNode.node c l v r → False) →
              motive x) →
          motive x
-- Mathlib.Algebra.Star.Conjneg
conjneg_mul : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f g : G → R),
  conjneg (f * g) = conjneg f * conjneg g
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The explicit limit cone in `ProfiniteAddGrp`.  -/
ProfiniteAddGrp.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) → CategoryTheory.Limits.Cone F
-- Mathlib.Data.Finsupp.Order
Finsupp.add_sub_single_one : ∀ {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ}, u' a ≠ 0 → u + (u' - fun₀ | a => 1) = u + u' - fun₀ | a => 1
-- Mathlib.CategoryTheory.Action.Continuous
Action.instMulActionCarrierObjTopCatForget₂ContinuousMap : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] →
                  (X : Action V G) → MulAction G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)
-- Std.Data.HashSet.Raw
/-- Creates a new empty hash set. The optional parameter `capacity` can be supplied to presize the set
so that it can hold the given number of elements without reallocating. It is also possible to use
the empty collection notations `∅` and `{}` to create an empty hash set with the default capacity.
 -/
Std.HashSet.Raw.emptyWithCapacity : {α : Type u} → optParam ℕ 8 → Std.HashSet.Raw α
-- Mathlib.CategoryTheory.Limits.Bicones
/-- The homs for a walking `Bicone J`.  -/
CategoryTheory.BiconeHom : (J : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.Bicone J → CategoryTheory.Bicone J → Type (max u₁ v₁)
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_reindex' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {ι' : Type u_6} [inst_5 : Fintype ι'] [inst_6 : DecidableEq ι']
  (b : Module.Basis ι R M) (e : ι ≃ ι'), (b.reindex e).det = AlternatingMap.domDomCongr e b.det
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (t : CategoryTheory.Limits.Cocone K),
  (CategoryTheory.WithInitial.coconeLift✝.obj t).pt = t.pt.right
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- Suppose `X` is a reduced scheme and that `f g : X ⟶ Y` agree over some separated `Y ⟶ Z`.
Then `f = g` if `ι ≫ f = ι ≫ g` for some dominant `ι`.
 -/
AlgebraicGeometry.ext_of_isDominant_of_isSeparated : ∀ {W X Y Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f g : X ⟶ Y} (s : Y ⟶ Z)
  [AlgebraicGeometry.IsSeparated s],
  CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s →
    ∀ (ι : W ⟶ X) [AlgebraicGeometry.IsDominant ι],
      CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g → f = g
-- Mathlib.Analysis.Calculus.FDeriv.Congr
hasFDerivWithinAt_congr_set_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  s =ᶠ[nhdsWithin x {x}ᶜ] t → (HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.Acyclic.unop : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex Vᵒᵖ c}, K.Acyclic → K.unop.Acyclic
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse, version subtracting vectors.  -/
Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.transpose` as a `RingEquiv` to the opposite ring.

See also `RingEquiv.mopMatrix` for a version that doesn't require `α` to have commutative
multiplication, by taking its opposite.  -/
Matrix.transposeRingEquiv : (m : Type u_2) →
  (α : Type u_11) →
    [inst : AddCommMonoid α] → [inst_1 : CommMagma α] → [inst_2 : Fintype m] → Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.mk : {α : Type u_1} → α → Stream'.Seq (GenContFract.Pair α) → GenContFract α
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis.congr_simp : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b b_1 : Module.Basis ι R M), b = b_1 → ∀ [inst_4 : Finite ι], b.dualBasis = b_1.dualBasis
-- Mathlib.Order.Interval.Set.Infinite
Set.instInfiniteElemIicOfNoMinOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] {a : α}, Infinite ↑(Set.Iic a)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.qParam_ne_zero : ∀ {h : ℝ} (z : ℂ), Function.Periodic.qParam h z ≠ 0
-- Lean.Meta.LitValues
/-- Return `some i` if `e` `OfNat.ofNat`-application encoding an integer, or `Neg.neg`-application of one.  -/
Lean.Meta.getIntValue? : Lean.Expr → Lean.MetaM (Option ℤ)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonSaveOptions : Lean.ToJson Lean.Lsp.SaveOptions
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- Deleting the incident set of the vertex `x` is equivalent to filtering the edges of the simple
graph `G` that do not contain `x`.  -/
SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (x : V),
  (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}
-- Mathlib.CategoryTheory.EpiMono
/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
instance because it would create an instance loop.  -/
CategoryTheory.isSplitEpi_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitEpiCategory C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
-- Mathlib.Data.List.Rotate
List.rotate_eq_iff : ∀ {α : Type u} {l l' : List α} {n : ℕ}, l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ωb_mul_ω : ∀ {q : ℕ}, LucasLehmer.X.ωb * LucasLehmer.X.ω = 1
-- Mathlib.Tactic.Substs
/-- Deprecated: this functionality exists in `subst` now.  -/
Mathlib.Tactic.Substs.substs : Lean.ParserDescr
-- Mathlib.Topology.Order.Basic
exists_Icc_mem_subset_of_mem_nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhdsWithin a (Set.Iic a) → ∃ b ≤ a, Set.Icc b a ∈ nhdsWithin a (Set.Iic a) ∧ Set.Icc b a ⊆ s
-- Batteries.Data.Array.Scan
Array.foldl.hcongr_7 : ∀ (α α' : Type u),
  α = α' →
    ∀ (β β' : Type v),
      β = β' →
        ∀ (f : β → α → β) (f' : β' → α' → β'),
          f ≍ f' →
            ∀ (init : β) (init' : β'),
              init ≍ init' →
                ∀ (as : Array α) (as' : Array α'),
                  as ≍ as' →
                    ∀ (start start' : ℕ),
                      start = start' →
                        ∀ (stop stop' : ℕ),
                          stop = stop' → Array.foldl f init as start stop ≍ Array.foldl f' init' as' start' stop'
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_le_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.toENat c ≤ ↑n ↔ c ≤ ↑n
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteMulSupport.mul` -/
Function.HasFiniteMulSupport.fun_mul : ∀ {α : Type u_1} {M : Type u_3} [inst : MulOneClass M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun i => f i * g i
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom_mk : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.Hom Y.toPresheafedSpace)
  (hf : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))),
  { toHom := f, prop := hf }.toShHom = CategoryTheory.InducedCategory.homMk f
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.indepSets_congr`. -/
ProbabilityTheory.Kernel.IndepSets.congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s1 s2 : Set (Set Ω)},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ → ProbabilityTheory.Kernel.IndepSets s1 s2 η μ
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.instCompleteLattice : {α : Type u_1} → [CompleteLattice α] → CompleteLattice (ULift.{v, u_1} α)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_mem : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ} {x : α}, s.get? n = some x → x ∈ s