mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.of_isoObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)},
  F.IsRepresentedBy x →
    ∀ {Y : C} (e : Y ≅ X), F.IsRepresentedBy ((CategoryTheory.ConcreteCategory.hom (F.map e.hom.op)) x)
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAnti_comp_ofDual_iff`. -/
StrictMono.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → StrictAnti (f ∘ ⇑OrderDual.ofDual)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roc : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toList[i]? = if i < (n - m).toNat then some (m + 1 + ↑i) else none
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `UInt32` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofUInt32 : Float.Model.Format → UInt32 → Float.Model.UnpackedFloat
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.ofSubtype.match_1.eq_1 : ∀
  (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) → (p : α.Arrow (TypeVec.repeat n Prop)) → (x : Fin2 n) → TypeVec.Subtype_ p x → Sort u_2)
  (n : ℕ) (α : TypeVec.{u_1} (n + 1)) (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) (i : Fin2 n)
  (x : TypeVec.Subtype_ p i.fs)
  (h_1 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
          (i : Fin2 n) → (x : TypeVec.Subtype_ p i.fs) → motive (n + 1) α p i.fs x)
  (h_2 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) → (x : TypeVec.Subtype_ p Fin2.fz) → motive (n + 1) α p Fin2.fz x),
  (match n + 1, α, p, i.fs, x with
    | .(n + 1), α, p, i.fs, x => h_1 n α p i x
    | .(n + 1), α, p, Fin2.fz, x => h_2 n α p x) =
    h_1 n α p i x
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_X : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {s : σ}, m.Monic (MvPolynomial.X s)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_4 x
-- Mathlib.Data.EReal.Inv
EReal.top_div_of_pos_ne_top : ∀ {a : EReal}, 0 < a → a ≠ ⊤ → ⊤ / a = ⊤
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_le_im`. -/
Complex.frontier_setOf_le_im : ∀ (a : ℝ), frontier {z | a ≤ z.im} = {z | z.im = a}
-- Mathlib.Data.Seq.Computation
Computation.tail_empty : ∀ {α : Type u}, (Computation.empty α).tail = Computation.empty α
-- Mathlib.Algebra.Group.Basic
one_div_one : ∀ {G : Type u_3} [inst : DivInvOneMonoid G], 1 / 1 = 1
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.enorm_LpToLpOfMeasureLeSMulₗ_apply_le : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal} (hc : c ≠ ⊤)
  (h : μ ≤ c • ν) [inst_2 : Fact (1 ≤ p)] {f : ↥(MeasureTheory.Lp E p ν)},
  ‖(MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ✝ hc h) f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ
-- Init.Grind.Attr
/-- The `ext` modifier marks extensionality theorems for use by `grind`.
For example, the standard library marks `funext` with this attribute.

Whenever `grind` encounters a disequality `a ≠ b`, it attempts to apply any
available extensionality theorems whose matches the type of `a` and `b`.
 -/
Lean.Parser.Attr.grindExt : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The interior of a fundamental domain, those points of the domain not lying in any translate.  -/
MeasureTheory.fundamentalInterior : (G : Type u_1) → {α : Type u_3} → [inst : Group G] → [MulAction G α] → Set α → Set α
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `QuotientMeasureEqMeasurePreimage`.  -/
IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] {V : Set (G ⧸ Γ)},
      (interior V).Nonempty →
        MeasurableSet V →
          μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕) → μ V ≠ ⊤ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.Order.Monotone.Defs
StrictMono.imp : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  StrictMono f → a < b → f a < f b
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.liftCoborder_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f]
  (U : (↑(AlgebraicGeometry.Scheme.Hom.coborderRange f)).Opens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.liftCoborder f) U =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app f
        ((AlgebraicGeometry.Scheme.Hom.opensFunctor (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι).obj U))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.instIsComonHomComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N O : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.ComonObj N] [inst_4 : CategoryTheory.ComonObj O]
  (f : M ⟶ N) (g : N ⟶ O) [CategoryTheory.IsComonHom f] [CategoryTheory.IsComonHom g],
  CategoryTheory.IsComonHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.postcomp_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ} (self : d.Universal)
  {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
  d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
-- Lean.Compiler.ExportAttr
Lean.getExportNameFor? : Lean.Environment → Lean.Name → Option Lean.Name
-- Aesop.Rule.Forward
/-- The priority of a forward rule.  -/
Aesop.ForwardRulePriority : Type
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift : ∀ {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f),
  (AddCommGrpCat.HasLimit.productLimitCone f).isLimit.lift s = AddCommGrpCat.HasLimit.lift f s
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcomp_functor : ∀ {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] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] (a : A),
  (F.postcomp G).functor a = (F.functor a).comp G
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLT! : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α → α × β
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_adj_mul_iff_right : ∀ {M : Type u_1} [inst : Semigroup M] [IsLeftCancelMul M] {s : Set M} {u v d : M},
  (SimpleGraph.mulCayley s).Adj (d * u) (d * v) ↔ (SimpleGraph.mulCayley s).Adj u v
