mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.id₂_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x : a ⟶ b},
  (CategoryTheory.CategoryStruct.id x).iso.hom = CategoryTheory.CategoryStruct.id x.of
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.response.sizeOf_spec : sizeOf Lean.JsonRpc.MessageKind.response = 1
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- For a morphism from a connected object `A` to a Galois object `B` and an automorphism
of `A`, there exists a unique automorphism of `B` making the canonical diagram commute.  -/
CategoryTheory.PreGaloisCategory.exists_autMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  (f : A ⟶ B) [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsGalois B]
  (σ : CategoryTheory.Aut A),
  ∃! τ, CategoryTheory.CategoryStruct.comp f τ.hom = CategoryTheory.CategoryStruct.comp σ.hom f
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The product cone induced by the concrete product.  -/
ModuleCat.productCone : {R : Type u} → [inst : Ring R] → {ι : Type v} → (Z : ι → ModuleCat R) → CategoryTheory.Limits.Fan Z
-- Batteries.Data.Fin.Lemmas
Fin.sum.eq_1 : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] (x : Fin n → α),
  Fin.sum x = Fin.foldr n (fun x1 x2 => x x1 + x2) 0
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_zero : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0},
  Finsupp.mapRange f hf 0 = 0
-- Mathlib.Combinatorics.Additive.Energy
Finset.card_sq_le_card_mul_addEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s t u : Finset α),
  {xy ∈ s ×ˢ t | xy.1 + xy.2 ∈ u}.card ^ 2 ≤ u.card * s.addEnergy t
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- **Alias** of `infEDist_cthickening`. -/
infEdist_cthickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (δ : ℝ) (s : Set E) (x : E),
  Metric.infEDist x (Metric.cthickening δ s) = Metric.infEDist x s - ENNReal.ofReal δ
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.uliftMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → Topology.IsEmbedding (ULift.map f)
-- Mathlib.GroupTheory.Finiteness
/-- If `f` `g` are homomorphisms from a canonically ordered and well-quasi-ordered monoid `M` to a
cancellative monoid `N`, the submonoid of `M` on which `f` and `g` agree is finitely generated.  -/
Submonoid.fg_eqLocusM : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M]
  [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] [inst_5 : Monoid N] [IsCancelMul N] (f g : M →* N),
  (f.eqLocusM g).FG
-- Init.Data.UInt.Lemmas
USize.toFin.eq_1 : ∀ (x : USize), x.toFin = x.toBitVec.toFin
-- Batteries.Recycling.RBTree.Basic
RBTree.RBColor.noConfusionType : Sort v✝ → RBTree.RBColor → RBTree.RBColor → Sort v✝
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.comp_L : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] (g : G)
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤),
  (X f).comp (smoothLeftMul I g) = X (f.comp (smoothLeftMul I g))
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.visitInc : Lean.Expr → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitEntry.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (key : Lean.Meta.LazyDiscrTree.Key) (entry : Lean.Meta.LazyDiscrTree.LazyEntry α),
  sizeOf { key := key, entry := entry } = 1 + sizeOf key + sizeOf entry
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} (f : X ⟶ Y)
  (h : W.TransfiniteCompositionOfShape J f), W.transfiniteCompositionsOfShape J f
-- Batteries.Data.Random.MersenneTwister
/-- Mersenne Twister configuration.

Letters in parentheses correspond to variable names used by Matsumoto and Nishimura (1998) and
Nishimura (2000).
 -/
Batteries.Random.MersenneTwister.Config : Type
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_add_one : ∀ {s : ℝ}, s ≠ 0 → Real.Gamma (s + 1) = s * Real.Gamma s
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) (x : WithAbs ↑v),
  (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv) { toCompletion := ↑x } =
    (NumberField.InfinitePlace.embedding_of_isReal hv) ((WithAbs.equiv ↑v) x)
