mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.ker_localizedMap_eq_localized₀_ker : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] {P : Type u_5} [inst_6 : AddCommMonoid P] [inst_7 : Module R P] {Q : Type u_6}
  [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q] (f' : P →ₗ[R] Q) [inst_10 : IsLocalizedModule p f'] (g : M →ₗ[R] P),
  ((IsLocalizedModule.map p f f') g).ker = Submodule.localized₀ p f g.ker
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of a formal power series `φ` is the greatest `n : ℕ∞`
such that `X^n` divides `φ`. The order is `⊤` if and only if `φ = 0`.  -/
PowerSeries.order : {R : Type u_1} → [Semiring R] → PowerSeries R → ℕ∞
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.ofEquiv : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : Module R M] [inst_4 : Module R N] (e : M ≃ₗ[R] N), IsBaseChange R ↑e
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- To prove something for an arbitrary `Lp` function in a second countable Borel normed group, it
suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in `Lp` for which the property holds is closed.
 -/
MeasureTheory.Lp.induction : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ (motive : ↥(MeasureTheory.Lp E p μ) → Prop),
      (∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
          motive ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) →
        (∀ ⦃f g : α → E⦄ (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
            Disjoint (Function.support f) (Function.support g) →
              motive (MeasureTheory.MemLp.toLp f hf) →
                motive (MeasureTheory.MemLp.toLp g hg) →
                  motive (MeasureTheory.MemLp.toLp f hf + MeasureTheory.MemLp.toLp g hg)) →
          IsClosed {f | motive f} → ∀ (f : ↥(MeasureTheory.Lp E p μ)), motive f
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The total complex shape for `c₂`, `c₁` and `c₁₂` that is deduced
from a total complex shape for `c₁`, `c₂` and `c₁₂`.  -/
TotalComplexShape.symm : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → TotalComplexShape c₂ c₁ c₁₂
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.cont : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsBrownianReal._auto_1},
  ProbabilityTheory.IsBrownianReal X P → ∀ᵐ (ω : Ω) ∂P, Continuous fun x => X x ω
-- Mathlib.Order.UpperLower.CompleteLattice
upperSetIsoLowerSet_apply : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), upperSetIsoLowerSet s = s.compl
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingularLift_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (a b : R),
  W'.NonsingularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Nonsingular a b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.drop_isSubwalk_drop : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {n k : ℕ} (p : G.Walk u v), n ≤ k → (p.drop k).IsSubwalk (p.drop n)
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If a group with zero has continuous inversion, then the inversion map restricts to an
auto-homeomorphism on the set of nonzero elements.  -/
Homeomorph.inv₀ : (G₀ : Type u_3) →
  [inst : GroupWithZero G₀] → [inst_1 : TopologicalSpace G₀] → [ContinuousInv₀ G₀] → { g // g ≠ 0 } ≃ₜ { g // g ≠ 0 }
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Continuous g)
  (K : TopologicalSpace.NonemptyCompacts α),
  TopologicalSpace.NonemptyCompacts.map (f ∘ g) ⋯ K =
    TopologicalSpace.NonemptyCompacts.map f hf (TopologicalSpace.NonemptyCompacts.map g hg K)
-- Mathlib.Order.Cover
WCovBy.of_le_of_le' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c ⩿ a → b ≤ a → c ≤ b → c ⩿ b
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.view : Lean.Elab.Tactic.ElimTargetInfo✝ → Lean.Elab.Tactic.ElimTargetView
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.mk.inj : ∀ {C₀ : Type u₀} {C : Type u} {inst : CategoryTheory.Category.{v₀, u₀} C₀} {inst_1 : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Functor C₀ C} {S : C} {I₀ : Type w} {X : I₀ → C₀} {f : (i : I₀) → F.obj (X i) ⟶ S}
  {I₁ : I₀ → I₀ → Type w} {Y : ⦃i₁ i₂ : I₀⦄ → I₁ i₁ i₂ → C₀} {p₁ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₁}
  {p₂ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₂}
  {w :
    ∀ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (F.map (p₁ j)) (f i₁) =
        CategoryTheory.CategoryStruct.comp (F.map (p₂ j)) (f i₂)}
  {I₀_1 : Type w} {X_1 : I₀_1 → C₀} {f_1 : (i : I₀_1) → F.obj (X_1 i) ⟶ S} {I₁_1 : I₀_1 → I₀_1 → Type w}
  {Y_1 : ⦃i₁ i₂ : I₀_1⦄ → I₁_1 i₁ i₂ → C₀} {p₁_1 : ⦃i₁ i₂ : I₀_1⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ X_1 i₁}
  {p₂_1 : ⦃i₁ i₂ : I₀_1⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ X_1 i₂}
  {w_1 :
    ∀ ⦃i₁ i₂ : I₀_1⦄ (j : I₁_1 i₁ i₂),
      CategoryTheory.CategoryStruct.comp (F.map (p₁_1 j)) (f_1 i₁) =
        CategoryTheory.CategoryStruct.comp (F.map (p₂_1 j)) (f_1 i₂)},
  { I₀ := I₀, X := X, f := f, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } =
      { I₀ := I₀_1, X := X_1, f := f_1, I₁ := I₁_1, Y := Y_1, p₁ := p₁_1, p₂ := p₂_1, w := w_1 } →
    I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1 ∧ I₁ ≍ I₁_1 ∧ Y ≍ Y_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1
