mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Discriminant
Algebra.discr_reindex : ∀ (A : Type u) {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] {ι' : Type u_1} [inst_4 : Fintype ι'] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι']
  (b : Module.Basis ι A B) (f : ι ≃ ι'), Algebra.discr A (⇑b ∘ ⇑f.symm) = Algebra.discr A ⇑b
-- Init.Data.SInt.Bitwise
Int32.toInt64_and : ∀ (a b : Int32), (a &&& b).toInt64 = a.toInt64 &&& b.toInt64
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.add_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β] (f g : MeasureTheory.SimpleFunc α β)
  (a : α), (f + g) a = f a + g a
-- Mathlib.Algebra.Star.Unitary
/-- For unitary `U` in a star-monoid `R`, `x * U = y * U` if and only if `x = y`
for all `x` and `y` in `R`.  -/
Unitary.mul_left_inj : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x y : R} (U : ↥(unitary R)), x * ↑U = y * ↑U ↔ x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.containsKey (Std.Internal.List.maxKey! l) l = true
-- Init.Data.AC
Lean.Data.AC.Context.vars : {α : Sort u} → (self : Lean.Data.AC.Context α) → List (Lean.Data.AC.Variable self.op)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.postReduce : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Computability.Partrec
Computable.sumInr : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Sum.inr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul.inj : ∀ {a? : Option Lean.Expr} {cs : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} {a?_1 : Option Lean.Expr}
  {cs_1 : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a? cs = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a?_1 cs_1 →
    a? = a?_1 ∧ cs = cs_1
-- Mathlib.GroupTheory.Exponent
/-- A predicate on an additive monoid saying that there is a positive integer `n` such that
`n • g = 0` for all `g`.  -/
AddMonoid.ExponentExists : (G : Type u) → [AddMonoid G] → Prop
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.exists_upcrossings_of_not_bounded_under : ∀ {ι : Type u_4} {l : Filter ι} {x : ι → ℝ},
  Filter.liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤ →
    (¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun i => |x i|) →
      ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
-- Mathlib.Logic.Equiv.Defs
Equiv.toFun_as_coe : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ⇑e
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- The parameterized integral `x ↦ ∫ y, g (y⁻¹ * x) ∂μ` depends continuously on `y` when `g` is a
compactly supported continuous function on a topological group `G`, and `μ` is finite on compact
sets.  -/
MeasureTheory.continuous_integral_apply_inv_mul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [LocallyCompactSpace G] [inst_2 : Group G] [IsTopologicalGroup G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : NormedSpace ℝ E] {g : G → E},
  Continuous g → HasCompactSupport g → Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ
-- Mathlib.Data.List.Destutter
List.destutter'.eq_1 : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (x : α), List.destutter' R x [] = [x]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k fallback : α}, m₂.contains k = true → (m₁.diff m₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and right homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced morphism `h₁.K ⟶ h₁.K` on opcycles.  -/
CategoryTheory.ShortComplex.opcyclesMap' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → (h₁ : S₁.RightHomologyData) → (h₂ : S₂.RightHomologyData) → h₁.Q ⟶ h₂.Q
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Reverts assignments to the array it was prior to adding derivedLits.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments : {n : ℕ} →
  Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
    List (Std.Tactic.BVDecide.LRAT.Internal.PosFin n × Bool) → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_inv_one_add_sq : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  IntervalIntegrable (fun x => (1 + x ^ 2)⁻¹) μ a b
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instSubsingletonOfIsEmpty : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [IsEmpty α], Subsingleton (BooleanSubalgebra α)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toSubgroup : Subgroup G)
  (isOpen' : IsOpen toSubgroup.carrier),
  sizeOf { toSubgroup := toSubgroup, isOpen' := isOpen' } = 1 + sizeOf toSubgroup + sizeOf isOpen'
-- Mathlib.Topology.Category.TopPair
/-- The functor from topological pairs to topological spaces that forgets the second space, i.e. the
projection to the first space.  -/
TopPair.proj₁ : CategoryTheory.Functor TopPair TopCat
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A topological space is completely metrizable if there exists a metric space structure
compatible with the topology which makes the space complete.
To endow such a space with a compatible distance, use
`letI := upgradeIsCompletelyMetrizable X`.  -/
TopologicalSpace.IsCompletelyMetrizableSpace : (X : Type u_3) → [t : TopologicalSpace X] → Prop
-- Mathlib.Data.Option.Basic
Option.coe_def : ∀ {α : Type u_1}, (fun a => some a) = some
-- Init.System.IO
/-- The directory in which the entry is found.  -/
IO.FS.DirEntry.root : IO.FS.DirEntry → System.FilePath
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_to_real : ∀ {x : ℝ}, RCLike.re x = x
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.exists_eq_of_of_eq : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] {i : ι} {x y : G i},
  (Module.DirectLimit.of R ι G f i) x = (Module.DirectLimit.of R ι G f i) y →
    ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limit_mul_val : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u})
  (x y : ↑(ProfiniteGrp.limit F).toProfinite.toTop) (j : J), ↑(x * y) j = ↑x j * ↑y j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∉ t → t.getKey! a = default
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraint : String → Lean.Omega.Constraint → String
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `baseChange A e` for `e : M ≃ₗ[R] N` is the `A`-linear map `A ⊗[R] M ≃ₗ[A] A ⊗[R] N`.  -/
LinearEquiv.baseChange : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_4) →
      (N : Type u_5) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (M ≃ₗ[R] N) → TensorProduct R A M ≃ₗ[A] TensorProduct R A N
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.ext : ∀ {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ},
  (∀ (a : σ), IsOpen (F.f a)) → (∀ (a : α), ∀ s ∈ nhds a, ∃ b, a ∈ F.f b ∧ F.f b ⊆ s) → F.toTopsp = T
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.BackwardSliceSearcher.skipSuffix?_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → String.Slice.Pattern.BackwardPattern.skipSuffix? pat s = some s.endPos
-- Mathlib.GroupTheory.Coset.Defs
/-- If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection.  -/
AddSubgroup.quotientEquivOfEq : {α : Type u_1} → [inst : AddGroup α] → {s t : AddSubgroup α} → s = t → α ⧸ s ≃ α ⧸ t
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulRight_toEquiv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  (IsometryEquiv.mulRight c).toEquiv = Equiv.mulRight c
-- Mathlib.Data.List.Rotate
List.IsRotated.perm : ∀ {α : Type u} {l l' : List α}, l ~r l' → l.Perm l'
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : NatCast F] (n : ℕ), HasStrictDerivAt (↑n) 0 x
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.LCtxId.isValid : Lean.Elab.WF.LCtxId✝ → Lean.MetaM Bool
-- Mathlib.Dynamics.Minimal
IsOpen.exists_smul_mem : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] (x : α) {U : Set α}, IsOpen U → U.Nonempty → ∃ c, c • x ∈ U
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.nextn : ∀ {l m₁ m₂ r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l (m₁ ++ m₂) r s →
    ∀ (n : ℕ),
      s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }
-- Init.Data.List.Erase
List.IsPrefix.eraseP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <+: l₂ → List.eraseP p l₁ <+: List.eraseP p l₂
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.tr_comp'_assoc : ∀ {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) {hb : b.len ≤ n} {hc : c.len ≤ n}
  (g : { obj := b, property := hb } ⟶ { obj := c, property := hc })
  (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp'._auto_1)
  {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ n} (h : { obj := c, property := hc } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.Hom.tr (CategoryTheory.CategoryStruct.comp f g.hom) ha hc) h =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr f ha hb)
      (CategoryTheory.CategoryStruct.comp g h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k}, a ∈ (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl ↔ compare k a = Ordering.eq ∨ a ∈ t
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.restrict_toContinuousLinearMap : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {H : Type u_6} [inst_10 : Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G)
  (f : ContIntertwiningMap π π'), (ContIntertwiningMap.restrict φ f).toContinuousLinearMap = f.toContinuousLinearMap
-- Mathlib.Algebra.Homology.Homotopy
/-- A homotopy showing that composing the forward and backward maps is homotopic to the identity
on C  -/
HomotopyEquiv.homotopyHomInvId : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (self : HomotopyEquiv C D) →
              Homotopy (CategoryTheory.CategoryStruct.comp self.hom self.inv) (CategoryTheory.CategoryStruct.id C)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {k k' : α}, (k == k') = true → m.get! k = m.get! k'
-- Init.GrindInstances.ToInt
Lean.Grind.instMulUSizeUintNumBits : Lean.Grind.ToInt.Mul USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprSourceInfo_mathlib : Lean.ToExpr Lean.SourceInfo
-- Mathlib.Data.ZMod.Basic
/-- **Alias** of the reverse direction of `ZMod.intCast_eq_zero_iff_even`. -/
Even.intCast_zmod_two : ∀ {n : ℤ}, Even n → ↑n = 0
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero.  -/
IsLocalMin.fderiv_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
  IsLocalMin f a → fderiv ℝ f a = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_coe : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑↑e = ⇑e
-- Init.Data.Char.Lemmas
Char.not_lt : ∀ {a b : Char}, ¬a < b ↔ b ≤ a
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_sub_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f₁ f₂ g : (i : ι) → E i), ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w]
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Std.Iterators.Vector.isPlausibleStep_iterM_of_pos : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n} (h : 0 < n),
  (xs.iterM m).IsPlausibleStep (Std.IterStep.yield (xs.iterFromIdxM m 1) xs[0])
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.id_map : ∀ {n : ℕ} (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} (x : ↑P α), MvFunctor.map TypeVec.id x = x
-- Mathlib.Data.Ordmap.Ordset
/-- O(1). Get the size of the set.  -/
Ordset.size : {α : Type u_1} → [inst : Preorder α] → Ordset α → ℕ
-- Mathlib.Algebra.Field.Defs
Semifield.toZPow : {K : Type u_2} → [self : Semifield K] → ZPow K
-- Mathlib.Algebra.Group.Pi.Basic
Pi.involutiveNeg : {I : Type u} → {f : I → Type v₁} → [(i : I) → InvolutiveNeg (f i)] → InvolutiveNeg ((i : I) → f i)
-- Mathlib.Order.CompactlyGenerated.Intervals
complementedLattice_of_complementedLattice_Iic : ∀ {ι : Type u_1} {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {s : Set ι}
  {f : ι → α}, (∀ i ∈ s, ComplementedLattice ↑(Set.Iic (f i))) → ⨆ i ∈ s, f i = ⊤ → ComplementedLattice α
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.ComonObj A]
  (X : C), (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj A X).X = A.obj X
