mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.ZMod.UnitsCyclic
/-- If `p` is an odd prime, then `(ZMod (p ^ n))ˣ` is cyclic for all n  -/
ZMod.isCyclic_units_of_prime_pow : ∀ (p : ℕ), Nat.Prime p → p ≠ 2 → ∀ (n : ℕ), IsCyclic (ZMod (p ^ n))ˣ
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [toHasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits C],
  (∀ {X Y Z : C} {f : X ⟶ Y} {g₁ g₂ : Z ⟶ X},
      CategoryTheory.IsKernelPair f g₁ g₂ → CategoryTheory.Limits.HasCoequalizer g₁ g₂) →
    (CategoryTheory.MorphismProperty.regularEpi C).IsStableUnderBaseChange → CategoryTheory.Regular C
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If a continuous alternating map is constructed from an alternating map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative.  -/
AlternatingMap.mkContinuous_norm_le' : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ}
  (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ‖f.mkContinuous C H‖ ≤ max C 0
-- Batteries.Data.RunningStats
Batteries.RunningStats.init.injEq : ∀ (count : ℕ) (mean var : Float) (count_1 : ℕ) (mean_1 var_1 : Float),
  ({ count := count, mean := mean, var := var } = { count := count_1, mean := mean_1, var := var_1 }) =
    (count = count_1 ∧ mean = mean_1 ∧ var = var_1)
-- Lean.Setup
/-- The path to the plugin's shared library.  -/
Lean.Plugin.path : Lean.Plugin → System.FilePath
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_eq_mk_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {a c : M} {b d : ↥S},
  AddLocalization.mk a b = AddLocalization.mk c d ↔ (AddLocalization.r S) (a, b) (c, d)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R}
  {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : NonUnitalRing A} {inst_6 : StarRing A}
  {inst_7 : TopologicalSpace A} {inst_8 : Module R A} {inst_9 : IsScalarTower R A A} {inst_10 : SMulCommClass R A A}
  [self : ContinuousMapZero.UniqueHom R A] (s : Set R) [CompactSpace ↑s] [inst_12 : Fact (0 ∈ s)]
  (φ ψ : ContinuousMapZero (↑s) R →⋆ₙₐ[R] A),
  Continuous ⇑φ → Continuous ⇑ψ → φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s) → φ = ψ
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.id_toFun : ∀ (X : Bipointed) (a : X.X), (Bipointed.Hom.id X).toFun a = id a
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRight.congr_simp : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (f f_1 : M₁ →ₗ[R] S),
  f = f_1 → ∀ (x x_1 : M), x = x_1 → f.smulRight x = f_1.smulRight x_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a
continuous multilinear map taking values in the space of functions `∀ i, M' i`.  -/
ContinuousMultilinearMap.pi : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
          [inst_2 : (i : ι) → Module R (M₁ i)] →
            [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] →
              {ι' : Type u_1} →
                {M' : ι' → Type u_2} →
                  [inst_4 : (i : ι') → AddCommMonoid (M' i)] →
                    [inst_5 : (i : ι') → TopologicalSpace (M' i)] →
                      [inst_6 : (i : ι') → Module R (M' i)] →
                        ((i : ι') → ContinuousMultilinearMap R M₁ (M' i)) →
                          ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.instMonoιSigmaStdSimplex : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) {j : ι}
  (c : f.Cell j), CategoryTheory.Mono c.ιSigmaStdSimplex
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.eq_1 : ∀ {α : Type u_1} (l₁ l₂ : List α) (le : α → α → Bool),
  List.MergeSort.Internal.mergeTR l₁ l₂ le = List.MergeSort.Internal.mergeTR.go✝ le l₁ l₂ []
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.upperBound : {α : Type u} → Std.Rxc.Iterator α → α
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_ne_zero' : ∀ {x : ℝ}, √x ≠ 0 ↔ 0 < x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_update_add : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
  f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.VAddAntidiagonal.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite),
  Finset.VAddAntidiagonal a h = h.toFinset
-- Std.Data.DTreeMap.Internal.Operations
/-- Changes the mapping of the key `k` by applying the function `f` to the current mapped value
(if any). This function can be used to insert a new mapping, modify an existing one or delete it.
This version of the function requires `LawfulEqOrd α`. There is an alternative non-dependent version
called `Const.alter`.
 -/
Std.DTreeMap.Internal.Impl.Const.alter : {α : Type u} →
  {β : Type v} →
    [Ord α] →
      α →
        (Option β → Option β) →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) →
            t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α (fun x => β) (t.size - 1) (t.size + 1)