-- Lean.Meta.Tactic.Grind.Types
/-- Cached extensionality theorems for types.  -/
Lean.Meta.Grind.GoalState.extThms : Lean.Meta.Grind.GoalState → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem)
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.smul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivAt c c' x → ∀ (f : F), HasDerivAt (fun y => c y • f) (c' • f) x
-- Init.Data.List.Nat.TakeDrop
List.lt_length_right_of_zip : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {l : List α} {l' : List β}, i < (l.zip l').length → i < l'.length
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
IsDiscrete.biUnion_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {I : Finset ι} {s : ι → Set X},
  (∀ i ∈ I, IsDiscrete (s i)) → (∀ i ∈ I, IsClosed (s i)) → IsDiscrete (⋃ i ∈ I, s i)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T : Submonoid P}
  (Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q] (h : R ≃+* P)
  (H : Submonoid.map h.toMonoidHom M = T) (a : S),
  (IsLocalization.ringEquivOfRingEquiv S Q h H) a = (IsLocalization.map Q ↑h ⋯) a
-- Mathlib.Condensed.Discrete.Basic
/-- The underlying object of a condensed object in `C` is the condensed object evaluated at a point.
This can be viewed as a sort of forgetful functor from `Condensed C` to `C`
 -/
Condensed.underlying : (C : Type w) → [inst : CategoryTheory.Category.{u + 1, w} C] → CategoryTheory.Functor (Condensed C) C
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeEquivSubtypePerm_apply_of_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (h : p a),
  ↑((Equiv.Perm.subtypeEquivSubtypePerm p) f) a = ↑(f ⟨a, h⟩)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.toPiLocalization_injective : ∀ (R : Type u_1) [inst : CommSemiring R], Function.Injective ⇑(MaximalSpectrum.toPiLocalization R)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filterM : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n] [LawfulMonad n]
  [WeaklyLawfulMonadAttach n] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ}
  {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterM f it) =
    Std.IterM.foldM
      (fun d b => do
        let __do_lift ← f b
        pure (if __do_lift.down = true then g d b else d))
      init it
-- Lean.Message
/-- A `BaseMessage` is a richly formatted piece of information emitted by Lean.
They are rendered by client editors in the infoview and in diagnostic windows.
There are two varieties in the Lean core:
* `Message`: Uses structured, effectful `MessageData` for formatting content.
* `SerialMessage`: Stores pure `String` data. Obtained by running the effectful
`Message.serialize`.
 -/
Lean.BaseMessage : Type u → Type u
-- Mathlib.Algebra.Group.Hom.Basic
MulHom.mul_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : CommSemigroup P]
  (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N), (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.specializes_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, s ⤳ closure s
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.mem_op : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : Aᵐᵒᵖ}
  {S : Subalgebra R A}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_iff_existsUnique_neg_add_mem : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! s, -↑s + g ∈ T
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.toMulOneClass.eq_1 : ∀ {M : Type u_4} [inst : MulOneClass M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] (S : A),
  SubmonoidClass.toMulOneClass S =
    { toOne := OneMemClass.one S, toMul := MulMemClass.mul S, one_mul := ⋯, mul_one := ⋯ }
-- Lean.Elab.Tactic.Doc
_private.Lean.Elab.Tactic.Doc.0.Lean.Elab.Tactic.Doc.firstTacticTokens.addFirstTokens : Lean.Parser.ParserCategory → Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ) → Lean.NameMap String → Lean.NameMap String
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- The `RelStruct f' g' i` deduced from `r : RelStruct f g i` when
`f = f'` and `g = g'`.  -/
SSet.PtSimplex.RelStruct.copy : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g : X.PtSimplex n x} →
        {i : Fin (n + 1)} → f.RelStruct g i → {f' g' : X.PtSimplex n x} → f = f' → g = g' → f'.RelStruct g' i
-- Mathlib.Analysis.CStarAlgebra.Classes
StarSubalgebra.commCStarAlgebra : {S : Type u_1} →
  {A : Type u_2} →
    [inst : CommCStarAlgebra A] →
      [inst_1 : SetLike S A] →
        [SubringClass S A] →
          [SMulMemClass S ℂ A] → [StarMemClass S A] → (s : S) → [h_closed : IsClosed ↑s] → CommCStarAlgebra ↥s
-- Mathlib.Data.Set.NAry
Set.image2_assoc : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {s : Set α} {t : Set β}
  {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
    Set.image2 f (Set.image2 g s t) u = Set.image2 f' s (Set.image2 g' t u)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} {s : Set E}
  {x : E} [Finite ι],
  DifferentiableWithinAt 𝕜 f s x →
    (∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x) →
      DifferentiableWithinAt 𝕜 (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x) s x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.toMatrix'_comp`. -/
QuadraticForm.QuadraticMap.toMatrix'_comp : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {m : Type w} [inst_4 : DecidableEq m] [inst_5 : Fintype m] (Q : QuadraticForm R (m → R)) (f : (n → R) →ₗ[R] m → R),
  QuadraticForm.toMatrix' (QuadraticMap.comp Q f) =
    (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.aux2 : ∀ {a b c : ℕ}, b < c * a → b % c < c
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.nullSingletonClass_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  (f : α → ENNReal), MeasureTheory.NullSingletonClass (μ.withDensity f)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over
the two morphisms `∐ I.left ⇉ ∐ I.right`. This is the diagram of the latter.
 -/
CategoryTheory.Limits.MultispanIndex.parallelPairDiagram : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [CategoryTheory.Limits.HasCoproduct I.left] →
          [CategoryTheory.Limits.HasCoproduct I.right] →
            CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Mathlib.Algebra.Group.Defs
CommGroup.mk : {G : Type u} → [toGroup : Group G] → (∀ (a b : G), a * b = b * a) → CommGroup G
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- **Alias** of `CategoryTheory.Limits.Types.isInitialPEmpty`.

---

The initial object in `Type u` is `PEmpty`.  -/
CategoryTheory.Limits.Types.isInitialPunit : CategoryTheory.Limits.IsInitial PEmpty.{u + 1}
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.push_log_last : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
    Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])
-- Mathlib.Data.List.Defs
/-- Runs a function over two lists returning the intermediate results and a final result.  -/
List.mapAccumr₂ : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α → β → γ → γ × δ) → List α → List β → γ → γ × List δ
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bodyInterest : {β : Type} → Bool → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toCostructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.toCostructuredArrow F).obj c = CategoryTheory.CostructuredArrow.mk c.π
-- Mathlib.RingTheory.Polynomial.Basic
/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself  -/
Ideal.polynomial_mem_ideal_of_coeff_mem_ideal : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R),
  (∀ (n : ℕ), p.coeff n ∈ Ideal.comap Polynomial.C I) → p ∈ I
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.prod.eq_1 : ∀ {ι : Type u} (f : ι → Cardinal.{u_1}), Cardinal.prod f = Cardinal.mk ((i : ι) → Quotient.out (f i))
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.instInhabitedHandleOverlapState : Inhabited Lean.Server.FileWorker.HandleOverlapState✝
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instWellFoundedRelation : {s : String.Slice} → WellFoundedRelation (String.Slice.Pattern.ForwardSliceSearcher s)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod.eq_2 : ∀ (p i : ℕ), LucasLehmer.sMod p i.succ = (LucasLehmer.sMod p i ^ 2 - 2) % (2 ^ p - 1)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- The canonical natural transformation `L ⋙ F.totalLeftDerived L W ⟶ F`.  -/
CategoryTheory.Functor.totalLeftDerivedCounit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (F : CategoryTheory.Functor C H) →
              (L : CategoryTheory.Functor C D) →
                (W : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L.IsLocalization W] →
                    [inst_4 : F.HasLeftDerivedFunctor W] → L.comp (F.totalLeftDerived L W) ⟶ F
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ : Measure α` is invariant under a multiplicative action of `M` on `α` if for any
measurable set `s : Set α` and `c : M`, the measure of its preimage under `fun x => c • x` is equal
to the measure of `s`.  -/
MeasureTheory.SMulInvariantMeasure : (M : Type u_1) → (α : Type u_2) → [SMul M α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.Algebra.MvPolynomial.CommRing
/-- Ring homomorphisms out of integer polynomials on a type `σ` are the same as
functions out of the type `σ`.  -/
MvPolynomial.homEquiv : {S : Type v} → {σ : Type u_1} → [inst : CommRing S] → (MvPolynomial σ ℤ →+* S) ≃ (σ → S)
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_inv_symm_left_iff : ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.SubarrayIterator.length_eq : ∀ {α : Type u} {it : Std.Iter α}, it.length = it.internalState.xs.stop - it.internalState.xs.start
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F]
  [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G] [inst_11 : TopologicalSpace G]
  [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G),
  g.continuousAlternatingMapCongrRight.symm = g.symm.continuousAlternatingMapCongrRight
-- Init.Data.Array.Lemmas
Array.empty_beq_eq : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α}, (#[] == xs) = xs.isEmpty
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_filter_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (p : α → Prop) [inst_2 : Fintype α]
  [inst_3 : DecidablePred p], ↑{x | p x}⁻¹ = {x | p x⁻¹}
-- Init.Data.UInt.Bitwise
USize.toNat_xor : ∀ (a b : USize), (a ^^^ b).toNat = a.toNat ^^^ b.toNat
-- Mathlib.Algebra.Group.Basic
zpow_eq_zpow_emod' : ∀ {G : Type u_3} [inst : Group G] {x : G} (m : ℤ) {n : ℕ}, x ^ n = 1 → x ^ m = x ^ (m % ↑n)
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_symm_toIntLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {modM : Module ℤ M}
  {modM₂ : Module ℤ M₂} (e : M ≃+ M₂), ⇑e.toIntLinearEquiv.symm = ⇑e.symm
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle K L n) {L' : CochainComplex C ℤ}
  (g : L ⟶ L'),
  CochainComplex.HomComplex.Cocycle.equivHomShift.symm (z.postcomp g) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.HomComplex.Cocycle.equivHomShift.symm z)
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map g)
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_ofLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Lex α}, IsAddRightRegular (ofLex a) ↔ IsAddRightRegular a
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.right_mem_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, b ∈ Set.uIcc a b
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.continuous : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Continuous ⇑f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.id : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → ℕ
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- The range of the adjoint action homomorphism from a Lie algebra `L` to the Lie algebra of its
derivations is an ideal of the latter.  -/
LieDerivation.ad_isIdealMorphism : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (LieDerivation.ad R L).IsIdealMorphism
-- Mathlib.Tactic.NormNum.IsCoprime
/-- Evaluates `IsCoprime` for the given integer number literals.
Panics if `ex` or `ey` aren't integer number literals.  -/
Mathlib.Meta.NormNum.proveIntIsCoprime : (ex ey : Q(ℤ)) → Q(IsCoprime «$ex» «$ey») ⊕ Q(¬IsCoprime «$ex» «$ey»)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.symm_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F),
  (LinearIsometryEquiv.rTensor G f).symm = LinearIsometryEquiv.rTensor G f.symm
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Star projection operators are equal iff their range are.  -/
ContinuousLinearMap.IsStarProjection.ext_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E] {S : E →L[𝕜] E},
  IsStarProjection S → IsStarProjection T → (S = T ↔ (↑S).range = (↑T).range)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.prod_fst : ∀ (ι : Type w) (self : ι × ι), (CategoryTheory.Limits.MultispanShape.prod ι).fst self = self.1
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.isCardinalAccessible_of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {κ : Cardinal.{w}} [inst_2 : Fact κ.IsRegular] [F.IsCardinalAccessible κ]
  {κ' : Cardinal.{w}} [inst_4 : Fact κ'.IsRegular], κ ≤ κ' → F.IsCardinalAccessible κ'
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.mergeIdem.loop.match_1.splitter : (motive : ℕ → List ℕ → Sort u_1) →
  (x : ℕ) →
    (x_1 : List ℕ) →
      ((curr next : ℕ) → (rest : List ℕ) → motive curr (next :: rest)) → ((curr : ℕ) → motive curr []) → motive x x_1