-- Init.Data.Vector.Lemmas
Vector.foldl_push : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : β → α → β} {init : β} {xs : Vector α n} {a : α},
  Vector.foldl f init (xs.push a) = f (Vector.foldl f init xs) a
-- Mathlib.Order.WithBot
WithBot.coe_max : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ↑(max a b) = max ↑a ↑b
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.map_comp_c_app : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃)
  (U : (TopologicalSpace.Opens ↑↑(F.obj j₃))ᵒᵖ),
  (F.map (CategoryTheory.CategoryStruct.comp f g)).c.app U =
    CategoryTheory.CategoryStruct.comp ((F.map g).c.app U)
      (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C (F.map g).base).map (F.map f).c).app U)
        ((TopCat.Presheaf.pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U))
-- Init.Meta.Defs
/-- Syntax that represents macro hygiene info.
 -/
Lean.Syntax.HygieneInfo : Type
-- Std.Time.Format.Modifier
/-- Unknown zone placeholder (1 letter, `V`): always formats as "unk".
 -/
Std.Time.ZoneId.unknown : Std.Time.ZoneId
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Dvd α] [inst_1 : Monoid β] [inst_2 : Monoid γ] {f : α → γ}
  [inst_3 : SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (b : β),
  IsDvdSequence f → IsDvdSequence (b • f)
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_eraseIdx_of_ge : ∀ {α : Type u} {a : α} {n i j : ℕ} {xs : Vector α n} (w₁ : i < n) (w₂ : j ≤ n - 1),
  i ≤ j → (xs.eraseIdx i w₁).insertIdx j a w₂ = Vector.cast ⋯ ((xs.insertIdx (j + 1) a ⋯).eraseIdx i ⋯)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_le_omega : ∀ {o₁ o₂ : Ordinal.{u_1}}, Ordinal.omega o₁ ≤ Ordinal.omega o₂ ↔ o₁ ≤ o₂
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X}, CategoryTheory.Sieve.pullback f ⊤ = ⊤
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instOrderTop.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass.instOrderTop = { top := MulArchimedeanClass.mk 1, le_top := ⋯ }
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- If `K` is a field, then so is `K` viewed as a valuation subring
of itself. (That is, `⊤ : ValuationSubring K`.)  -/
ValuationSubring.instFieldSubtypeMemTop : {K : Type u} → [inst : Field K] → Field ↥⊤
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.le_stabilizer_smul_right : ∀ {α : Type u_2} {β : Type u_3} {G' : Type u_4} [inst : Group G'] [inst_1 : SMul α β] [inst_2 : MulAction G' β]
  [SMulCommClass G' α β] (a : α) (b : β), MulAction.stabilizer G' b ≤ MulAction.stabilizer G' (a • b)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.isExtTangent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsExtTangentAt s₂ p → s₁.IsExtTangent s₂
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_apply : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.X = MvPowerSeries.X ()
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_le_one : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), A.valuation ↑a ≤ 1
-- Mathlib.Data.EReal.Operations
EReal.coe_mul_bot_of_neg : ∀ {x : ℝ}, x < 0 → ↑x * ⊥ = ⊤
-- Init.Grind.ToInt
/-- An interval in the integers (either finite, half-infinite, or infinite).  -/
Lean.Grind.IntInterval : Type
-- Mathlib.Data.Finset.Insert
/-- The equivalence between pi types on cons and the product.  -/
Finset.consPiProdEquiv : {α : Type u_1} →
  [DecidableEq α] →
    {s : Finset α} →
      (f : α → Type u_3) →
        {a : α} → (has : a ∉ s) → ((i : α) → i ∈ Finset.cons a s has → f i) ≃ f a × ((i : α) → i ∈ s → f i)
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_sub : ∀ (a b : BitVec 16), { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsUniversallyEffectiveEquivalenceRelation.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A},
  Nonempty (CategoryTheory.UniversallyEffectiveEquivalenceRelation p₁ p₂) →
    CategoryTheory.IsUniversallyEffectiveEquivalenceRelation p₁ p₂
-- Mathlib.Order.SuccPred.Basic
/-- Proof of basic ordering with respect to `succ`  -/
SuccOrder.le_succ : ∀ {α : Type u_3} {inst : Preorder α} [self : SuccOrder α] (a : α), a ≤ SuccOrder.succ a
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.exists_isRegular_of_finrank_le_card : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [IsDomain R],
  ↑(Module.finrank R L) ≤ Cardinal.mk R → ∃ x, LieAlgebra.IsRegular R x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inr_mem_Icc_iff_norm_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A},
  ↑x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1