-- Mathlib.Order.Ideal
Order.Cofinal.instMembership : {P : Type u_1} → [inst : Preorder P] → Membership P (Order.Cofinal P)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₀ = h₀
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacksAgainst.hasPullbacksAlong : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P P' : CategoryTheory.MorphismProperty C}
  [self : P.HasPullbacksAgainst P'] ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.HasPullbacksAlong f
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k'
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_subset_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t₁ t₂ : Finset β},
  t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- Semigroup structure on additive submonoids of a (possibly, non-unital) semiring.  -/
AddSubmonoid.semigroup : {R : Type u_2} → [inst : NonUnitalSemiring R] → Semigroup (AddSubmonoid R)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (n : WithTop ℕ∞) (f : M → M'),
  ContMDiff I I' n f = ∀ (x : M), ContMDiffAt I I' n f x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.LinearAlgebra.DFinsupp
/-- **Alias** of `iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero`. -/
iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  (p : ι → Submodule R N),
  iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
-- Init.Prelude
/-- The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 -/
Nat : Type
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.toList_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m], (Std.IterM.empty m β).toList = pure []
-- Init.Data.Int.Order
Int.eq_negSucc_of_lt_zero : ∀ {a : ℤ}, a < 0 → ∃ n, a = Int.negSucc n
-- Init.Data.UInt.Lemmas
instAssociativeUInt64HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndepOn_finset_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {s : Finset ι},
  ¬LinearIndepOn R v ↑s ↔ ∃ f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = true},
  (m₁.diff m₂ ⋯).getKey k h_contains = m₁.getKey k ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isRestriction_iff_exists : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M ↔ ∃ R ⊆ M.E, N = M.restrict R
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.partition_zero_parts : ∀ (p : Nat.Partition 0), p.parts = 0
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAtChain_iff_toList : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain c pos pos' ↔
    ∃ (h : pos ≤ pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.toList.length c
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAtChain_startPos_endPos_iff : ∀ {pat s : String.Slice},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat s.startPos s.endPos ↔
    ∃ n, s.copy = String.join (List.replicate n pat.copy)
-- Mathlib.Control.LawfulFix
Part.fix_eq_of_ωScottContinuous : ∀ {α : Type u_1} {β : α → Type u_2} {g : ((a : α) → Part (β a)) → (a : α) → Part (β a)},
  OmegaCompletePartialOrder.ωScottContinuous g → Part.fix g = g (Part.fix g)
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.mapEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_4} {N' : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_6)
  [inst_11 : CommSemiring Rₛ] [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N']
  [inst_15 : IsScalarTower R Rₛ M'] [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ] (e : M ≃ₗ[R] N)
  (a : M'), (IsLocalizedModule.mapEquiv S f g Rₛ e) a = ((IsLocalizedModule.map S f g) ↑e) a
-- Mathlib.RingTheory.FinitePresentation
/-- `R` is finitely presented as `R`-algebra.  -/
Algebra.FinitePresentation.self : ∀ (R : Type w₁) [inst : CommRing R], Algebra.FinitePresentation R R
-- Mathlib.Data.Matrix.Basic
/-- The ring homomorphism `α →+* Matrix n n α`
sending `a` to the diagonal matrix with `a` on the diagonal.
 -/
Matrix.scalar : {α : Type u_11} →
  [inst : Semiring α] → (n : Type u) → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → α →+* Matrix n n α
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A modification of the valuation, sending `0` to `⊥` instead of `⊤`.  -/
IsDiscreteValuationRing.toWithBotNat : {R : Type u_2} → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → R → WithBot ℕ
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Transfer divided powers under an equivalence  -/
DividedPowers.ofRingEquiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommSemiring A] →
      {I : Ideal A} →
        [inst_1 : CommSemiring B] →
          {J : Ideal B} → {e : A ≃+* B} → Ideal.map e I = J → DividedPowers I → DividedPowers J
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.mono : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A B : Set (G × G)} {x₁ y₁ x₂ y₂ : G},
  A ⊆ B → IsCorner A x₁ y₁ x₂ y₂ → IsCorner B x₁ y₁ x₂ y₂
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, a / b < 1 ↔ a < b
-- Std.Time.Format.Modifier
/-- Full form of zone name (e.g., "Pacific Standard Time")
 -/
Std.Time.ZoneName.full : Std.Time.ZoneName
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_right_of_lt_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀],
  0 < a → a < 1 → m < n → a ^ n < a ^ m
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_nonneg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  0 ≤ MeasureTheory.Measure.haar.addCHaar K₀ K
-- Batteries.Data.UInt
UInt16.toNat_max : ∀ (x y : UInt16), (x ⊔ y).toNat = max x.toNat y.toNat
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {g : a ⟶ c} {h : b ⟶ d} {l₁ l₂ : a ⟶ b} {l₃ : c ⟶ d}
  (α : l₂ ⟶ l₁) (β : CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h),
  CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp α β =
    CategoryTheory.CategoryStruct.comp β (CategoryTheory.Bicategory.whiskerRight α h)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.whiskerLeft₂_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u_1} {B : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} A]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} B] (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D)
  (F : CategoryTheory.Functor A C) (G : CategoryTheory.Functor B D) (X : A) {X_1 Y : Bᵒᵖ} (f : X_1 ⟶ Y),
  ((P.whiskerLeft₂ F G).obj X).map f = (P.obj (F.obj X)).map (G.map f.unop).op
-- Mathlib.Data.Finset.NoncommProd
/-- Proof used in definition of `Finset.noncommProd`  -/
Finset.noncommProd_lemma : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β),
  (↑s).Pairwise (Function.onFun Commute f) → {x | x ∈ Multiset.map f s.val}.Pairwise Commute
-- Mathlib.LinearAlgebra.Pi
LinearMap.apply_single : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : DecidableEq ι]
  (f : (i : ι) → φ i →ₗ[R] M) (i j : ι) (x : φ i), (f j) (Pi.single i x j) = Pi.single i ((f i) x) j
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.ι_evalHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  (x_1 : ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).obj).obj U),
  (CategoryTheory.ConcreteCategory.hom (smoothSheaf.evalHom IM I N x))
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).obj)
            U))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom (TypeCat.ofHom (smoothSheaf.evalAt IM I N x (Opposite.unop U)))) x_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceEq : Lean.Meta.Simp.Simproc
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  t.alter k f ≠ ∅ →
    ∀ {fallback : α}, (t.alter k f).minKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.Abelian.coimageImageComparison f = CategoryTheory.Abelian.coimageImageComparison' f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_sInf : ∀ {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)} {x : R}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.CategoryTheory.EpiMono
/-- A split epi which is mono is an iso.  -/
CategoryTheory.isIso_of_mono_of_isSplitEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f]
  [CategoryTheory.IsSplitEpi f], CategoryTheory.IsIso f
-- Mathlib.Tactic.MoveAdd
/-- `getExprInputs e` inspects the outermost constructor of `e` and returns the array of all the
arguments to that constructor that are themselves `Expr`essions.  -/
Lean.Expr.getExprInputs : Lean.Expr → Array Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_X_self : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (j : σ) (f : MvPolynomial σ R),
  MvPolynomial.degreeOf j (f * MvPolynomial.X j) ≤ MvPolynomial.degreeOf j f + 1
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.symm : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (self : RootPairing.RootPositiveForm S P), LinearMap.IsSymm self.form
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- Relationship between the Fibonacci Sequence, the golden ratio, and its conjugate's exponents.  -/
Real.fib_succ_sub_goldenRatio_mul_fib : ∀ (n : ℕ), ↑(Nat.fib (n + 1)) - Real.goldenRatio * ↑(Nat.fib n) = Real.goldenConj ^ n
-- ProofWidgets.Presentation.Expr
_private.ProofWidgets.Presentation.Expr.0.ProofWidgets.evalExprPresenterUnsafe : Lean.Environment → Lean.Options → Lean.Name → Except String ProofWidgets.ExprPresenter