-- Mathlib.Data.Num.Lemmas
PosNum.of_to_nat' : ∀ (n : PosNum), Num.ofNat' ↑n = Num.pos n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Mathlib.Geometry.Manifold.Instances.Real
instInhabitedEuclideanHalfSpace : {n : ℕ} → [inst : NeZero n] → Inhabited (EuclideanHalfSpace n)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_zero : ∀ {R : Type u_1} {a b u₀ : R} [inst : Mul R] [inst_1 : Add R], arithGeom a b u₀ 0 = u₀
-- Init.Meta.Defs
Lean.TSyntax.instCoeConsSyntaxNodeKind : {ks : Lean.SyntaxNodeKinds} → {k' : Lean.SyntaxNodeKind} → Coe (Lean.TSyntax ks) (Lean.TSyntax (k' :: ks))
-- Lean.Declaration
Lean.ConstructorVal.toConstantVal : Lean.ConstructorVal → Lean.ConstantVal
-- Mathlib.Topology.Order.LocalExtr
isLocalExtrOn_univ_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalExtrOn f Set.univ a ↔ IsLocalExtr f a
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.prodSwap_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α × β),
  ContinuousMap.prodSwap x = (x.2, x.1)
-- Mathlib.Logic.Encodable.Basic
Directed.sequence.eq_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] {r : β → β → Prop} (f : α → β)
  (hf : Directed r f) (x : ℕ),
  Directed.sequence f hf x =
    match x with
    | 0 => default
    | n.succ =>
      have p := Directed.sequence f hf n;
      match Encodable.decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_natCast_le_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.aleph ↑n ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph ↑n ≤ c
-- Mathlib.Data.Matrix.Reflection
Matrix.Exists.eq_def : ∀ {α : Type u_1} (x x_1 : ℕ) (x_2 : Matrix (Fin x) (Fin x_1) α → Prop),
  Matrix.Exists x_2 =
    match x, x_1, x_2 with
    | 0, x, P => P (Matrix.of ![])
    | n.succ, x, P => FinVec.Exists fun r => Matrix.Exists fun A => P (Matrix.of (Matrix.vecCons r A))
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
IsRegularCardinalOrder.type_lt_le_ord_cof : ∀ {α : Type u_2} {inst : LinearOrder α} {inst_1 : WellFoundedLT α} [self : IsRegularCardinalOrder α],
  (Ordinal.type fun x1 x2 => x1 < x2) ≤ (Order.cof α).ord
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
/-- `p ^ (n + 1)` divides
`x` minus the summation of the first `n + 1` terms of the Teichmuller series.
 -/
WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [inst_1 : CharP R p] [inst_2 : PerfectRing R p]
  (x : WittVector p R) (n : ℕ),
  ↑p ^ (n + 1) ∣ x - ∑ i ≤ n, (WittVector.teichmuller p) (((frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P],
  CategoryTheory.Limits.HasFiniteCoproducts (CompHausLike P)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)),
  edist μ ν = MeasureTheory.levyProkhorovEDist ↑μ.toMeasure ↑ν.toMeasure
-- Mathlib.Order.Basic
Decidable.le_iff_eq_or_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b ↔ a = b ∨ a < b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.zero_of_map_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X Y : C} (f : X ⟶ Y), F.map f = 0 → f = 0
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
IsLocalRing.ResidueField.algebraOfIsIntegral : {R : Type u_4} →
  {k : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] →
        [inst_2 : Field k] → [inst_3 : Algebra R k] → [Algebra.IsIntegral R k] → Algebra (IsLocalRing.ResidueField R) k
-- Mathlib.CategoryTheory.SingleObj
/-- The fully faithful functor from `MonCat` to `Cat`.  -/
MonCat.toCat : CategoryTheory.Functor MonCat CategoryTheory.Cat
-- Aesop.Tree.Data
Aesop.RappId.mk : ℕ → Aesop.RappId
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_sub_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.MeasurePreserving (fun t => g - t) μ μ
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_surjective_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Surjective ⇑f → Function.Surjective (Ideal.map f)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- Use linearity of `cramer` to take it out of a summation.  -/
Matrix.sum_cramer : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  {β : Type u_1} (s : Finset β) (f : β → n → α), ∑ x ∈ s, A.cramer (f x) = A.cramer (∑ x ∈ s, f x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.get? (t.maxD fallback) = some (t.maxD fallback)
-- Mathlib.CategoryTheory.Presentable.Directed
/-- `top` is terminal  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) →
        self.IsTerminal self.top
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsSelfAdjoint.spectrum_nonempty : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [Nontrivial A] {a : A}, IsSelfAdjoint a → (spectrum ℝ a).Nonempty
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_uIoo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.uIoo i j = Set.uIoo (i.addNat m) (j.addNat m)
-- Mathlib.Algebra.Ring.BooleanRing
/-- The join operation in a Boolean ring is `x + y + x * y`.  -/
BooleanRing.sup : {α : Type u_1} → [BooleanRing α] → Max α
-- Mathlib.RingTheory.Ideal.Operations
Ideal.finsuppTotal_apply_eq_of_fintype : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommGroup M] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Module R M]
  (I : Ideal R) {v : ι → M} [inst_3 : Fintype ι] (f : ι →₀ ↥I), (Ideal.finsuppTotal ι M I v) f = ∑ i, ↑(f i) • v i
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₄ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (h₀ : f.obj' 0 _proof_361✝ = g.obj' 0 _proof_361✝) (h₁ : f.obj' 1 _proof_362✝ = g.obj' 1 _proof_362✝)
  (h₂ : f.obj' 2 _proof_363✝ = g.obj' 2 _proof_363✝) (h₃ : f.obj' 3 _proof_364✝ = g.obj' 3 _proof_364✝)
  (h₄ : f.obj' 4 _proof_365✝ = g.obj' 4 _proof_365✝),
  f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
        (CategoryTheory.CategoryStruct.comp (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          (CategoryTheory.eqToHom ⋯)) →
    f.map' 1 2 _proof_246✝ _proof_363✝ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
          (CategoryTheory.CategoryStruct.comp (g.map' 1 2 _proof_246✝ _proof_363✝) (CategoryTheory.eqToHom ⋯)) →
      f.map' 2 3 _proof_299✝ _proof_364✝ =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
            (CategoryTheory.CategoryStruct.comp (g.map' 2 3 _proof_299✝ _proof_364✝) (CategoryTheory.eqToHom ⋯)) →
        f.map' 3 4 _proof_364✝ _proof_365✝ =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃)
              (CategoryTheory.CategoryStruct.comp (g.map' 3 4 _proof_364✝ _proof_365✝) (CategoryTheory.eqToHom ⋯)) →
          f = g
-- Init.Prelude
/-- Creates a `Fin n` from `i : Nat` and a proof that `i < n`.  -/
Fin.mk : {n : ℕ} → (val : ℕ) → val < n → Fin n
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.compCLM_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (R : Type u_3) (M : Type u_5)
  [inst_2 : TopologicalSpace M] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M] [inst_5 : ContinuousAdd M]
  [inst_6 : Module R M] [inst_7 : ContinuousConstSMul R M] (f : C(α, β)) (g : C(β, M)),
  (ContinuousMap.compCLM R M f) g = g.comp f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, Std.DTreeMap.Const.get? (t.insert k v) k = some v
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `L` and `R` are semilinear maps whose composite is linear, and `f` is differentiable at
`R z`, then `L ∘ f ∘ R` is differentiable at `z`.  -/
DifferentiableAt.comp_semilinear₂ : ∀ {𝕜 : Type u_1} {V : Type u_2} {V' : Type u_3} {W : Type u_4} {W' : Type u_5} [inst : NontriviallyNormedField 𝕜]
  {σ σ' : 𝕜 →+* 𝕜} [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup V']
  [inst_4 : NormedSpace 𝕜 V'] [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W]
  [inst_7 : NormedAddCommGroup W'] [inst_8 : NormedSpace 𝕜 W'] [RingHomIsometric σ] [RingHomInvPair σ σ']
  (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {z : V'},
  DifferentiableAt 𝕜 f (R z) → DifferentiableAt 𝕜 (⇑L ∘ f ∘ ⇑R) z
-- Mathlib.Order.SuccPred.IntervalSucc
/-- Union formula for `Set.Ioc (f i) (f (Order.succ i))` over `i ∈ Ici a`. See also
`iUnion_Ioc_map_succ_eq_Ioi` for the specialization `a = ⊥`.  -/
biUnion_Ici_Ioc_map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α]
  [inst_3 : LinearOrder β] {f : α → β} {a : α},
  (∀ i ∈ Set.Ici a, f a ≤ f i) →
    ¬BddAbove (f '' Set.Ici a) → ⋃ i ∈ Set.Ici a, Set.Ioc (f i) (f (Order.succ i)) = Set.Ioi (f a)
-- Mathlib.Algebra.Homology.Single
/-- Morphisms from a single object chain complex with `X` concentrated in degree 0
to an `ℕ`-indexed chain complex `C` are the same as morphisms `f : X → C.X 0`.
 -/
ChainComplex.fromSingle₀Equiv : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : ChainComplex V ℕ) → (X : V) → ((ChainComplex.single₀ V).obj X ⟶ C) ≃ (X ⟶ C.X 0)
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_cons : ∀ {x : ℤ} {xs : List ℤ}, Lean.Omega.IntList.gcd (x :: xs) = x.natAbs.gcd (Lean.Omega.IntList.gcd xs)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.recordSimpTheorem : Lean.Meta.Origin → Lean.Meta.SimpM Unit
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_coweightMap_apply : ∀ {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (x : N₂),
  (g.comp f).coweightMap x = f.coweightMap (g.coweightMap x)
-- Mathlib.Algebra.Order.Star.Basic
/-- **Alias** of `IsSelfAdjoint.of_ge`. -/
IsSelfAdjoint.mono : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, x ≤ y → IsSelfAdjoint x → IsSelfAdjoint y
-- Mathlib.Data.Set.Lattice
Set.iInter_union_of_monotone : ∀ {ι : Type u_12} {α : Type u_13} [inst : Preorder ι] [IsCodirectedOrder ι] {s t : ι → Set α},
  Monotone s → Monotone t → ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i
-- Mathlib.Topology.Algebra.Algebra
/-- The Cartesian product of two continuous algebra morphisms as a continuous algebra morphism.  -/
ContinuousAlgHom.prod : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    {C : Type u_4} →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] →
                          [inst_9 : TopologicalSpace C] → (A →A[R] B) → (A →A[R] C) → A →A[R] B × C
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_cons_tail : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} (s : Multiset α), b ≠ a → (b ::ₘ s).erase a = b ::ₘ s.erase a
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The equivalence between `(Fin 2 → ℤ)` and `Σ n : ℕ, gammaSet 1 n 0)` .  -/
EisensteinSeries.gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (r : ℕ) × ↑(EisensteinSeries.gammaSet 1 r 0)
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_nonneg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  (I : FractionalIdeal (nonZeroDivisors R) K), 0 ≤ FractionalIdeal.absNorm I
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∩ t = t ∩ s
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_halt : Turing.PartrecToTM2.contSupp Turing.PartrecToTM2.Cont'.halt = ∅
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.empty : {α : outParam (Type u)} → {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β
-- Mathlib.Order.Zorn
Flag.instNonempty : ∀ {α : Type u_1} [inst : Preorder α], Nonempty (Flag α)
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.holder : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] {e : (i : ι) → E i} {f : (i : ι) → F i},
  Memℓp e p →
    Memℓp f q →
      ∀ (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ}, (∀ (i : ι), ‖B i‖ ≤ K) → Memℓp (fun i => ((B i) (e i)) (f i)) r
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_congr : ∀ {f g : ℕ → ℂ}, (∀ {n : ℕ}, n ≠ 0 → f n = g n) → ∀ (s : ℂ) (n : ℕ), LSeries.term f s n = LSeries.term g s n
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toNonUnitalSubalgebra_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective Subalgebra.toNonUnitalSubalgebra
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.support_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  (p.transfer H hp).support = p.support
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.State.mk.inj : ∀ {steps : ℕ} {infos : Lean.SubExpr.PosMap Lean.Elab.Info}
  {holeIter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator} {steps_1 : ℕ}
  {infos_1 : Lean.SubExpr.PosMap Lean.Elab.Info} {holeIter_1 : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator},
  { steps := steps, infos := infos, holeIter := holeIter } =
      { steps := steps_1, infos := infos_1, holeIter := holeIter_1 } →
    steps = steps_1 ∧ infos = infos_1 ∧ holeIter = holeIter_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter! m₂) = true},
  (m₁.inter! m₂).get k h_contains = m₁.get k ⋯
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G), CategoryTheory.IsIso e.inv.toNatTrans
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f)[k]? = Option.map f t[k]?
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.Existence.instIsLocalHomCarrierRingHomHomHomCommRingCat : ∀ {R S : CommRingCat} (e : R ≅ S), IsLocalHom (CommRingCat.Hom.hom e.hom)