-- Mathlib.Topology.Order
/-- Every function to the indiscrete topology is continuous  -/
continuous_of_indiscreteTopology : ∀ {α : Type u_1} {t₂ : TopologicalSpace α} {β : Type u_2} [inst : TopologicalSpace β] [IndiscreteTopology β]
  {f : α → β}, Continuous f
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.support_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) [inst_1 : DecidableEq σ],
  p ≠ 0 → ((MvPolynomial.expand p) φ).support = Finset.image (fun x => p • x) φ.support
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- Composition of `StrictPseudofunctor`.  -/
CategoryTheory.StrictPseudofunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.StrictPseudofunctor B C →
              CategoryTheory.StrictPseudofunctor C D → CategoryTheory.StrictPseudofunctor B D
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.singleRuleTac.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.RuleTacDescr.singleRuleTac decl) = 1 + sizeOf decl
-- Mathlib.Topology.MetricSpace.Closeds
/-- By definition, the edistance on `Closeds α` is given by the Hausdorff edistance  -/
TopologicalSpace.Closeds.edist_eq : ∀ {α : Type u_1} [inst : EMetricSpace α] {s t : TopologicalSpace.Closeds α}, edist s t = Metric.hausdorffEDist ↑s ↑t
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.equivPiOfIsSepClosed_comap : ∀ {K : Type u_1} {A : Type u} [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] {B : Type u_3}
  [inst_3 : CommRing B] [inst_4 : Algebra.EssFiniteType K A] [inst_5 : Algebra.FormallyEtale K A] [inst_6 : Algebra K B]
  [inst_7 : Algebra.EssFiniteType K B] [inst_8 : Algebra.FormallyEtale K B] [inst_9 : IsSepClosed K] (f : A →ₐ[K] B)
  (x : A) (p : PrimeSpectrum B),
  (Algebra.FormallyEtale.equivPiOfIsSepClosed K A) x (PrimeSpectrum.comap (↑f) p) =
    (Algebra.FormallyEtale.equivPiOfIsSepClosed K B) (f x) p
-- Mathlib.Order.Filter.Pointwise
Filter.isUnit_pure : ∀ {α : Type u_2} [inst : Group α] (a : α), IsUnit (pure a)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.instFaithfulSMul_2 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ}, FaithfulSMul H (Monoid.PushoutI.NormalWord d)
-- Mathlib.Analysis.Complex.Poisson
herglotzRieszKernel_add_const : ∀ (c w z : ℂ), herglotzRieszKernel c w (z + c) = herglotzRieszKernel 0 (w - c) z