-- Batteries.Data.Nat.Lemmas
Nat.casesAuxOn_zero : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive (n + 1)), Nat.casesAuxOn 0 zero succ = zero
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_1.splitter : (n : ℕ) →
  (P : Fin (n + 1) → Prop) →
    (motive : { i // P i.succ } → Sort u_1) →
      (x : { i // P i.succ }) → ((i : ℕ) → (hi : i < n) → (hp : P ⟨i, hi⟩.succ) → motive ⟨⟨i, hi⟩, hp⟩) → motive x
-- Lean.Expr
Lean.Nat.mkInstSub : Lean.Expr
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_mul : ∀ {K : Type u_1} [inst : Field K] (x y : (NumberField.RingOfIntegers K)ˣ),
  (algebraMap (NumberField.RingOfIntegers K) K) ↑(x * y) =
    (algebraMap (NumberField.RingOfIntegers K) K) ↑x * (algebraMap (NumberField.RingOfIntegers K) K) ↑y
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s ++ s₁ == s₂`  -/
Lean.Grind.AC.SubseqResult.suffix : Lean.Grind.AC.Seq → Lean.Grind.AC.SubseqResult
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.addAndCompilePartial : Lean.LocalContext × Lean.LocalInstances → Array Lean.Elab.PreDefinition → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Data.Set.Insert
Set.inter_insert_of_mem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∈ s → s ∩ insert a t = insert a (s ∩ t)
-- Mathlib.Order.Disjoint
IsCompl.inf_sup : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y x' y' : α},
  IsCompl x y → IsCompl x' y' → IsCompl (x ⊓ x') (y ⊔ y')
-- Mathlib.Analysis.Complex.Norm
Complex.edist_of_re_eq : ∀ {z w : ℂ}, z.re = w.re → edist z w = edist z.im w.im
-- Init.Data.Char.Ordinal
/-- Computes the `m`-th next `Char`, skipping over surrogate code points \(which are not
valid `Char`s\) as necessary.

This function is specified by its interaction with `Char.ordinal`, see
`Char.succMany?_eq`.
 -/
Char.succMany? : ℕ → Char → Option Char
-- Mathlib.Data.Complex.Basic
Complex.conj_eq_iff_real : ∀ {z : ℂ}, (starRingEnd ℂ) z = z ↔ ∃ r, z = ↑r
-- Mathlib.Topology.ContinuousMap.Star
/-- Evaluation of continuous maps at a point, bundled as a star algebra homomorphism.  -/
ContinuousMap.evalStarAlgHom : {X : Type u_1} →
  (S : Type u_2) →
    (R : Type u_3) →
      [inst : TopologicalSpace X] →
        [inst_1 : CommSemiring S] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Algebra S R] →
              [inst_4 : TopologicalSpace R] →
                [inst_5 : IsTopologicalSemiring R] →
                  [inst_6 : StarRing R] → [inst_7 : ContinuousStar R] → X → C(X, R) →⋆ₐ[S] R
-- Mathlib.Algebra.Ring.Equiv
MulEquiv.noZeroDivisors_iff : ∀ {A : Type u_7} {B : Type u_8} [inst : MulZeroClass A] [inst_1 : MulZeroClass B] (e : A ≃* B),
  NoZeroDivisors A ↔ NoZeroDivisors B
-- Mathlib.Algebra.Group.ULift
ULift.sub_down : ∀ {α : Type u} {x y : ULift.{w, u} α} [inst : Sub α], (x - y).down = x.down - y.down
-- Mathlib.Data.NNRat.Defs
NNRat.den_zero : NNRat.den 0 = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forget_reflects_iso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T}, (CategoryTheory.Over.forget X).ReflectsIsomorphisms
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.toLeftFun.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H),
  hS.toLeftFun = ⇑hS.leftQuotientEquiv ∘ Quotient.mk''
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centerCongr_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (e : R ≃+* S)
  (r : ↥(Subsemigroup.center R)), ↑((Subring.centerCongr e) r) = e ↑r
-- Init.Data.String.Basic
String.Slice.Pos.byteIdx_offset_next : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  (pos.next h).offset.byteIdx = pos.offset.byteIdx + (pos.get h).utf8Size
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
/-- An element `s` in an `R`-algebra is almost integral if there exists `r ∈ R⁰` such that
`r • s ^ n ∈ R` for all `n`.  -/
IsAlmostIntegral : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Prop
-- Init.Data.Char.Lemmas
Char.le_trans : ∀ {a b c : Char}, a ≤ b → b ≤ c → a ≤ c
-- Init.Data.String.Basic
String.bytes_inj : ∀ {s t : String}, s.toByteArray = t.toByteArray ↔ s = t
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A morphism in `Comma (𝟭 (C ⥤ D)) (Functor.const C)` gives a morphism between the associated
functors `WithTerminal C ⥤ D`.  -/
CategoryTheory.WithTerminal.ofCommaMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {c c' :
            CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D))
              (CategoryTheory.Functor.const C)} →
          (c ⟶ c') → (CategoryTheory.WithTerminal.ofCommaObject c ⟶ CategoryTheory.WithTerminal.ofCommaObject c')
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, m.WF → k ∈ Std.HashSet.Raw.filter f m → k ∈ m
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst.inj : ∀ {k₁ k₂ : ℤ} {c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr} {c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr} {k₁_1 k₂_1 : ℤ}
  {c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁ k₂ c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁_1 k₂_1 c₁_1 c₂_1 →
    k₁ = k₁_1 ∧ k₂ = k₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearMap₁₂_mkL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  ContinuousLinearMap.toLinearMap₁₂ (TensorProduct.mkL 𝕜 E F) = TensorProduct.mk 𝕜 E F
-- Std.Http.Data.Body.Basic
/-- Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
message if the bytes are not valid for the target type.
 -/
Std.Http.Body.FromByteArray : Type → Type
-- Mathlib.Algebra.Ring.Nat
Nat.instCharZero : CharZero ℕ
-- Lean.Parser.Extension
Lean.Parser.mkParserOfConstantAux : Lean.Name → (Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser) → Lean.ImportM (Bool × Lean.Parser.Parser)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapWithPostcondition_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : γ → Std.Iterators.PostconditionT o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapWithPostcondition g (Std.IterM.filterMapWithPostcondition f it)).toArray =
    (Std.IterM.filterMapWithPostcondition
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toArray
-- Mathlib.Combinatorics.Quiver.Push
Quiver.PushQuiver.arrow : {V : Type u} → [inst : Quiver V] → {W : Type u₂} → {σ : V → W} → {X Y : V} → (X ⟶ Y) → Quiver.PushQuiver σ (σ X) (σ Y)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.smallCoproductDesc.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasCoproducts C] {A : C}
  (s : Set (CategoryTheory.Subobject A)),
  CategoryTheory.Subobject.smallCoproductDesc s =
    CategoryTheory.Limits.Sigma.desc fun j => ((equivShrink (CategoryTheory.Subobject A)).symm ↑j).arrow
-- Lean.Compiler.Specialize
Lean.Compiler.instBEqSpecializeAttributeKind.beq : Lean.Compiler.SpecializeAttributeKind → Lean.Compiler.SpecializeAttributeKind → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Since `⦋0⦌ : SimplexCategory` is terminal, `Δ[0]` has a unique edge and thus the homs of
`OneTruncation₂ ((truncation 2).obj Δ[0])` have unique inhabitants.  -/
SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk : (x y : SSet.OneTruncation₂ ((SSet.truncation 2).obj (SSet.stdSimplex.obj { len := 0 }))) → Unique (x ⟶ y)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.den_smul_val : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f : HomogeneousLocalization 𝒜 x), f.den • f.val = (algebraMap A (Localization x)) f.num
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_one' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K),
  RatFunc.mk p 1 = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p }
-- Mathlib.Topology.Homotopy.Equiv
/-- The forward map of a homotopy.

Do NOT use directly. Use the coercion instead.  -/
ContinuousMap.HomotopyEquiv.toFun : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → C(X, Y)
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivativeFun_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R) (f : PowerSeries R), (r • f).derivativeFun = r • f.derivativeFun
-- Mathlib.Topology.Category.Profinite.Product
/-- The canonical map from `C` to the explicit limit as an isomorphism.  -/
Profinite.isoindexConeLift : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [inst_1 : ∀ (i : ι), T2Space (X i)] →
          [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] →
            (hC : IsCompact C) → Profinite.of ↑C ≅ (Profinite.limitCone (Profinite.indexFunctor hC)).pt
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β))
  (target : { d // 0 < d.size }),
  Std.DHashMap.Internal.Raw₀.expand.go✝ i source target =
    if h : i < source.size then
      have es := source[i];
      have source := source.set i Std.DHashMap.Internal.AssocList.nil h;
      have target := Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target es;
      Std.DHashMap.Internal.Raw₀.expand.go✝ (i + 1) source target
    else target
-- Mathlib.Data.Num.Basic
/-- Ordering of `PosNum`s.  -/
PosNum.cmp : PosNum → PosNum → Ordering
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
      (CategoryTheory.Limits.pullback.fst g f) =
    CategoryTheory.Limits.pullback.snd f g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map f).obj X).left = X.left
-- Mathlib.Algebra.Ring.IsFormallyReal
/-- A ring is formally real if, whenever `∑ i, x i ^ 2 = 0`, we in fact have `x i = 0` for all `i`.
 -/
IsFormallyReal : (R : Type u_1) → [AddCommMonoid R] → [Mul R] → Prop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.offset.injEq : ∀ (e o : Lean.Expr) (n : ℕ) (e_1 o_1 : Lean.Expr) (n_1 : ℕ),
  (Nat.NatOffset.offset✝ e o n = Nat.NatOffset.offset✝ e_1 o_1 n_1) = (e = e_1 ∧ o = o_1 ∧ n = n_1)
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.x_one : ∀ {d : ℤ}, Pell.Solution₁.x 1 = 1
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `absorbs_biUnion_finset`. -/
Absorbs.biUnion_finset : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
  {I : Finset ι}, (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeMaxOrder.liftRight : {𝕆 : Type u_1} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [GradeMaxOrder 𝕆 β] →
              (f : α → β) →
                StrictMono f → (∀ (a b : α), a ⋖ b → f a ⋖ f b) → (∀ (a : α), IsMax a → IsMax (f a)) → GradeMaxOrder 𝕆 α
-- Lean.Language.Basic
Lean.Language.Snapshot.mk.injEq : ∀ (desc : autoParam String Lean.Language.Snapshot.desc._autoParam) (diagnostics : Lean.Language.Snapshot.Diagnostics)
  (infoTree? : Option Lean.Elab.InfoTree) (traces : Lean.TraceState) (isFatal : Bool)
  (desc_1 : autoParam String Lean.Language.Snapshot.desc._autoParam)
  (diagnostics_1 : Lean.Language.Snapshot.Diagnostics) (infoTree?_1 : Option Lean.Elab.InfoTree)
  (traces_1 : Lean.TraceState) (isFatal_1 : Bool),
  ({ desc := desc, diagnostics := diagnostics, infoTree? := infoTree?, traces := traces, isFatal := isFatal } =
      { desc := desc_1, diagnostics := diagnostics_1, infoTree? := infoTree?_1, traces := traces_1,
        isFatal := isFatal_1 }) =
    (desc = desc_1 ∧ diagnostics = diagnostics_1 ∧ infoTree? = infoTree?_1 ∧ traces = traces_1 ∧ isFatal = isFatal_1)
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.triples₂ : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [RingHomInvPair σ₁₂ σ₂₁], RingHomCompTriple σ₂₁ σ₁₂ (RingHom.id R₂)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.contains_eq_false_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice},
  s.contains pat = false ↔ ∀ (pos : s.Pos), ¬String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.sfinite : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → ∀ [MeasureTheory.SFinite μa], MeasureTheory.SFinite μb
-- Mathlib.Data.Multiset.ZeroCons
Multiset.inhabitedMultiset : {α : Type u_1} → Inhabited (Multiset α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Rotating right by a constant value.
 -/
Std.Tactic.BVDecide.BVUnOp.rotateRight : ℕ → Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (toContinuousMap : C(α, β)) (hasCompactSupport' : HasCompactSupport toContinuousMap.toFun)
  (toContinuousMap_1 : C(α, β)) (hasCompactSupport'_1 : HasCompactSupport toContinuousMap_1.toFun),
  ({ toContinuousMap := toContinuousMap, hasCompactSupport' := hasCompactSupport' } =
      { toContinuousMap := toContinuousMap_1, hasCompactSupport' := hasCompactSupport'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ico_of_le : ∀ {a b : ℝ}, a ≤ b → MeasureTheory.volume.real (Set.Ico a b) = b - a
-- Init.Prelude
List.brecOn.go : {α : Type u} →
  {motive : List α → Sort u_1} → (t : List α) → ((t : List α) → List.below t → motive t) → motive t ×' List.below t
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOn.pow`

---

Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticOn.fun_pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A}
  {s : Set E}, AnalyticOn 𝕜 f s → ∀ (n : ℕ), AnalyticOn 𝕜 (fun i => f i ^ n) s
-- Init.Core
PProd.mk.injEq : ∀ {α : Sort u} {β : Sort v} (fst : α) (snd : β) (fst_1 : α) (snd_1 : β),
  (⟨fst, snd⟩ = ⟨fst_1, snd_1⟩) = (fst = fst_1 ∧ snd = snd_1)
-- Init.Data.Array.Lemmas
/-- Variant of `foldl_push` with a side condition for the `stop` argument.  -/
Array.foldl_push' : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β} {xs : Array α} {a : α} {stop : ℕ},
  stop = xs.size + 1 → Array.foldl f init (xs.push a) 0 stop = f (Array.foldl f init xs) a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.sup_toSubalgebra_of_isAlgebraic_right : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [Algebra.IsAlgebraic K ↥E2],
  (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra