mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr σ (f + g) = AlternatingMap.domDomCongr σ f + AlternatingMap.domDomCongr σ g
-- Mathlib.Data.Fintype.EquivFin
_private.Mathlib.Data.Fintype.EquivFin.0.Infinite.natEmbeddingAux_injective : ∀ (α : Type u_4) [inst : Infinite α], Function.Injective (Infinite.natEmbeddingAux✝ α)
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.mk.sizeOf_spec : ∀ (elimInfo : Lean.Elab.Term.ElabElimInfo) (expectedType : Lean.Expr),
  sizeOf { elimInfo := elimInfo, expectedType := expectedType } = 1 + sizeOf elimInfo + sizeOf expectedType
-- Mathlib.Combinatorics.Enumerative.Bell
Multiset.bell_eq : ∀ (m : Multiset ℕ),
  m.bell =
    m.sum.factorial /
      ((Multiset.map (fun j => j.factorial) m).prod * ∏ j ∈ m.toFinset.erase 0, (Multiset.count j m).factorial)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.intCast : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (n : ℤ), (↑n).IsSymmetric
-- Init.Data.UInt.Lemmas
UInt8.le_or_lt : ∀ (a b : UInt8), a ≤ b ∨ b < a
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mulIndicator_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : One R] {U : Set X} (f : LocallyConstant X R)
  {a : X} (hU : IsClopen U), a ∉ U → (f.mulIndicator hU) a = 1
-- Mathlib.Data.Vector.Snoc
List.Vector.mapAccumr₂_nil : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {s : σ} {f : α → β → σ → σ × φ},
  List.Vector.mapAccumr₂ f List.Vector.nil List.Vector.nil s = (s, List.Vector.nil)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.neg_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  -spectrum R a = spectrum R (-a)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_norm_le : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedRing E]
  [inst_2 : NormedAlgebra 𝕜 E] (c : ℕ → 𝕜), ∀ n > 0, ‖FormalMultilinearSeries.ofScalars E c n‖ ≤ ‖c n‖
-- Mathlib.LinearAlgebra.Ray
/-- The ray of `someRayVector`.  -/
Module.Ray.someRayVector_ray : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : Module.Ray R M), ⟦x.someRayVector⟧ = x
-- Init.Data.Vector.Attach
Vector.pmap_eq_self : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Prop} {hp : ∀ a ∈ xs, p a} {f : (a : α) → p a → α},
  Vector.pmap f xs hp = xs ↔ ∀ (a : α) (h : a ∈ xs), f a ⋯ = a
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.GSMul.toSMul : {ιA : Type u_1} →
  {ιM : Type u_3} →
    (A : ιA → Type u_4) →
      (M : ιM → Type u_5) → [inst : VAdd ιA ιM] → [GradedMonoid.GSMul A M] → SMul (GradedMonoid A) (GradedMonoid M)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
/-- For two arrows `f₁ f₂ : U ⟶ V`, the arrows `i` such that `i ≫ f₁ = i ≫ f₂` forms a sieve.
 -/
CategoryTheory.Sieve.equalizer : {C : Type uC} → [inst : CategoryTheory.Category.{vC, uC} C] → {U V : C} → (U ⟶ V) → (U ⟶ V) → CategoryTheory.Sieve U
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.coeMatrix : {l : Type u_1} →
  {R : Type u_2} →
    [inst : DecidableEq l] →
      [inst_1 : Fintype l] → [inst_2 : CommRing R] → Coe (↥(Matrix.symplecticGroup l R)) (Matrix (l ⊕ l) (l ⊕ l) R)
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_neg : ∀ {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] [inst_2 : CategoryTheory.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G), (-α).app X = -α.app X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig → ℕ
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.Equivalence.toOrderIso_apply : ∀ {X : Type u} {Y : Type v} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (e : X ≌ Y) (x : X),
  e.toOrderIso x = e.functor.obj x
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_div : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α}, Filter.map₂ (fun x1 x2 => x1 / x2) f g = f / g
-- Mathlib.CategoryTheory.Category.ULift
/-- One half of the equivalence between `C` and `AsSmall C`.  -/
CategoryTheory.AsSmall.up : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.AsSmall C)
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.mk_fontaineTheta : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] (x : WittVector p (PreTilt R p)),
  (Ideal.Quotient.mk (Ideal.span {↑p})) ((WittVector.fontaineTheta R p) x) = (PreTilt.coeff 0) (x.coeff 0)
-- Mathlib.Algebra.Field.Basic
Field.isDomain : ∀ {K : Type u_1} [inst : Field K], IsDomain K
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.outsidePart.eq_1 : ∀ (p : DyckWord), p.outsidePart = if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯
-- Mathlib.Data.Num.Basic
/-- The predecessor of a `PosNum` as a `PosNum`. This means that `pred 1 = 1`.  -/
PosNum.pred : PosNum → PosNum
-- Init.Data.String.Slice
String.Slice.lines.lineMap : String.Slice → String.Slice
-- Init.Data.List.Find
List.find?_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → p a = true
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- When `[Zero X]`, the shift of a map `f : Fin n → X`
is a map `Fin (n + 1) → X` which sends `0` to `0` and `i.succ` to `f i`.  -/
SSet.Augmented.StandardSimplex.shiftFun : {n : ℕ} → {X : Type u_1} → [Zero X] → (Fin n → X) → Fin (n + 1) → X
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.coe_evalRingHom : ∀ {R : Type u} [inst : CommSemiring R] (r : R), ⇑(Polynomial.evalRingHom r) = Polynomial.eval r
-- Mathlib.Data.Sum.Interval
_private.Mathlib.Data.Sum.Interval.0.Finset.sumLift₂.match_1.splitter : {α₁ : Type u_1} →
  {α₂ : Type u_2} →
    {β₁ : Type u_3} →
      {β₂ : Type u_4} →
        (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) →
          (x : α₁ ⊕ α₂) →
            (x_1 : β₁ ⊕ β₂) →
              ((a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b)) →
                ((val : α₁) → (val_1 : β₂) → motive (Sum.inl val) (Sum.inr val_1)) →
                  ((val : α₂) → (val_1 : β₁) → motive (Sum.inr val) (Sum.inl val_1)) →
                    ((a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)) → motive x x_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.domRestrict.eq_1 : ∀ {M : Type u_1} {σ : Type u_4} [inst : Add M] {N : Type u_5} [inst_1 : Add N] [inst_2 : SetLike σ M]
  [inst_3 : AddMemClass σ M] (f : M →ₙ+ N) (S : σ), f.domRestrict S = f.comp (AddMemClass.subtype S)
-- Std.Http.Data.Method
/-- Search a resource.
Source: https://www.rfc-editor.org/rfc/rfc5323#section-2
 -/
Std.Http.Method.search : Std.Http.Method
-- Mathlib.Data.Sign.Defs
SignType.not_lt_neg_one : ∀ (a : SignType), ¬a < -1
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_eq_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a = ArchimedeanClass.mk b ↔ (∃ m, |b| ≤ m • |a|) ∧ ∃ n, |a| ≤ n • |b|
-- Mathlib.Tactic.IntervalCases
/-- Given `a, b`, prove `a ≱ b` or fail.  -/
Mathlib.Tactic.IntervalCases.Methods.proveLT : Mathlib.Tactic.IntervalCases.Methods → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.MinMaxOn
List.isSome_maxOn?_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α},
  x ∈ xs → (List.maxOn? f xs).isSome = true
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_nil : ∀ {α : Type u}, Stream'.WSeq.nil.destruct = Computation.pure none
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)},
  (∀ W' ∈ W, W'.ContainsIdentities) → (sInf W).ContainsIdentities
-- Lean.Expr
/-- Return `true` if `e` contains free variables.
This is a constant time operation.
 -/
Lean.Expr.hasFVar : Lean.Expr → Bool
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.mk.injEq : ∀ (lhs rhs : Lean.Expr) (rlhs rrhs : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (ofSemiring? : Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr))
  (lhs_1 rhs_1 : Lean.Expr) (rlhs_1 rrhs_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (ofSemiring?_1 : Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr)),
  ({ lhs := lhs, rhs := rhs, rlhs := rlhs, rrhs := rrhs, d := d, ofSemiring? := ofSemiring? } =
      { lhs := lhs_1, rhs := rhs_1, rlhs := rlhs_1, rrhs := rrhs_1, d := d_1, ofSemiring? := ofSemiring?_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ rlhs = rlhs_1 ∧ rrhs = rrhs_1 ∧ d = d_1 ∧ ofSemiring? = ofSemiring?_1)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_pow_eq : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ) (n : ℕ),
  MvPowerSeries.X s ^ n = (MvPowerSeries.monomial fun₀ | s => n) 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keysArray.size = t.size
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] {s : Set G},
  IsOpen s → IsOpen (-s)
-- Init.Data.List.ToArray
List.eraseIdxIfInBounds_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ), l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasStrictFDerivAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → f x ≠ 0 → HasStrictFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x
-- Mathlib.CategoryTheory.Shift.Quotient
/-- A relation on morphisms is compatible with the shift by a monoid `A` when the
relation if preserved by the shift.  -/
HomRel.IsCompatibleWithShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    HomRel C → (A : Type w) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Prop
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.valueGroup₀Fun_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w), h.valueGroup₀Fun 0 = 0
-- Init.Data.Int.Order
Int.zero_lt_one : 0 < 1
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_right_injective : ∀ {α : Type u_1} {n : ℕ}, n ≠ 0 → Function.Injective (Multiset.replicate n)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_inj : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, ↑I = ↑J ↔ I = J
-- Aesop.Tree.UnsafeQueue
Aesop.instInhabitedPostponedSafeRule : Inhabited Aesop.PostponedSafeRule
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_lt_norm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] (r : ℝ), ∃ x, r < ‖x‖
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.instFiniteSubtypeMem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) [Finite G], Finite ↥K
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHomClass.toZeroHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [inst_3 : ZeroHomClass F M N] (f : F), ↑f = { toFun := ⇑f, map_zero' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If the affine span of an affine independent finset is strictly contained in the affine span of
another finset, then its cardinality is strictly less than the cardinality of that finset.  -/
AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan : ∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  {s t : Finset V}, AffineIndependent k Subtype.val → affineSpan k ↑s < affineSpan k ↑t → s.card < t.card
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_map_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] {E : Type u_2} [inst_5 : EquivLike E S S₁]
  [AlgEquivClass E R S S₁] (P : Ideal S) (e : E), p.ramificationIdx' (Ideal.map e P) = p.ramificationIdx' P
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.comp_toRationalMap : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.RationalMap Y)
  [inst_2 : f.IsDominant] (h : Y ⟶ Z), f.comp (AlgebraicGeometry.Scheme.Hom.toRationalMap h) = f.compHom h
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_lt_nat_iff : ∀ {a : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} a < ↑n ↔ a < ↑n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {km : α}, t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_not_le : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a b : α} {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → ¬a ≤ b → ¬a' ≤ b'
-- Mathlib.Tactic.ITauto
/-- `(n: A) ⊢ A`  -/
Mathlib.Tactic.ITauto.Proof.hyp : Lean.Name → Mathlib.Tactic.ITauto.Proof
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.below.leaf : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1}
  {motive : (a : Std.DTreeMap.Internal.Impl α β) → (a_1 : Std.DTreeMap.Internal.Impl α β') → a.SameKeys a_1 → Prop},
  Std.DTreeMap.Internal.Impl.SameKeys.below ⋯
-- Lean.Declaration
Lean.ConstantInfo.defnInfo.sizeOf_spec : ∀ (val : Lean.DefinitionVal), sizeOf (Lean.ConstantInfo.defnInfo val) = 1 + sizeOf val
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.essFiniteType_iff_exists_subalgebra : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.EssFiniteType R S ↔ ∃ S₀ M, Algebra.FiniteType R ↥S₀ ∧ IsLocalization M S
-- Mathlib.Data.Seq.Defs
/-- A stream `s : Option α` is a sequence if `s.get n = none` implies `s.get (n + 1) = none`.
 -/
Stream'.IsSeq : {α : Type u} → Stream' (Option α) → Prop
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instReflectsIsomorphismsRestrictScalars : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (ModuleCat.restrictScalars f).ReflectsIsomorphisms
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_above_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], r.inertiaDeg S ∣ r.inertiaDeg R
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasProd.nonneg : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α]
  [inst_2 : Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] [L.NeBot] {f : ι → α},
  (∀ (i : ι), 0 ≤ f i) → ∀ {a : α}, HasProd f a L → 0 ≤ a
-- Mathlib.GroupTheory.Exponent
AddSubgroup.nsmul_exponent_eq_zero : ∀ {G : Type u} [inst : AddGroup G] {H : AddSubgroup G} {g : G}, g ∈ H → AddMonoid.exponent ↥H • g = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- the morphism between the underlying simplicial objects  -/
CategoryTheory.SimplicialObject.Split.Hom.F : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S₁ S₂ : CategoryTheory.SimplicialObject.Split C} → S₁.Hom S₂ → (S₁.X ⟶ S₂.X)
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a : ℝ} {γ : ℝ → M}, Manifold.pathELength I γ a a = 0
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_zero : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ], (DFinsupp.sumAddHom fun i => 0) = 0
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V), G.vertexCoverNum = ⨅ s, ⨅ (_ : G.IsVertexCover s), s.encard
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLE.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (x : WithBot α) (h_1 : (x : WithBot α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match none, x with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_1 x
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.scalingConstantOf.eq_1 : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ),
  IsUnifLocDoublingMeasure.scalingConstantOf μ K = max (Classical.choose ⋯) 1
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.compare_left_not_beq_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
    (k k').isGE = true → ∀ p ∈ l.toListModel, ¬(k p.fst == Ordering.eq) = true
-- Lean.Meta.Basic
/-- Returns `true` if the free variable is a let-variable with a visible local definition in the current local context
(using `Lean.LocalDecl.isLet`).

Setting `allowNondep := true` includes nondependent let declarations, whose values are normally hidden.
 -/
Lean.FVarId.isLetVar : Lean.FVarId → optParam Bool false → Lean.MetaM Bool
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.Quotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : SMul S M] (c : SMulCon S M), SMulCon.Quotient M c = Quotient c.toSetoid
-- Init.Internal.Order.Basic
Lean.Order.instOrderPi : {α : Sort u} → {β : α → Sort v} → [(x : α) → Lean.Order.PartialOrder (β x)] → Lean.Order.PartialOrder ((x : α) → β x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipPrefix?_slice_eq_some_iff : ∀ {pat s : String.Slice} {pos : s.Pos}, s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.topologicalClosure_map : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A]
  [inst_5 : IsSemitopologicalSemiring A] [inst_6 : TopologicalSpace B] [inst_7 : NonUnitalSemiring B]
  [inst_8 : Module R B] [inst_9 : IsTopologicalSemiring B] [inst_10 : ContinuousConstSMul R B]
  (s : NonUnitalSubalgebra R A) {φ : A →ₙₐ[R] B},
  IsClosedMap ⇑φ →
    Continuous ⇑φ → (NonUnitalSubalgebra.map φ s).topologicalClosure = NonUnitalSubalgebra.map φ s.topologicalClosure
-- Init.Data.List.Find
List.findFinIdx?.go.eq_def : ∀ {α : Type u} (p : α → Bool) (l l' : List α) (i : ℕ) (h : l'.length + i = l.length),
  List.findFinIdx?.go p l l' i h =
    match l', i, h with
    | [], x, x_1 => none
    | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else List.findFinIdx?.go p l l_1 (i + 1) ⋯
-- Mathlib.Algebra.RingQuot
RingQuot.lift_def : ∀ {R : Type u_1} [inst : Semiring R] {T : Type u_2} [inst_1 : Semiring T] {r : R → R → Prop},
  RingQuot.lift =
    { toFun := fun f => RingQuot.preLift ⋯, invFun := fun F => ⟨F.comp (RingQuot.mkRingHom r), ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.prop : ∀ {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] [P.IsClosedUnderColimitsOfShape J] {X : C} (h : P.ColimitOfShape J X),
  P X
-- Lean.Parser.Command
Lean.Parser.Command.extends.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Float.Model.Float
/-- Converts an `Int` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofInt : ℤ → Float.Model
-- Mathlib.FieldTheory.RatFunc.Basic
/-- A version of `num_div_dvd` with the LHS in simp normal form  -/
RatFunc.num_div_dvd' : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 → Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.unop_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.RightHomologyData), h.unop.H = Opposite.unop h.H
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Array.lex.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (as bs : Array α) (lt : α → α → Bool),
  as.lex bs lt =
    (do
        let __s ←
          forIn' (0...min as.size bs.size) (none, ()) fun i h __s =>
              have __r := __s;
              have this := ⋯;
              if lt as[i] bs[i] = true then pure (ForInStep.done (some true, ()))
              else
                if (as[i] != bs[i]) = true then pure (ForInStep.done (some false, ()))
                else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure (decide (as.size < bs.size))).run
-- Init.Data.Vector.Lemmas
Vector.isEqv_eq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {xs ys : Vector α n},
  ((xs.isEqv ys fun x1 x2 => x1 == x2) = true) = (xs = ys)
-- Lean.CoreM
Lean.Core.debug.moduleNameAtTimeout : Lean.Option Bool
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G},
  DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₂ x).1) x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comp_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂),
  (h.comp h').h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₂ h'.h₁
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instZSMul : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → SMul ℤ (SeparationQuotient G)