mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inst : (B : Type u₁) → [CategoryTheory.Bicategory B] → CategoryTheory.Bicategory (CategoryTheory.Bicategory.Pith B)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f),
  (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).fiber =
    CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any
object.  -/
CategoryTheory.Comonad.cofree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (G : CategoryTheory.Comonad C) → CategoryTheory.Functor C G.Coalgebra
-- Lean.Elab.PreDefinition.PartialFixpoint.Main
_private.Lean.Elab.PreDefinition.PartialFixpoint.Main.0.Lean.Elab.replaceRecApps : Array Lean.Name → Lean.Elab.FixedParamPerms → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.String.FindPos
/-- Obtains the smallest valid position that is strictly greater than the given byte position.
 -/
String.posGT : (s : String) → (offset : String.Pos.Raw) → offset < s.rawEndPos → s.Pos
-- Mathlib.Algebra.Exact.Basic
Function.Exact.of_ladder_addEquiv_of_exact : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : AddCommMonoid X₁] [inst_1 : AddCommMonoid X₂] [inst_2 : AddCommMonoid X₃] [inst_3 : AddCommMonoid Y₁]
  [inst_4 : AddCommMonoid Y₂] [inst_5 : AddCommMonoid Y₃] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃)
  {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ → g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → Function.Exact ⇑f₁₂ ⇑f₂₃ → Function.Exact ⇑g₁₂ ⇑g₂₃
-- Mathlib.Algebra.Group.AddChar
/-- Define the multiplicative shift of an additive character.
This satisfies `mulShift ψ a x = ψ (a * x)`.  -/
AddChar.mulShift : {R : Type u_1} → {M : Type u_2} → [inst : Ring R] → [inst_1 : CommMonoid M] → AddChar R M → R → AddChar R M
-- Aesop.Index.Basic
Aesop.IndexingMode.hyps : Array Lean.Meta.DiscrTree.Key → Aesop.IndexingMode
-- Lean.Level
Lean.Level.format : Lean.Level → Bool → (Lean.LMVarId → Option ℕ) → Std.Format
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_sum : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] {ι : Type u_5} (s : Finset ι) (f : ι → CompactlySupportedContinuousMap α β),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Order.Lattice
OrderDual.instSemilatticeInf.eq_1 : ∀ (α : Type u_1) [h : SemilatticeSup α],
  OrderDual.instSemilatticeInf α =
    { toPartialOrder := OrderDual.instPartialOrder α, inf := fun a b => SemilatticeSup.sup a b, inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_of_cfcHom_map_quasispectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (f : ContinuousMapZero (↑(quasispectrum R a)) R), quasispectrum R ((cfcₙHom_of_cfcHom R ha) f) = Set.range ⇑f
-- Mathlib.Algebra.Ring.Subring.Units
RingHom.instIsLocalHomSubtypeMemSubsemiringEqLocusSSubtype : ∀ {R : Type u_1} {T : Type u_2} [inst : Semiring T] [inst_1 : Semiring R] (f g : R →+* T),
  IsLocalHom (f.eqLocusS g).subtype
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- Every cofinal set has a cofinal subset of order type `(cof α).ord`.  -/
Ordinal.exists_ord_cof_eq_of_isCofinal : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] {s : Set α},
  IsCofinal s → ∃ t ⊆ s, IsCofinal t ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.ofList_append : ∀ {R : Type u_1} [inst : Semiring R] (rs₁ rs₂ : List R), Ideal.ofList (rs₁ ++ rs₂) = Ideal.ofList rs₁ ⊔ Ideal.ofList rs₂
-- Mathlib.Data.Set.Card
Set.ncard_union_eq : ∀ {α : Type u_1} {s t : Set α},
  Disjoint s t →
    autoParam s.Finite Set.ncard_union_eq._auto_1 →
      autoParam t.Finite Set.ncard_union_eq._auto_3 → (s ∪ t).ncard = s.ncard + t.ncard
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalCase : Lean.Elab.Tactic.Tactic
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.mul_adjp_apply_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R) (i : n), (A * Matrix.adjp s A) i i = Matrix.detp s A
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- Construct a bundled ωCPO from the underlying type and typeclass.  -/
ωCPO.of : (carrier : Type u) → [str : OmegaCompletePartialOrder carrier] → ωCPO
-- LeanSearchClient.Syntax
/-- Search [LeanSearch](https://leansearch.net/) from within Lean.
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry
```

You can modify the LeanSearch URL by setting the `LEANSEARCHCLIENT_LEANSEARCH_API_URL` environment variable.
  -/
LeanSearchClient.leansearch_search_term : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1)))
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β),
  x = Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
        h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) ≍
      h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_mul_equiv_snd : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (g : G),
  ↑(hST.equiv g).1 * ↑(hST.equiv g).2 = g
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  {as as_1 : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ}, { as := as } = { as := as_1 } → as = as_1
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.forward_eq_nextn : String.Legacy.Iterator.forward = String.Legacy.Iterator.nextn
-- Mathlib.Data.List.Destutter
List.isChain_destutter : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), List.IsChain R (List.destutter R l)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- If two finite measures have the same characteristic function, then they are equal.  -/
MeasureTheory.Measure.ext_of_charFunDual : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E]
  [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.charFunDual μ = MeasureTheory.charFunDual ν → μ = ν
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousAt.cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℂ} {a : α},
  ContinuousAt f a → ContinuousAt g a → f a ∈ Complex.slitPlane → ContinuousAt (fun x => f x ^ g x) a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow : ∀ {k : ℕ},
  1 ≤ k →
    ∀ {z : ℂ},
      z ∈ UpperHalfPlane.upperHalfPlaneSet →
        iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z =
          (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
-- Mathlib.FieldTheory.Finite.Basic
Subfield.splits_bot : ∀ (F : Type u_3) [inst : Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p], (Polynomial.X ^ p - Polynomial.X).Splits
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCone.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)}
  {liftedCone : CategoryTheory.Limits.Cone K} {validLift : F.mapCone liftedCone ≅ c}
  {liftedCone_1 : CategoryTheory.Limits.Cone K} {validLift_1 : F.mapCone liftedCone_1 ≅ c},
  { liftedCone := liftedCone, validLift := validLift } = { liftedCone := liftedCone_1, validLift := validLift_1 } →
    liftedCone = liftedCone_1 ∧ validLift ≍ validLift_1
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivAt.mul` -/
HasFDerivAt.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasFDerivAt c c' x → HasFDerivAt d d' x → HasFDerivAt (fun i => c i * d i) (c x • d' + d x • c') x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (t.alter k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then some k else none else t.getKey? k'
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a unit from limits of units and their inverses.  -/
Filter.Tendsto.units : {ι : Type u_1} →
  {N : Type u_4} →
    [inst : TopologicalSpace N] →
      [inst_1 : Monoid N] →
        [ContinuousMul N] →
          [T2Space N] →
            {f : ι → Nˣ} →
              {r₁ r₂ : N} →
                {l : Filter ι} →
                  [l.NeBot] →
                    Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁) → Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂) → Nˣ
-- Mathlib.Data.List.Rotate
List.rotate_eq_rotate' : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate n = l.rotate' n
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.map_map : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : AddCommMonoid G] [inst_8 : Module R G] (g : F →ₗ[R] G) (f : E →ₗ[R] F)
  (C : PointedCone R E), PointedCone.map g (PointedCone.map f C) = PointedCone.map (g ∘ₗ f) C
-- Lean.Declaration
Lean.AxiomVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {isUnsafe : Bool} {toConstantVal_1 : Lean.ConstantVal} {isUnsafe_1 : Bool},
  { toConstantVal := toConstantVal, isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, isUnsafe := isUnsafe_1 } →
    toConstantVal = toConstantVal_1 ∧ isUnsafe = isUnsafe_1
-- Mathlib.Algebra.Module.FinitePresentation
FinitePresentation.of_isBaseChange : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {A : Type u_1} [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (f : M →ₗ[R] N),
  IsBaseChange A f → ∀ [Module.FinitePresentation R M], Module.FinitePresentation A N
-- Mathlib.Tactic.TacticAnalysis
/-- The internal representation of a tactic analysis pass,
extending `Config` with some declaration meta-information.
 -/
Mathlib.TacticAnalysis.Pass : Type
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `simp_all` at every step in proofs, reporting where it succeeds.  -/
linter.tacticAnalysis.tryAtEachStepSimpAll : Lean.Option Bool
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- `HasPointwiseLeftKanExtensionAt` is invariant when we replace `L` and `F` by isomorphic
functors.  -/
CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} {Y : D} (e₁ : L ≅ L') (e₂ : F ≅ F'),
  L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F' Y
-- Batteries.Lean.LawfulMonad
instLawfulMonadCoreM_batteries : LawfulMonad Lean.CoreM
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.add_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → ∀ (c : F), DiffContOnCl 𝕜 (fun x => f x + c) s
-- Init.Data.SInt.Lemmas
Int16.ofNat_mul : ∀ (a b : ℕ), Int16.ofNat (a * b) = Int16.ofNat a * Int16.ofNat b
-- Mathlib.Order.SuccPred.Tree
SubRootedTree.root_ne_bot_of_mem_subtrees : ∀ {t : RootedTree}, ∀ r ∈ t.subtrees, r.root ≠ ⊥
-- Mathlib.Data.Pi.Interval
Pi.instLocallyFiniteOrderTop : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [Fintype ι] →
      [DecidableEq ι] →
        [(i : ι) → DecidableEq (α i)] →
          [inst : (i : ι) → PartialOrder (α i)] →
            [(i : ι) → LocallyFiniteOrderTop (α i)] → LocallyFiniteOrderTop ((i : ι) → α i)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The canonical image of the `FreeAlgebra` in the `TensorAlgebra`, which maps
`FreeAlgebra.ι R x` to `TensorAlgebra.ι R x`.  -/
FreeAlgebra.toTensor : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → FreeAlgebra R M →ₐ[R] TensorAlgebra R M
-- Lean.Meta.Tactic.Grind.Types
/-- New equalities and facts to be processed.  -/
Lean.Meta.Grind.NewFact : Type
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_6 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S q.succ = Turing.PartrecToTM2.Λ'.Supports S q
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mk.injEq : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (toSubmodule : Submodule R M) (isClosed' : IsClosed toSubmodule.carrier)
  (toSubmodule_1 : Submodule R M) (isClosed'_1 : IsClosed toSubmodule_1.carrier),
  ({ toSubmodule := toSubmodule, isClosed' := isClosed' } =
      { toSubmodule := toSubmodule_1, isClosed' := isClosed'_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (x : ↑↑D.glued),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = x
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_trans : ∀ {X : AlgebraicGeometry.Scheme} {x y z : ↥X} (e : x = y) (e' : y = z),
  AlgebraicGeometry.Scheme.residueFieldCongr e ≪≫ AlgebraicGeometry.Scheme.residueFieldCongr e' =
    AlgebraicGeometry.Scheme.residueFieldCongr ⋯
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.post_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.post L R F).obj X).left = X.left
-- Mathlib.Data.Stream.Defs
/-- Enumerate a stream by tagging each element with its index.  -/
Stream'.enum : {α : Type u} → Stream' α → Stream' (ℕ × α)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andLeft.inj : ∀ {ak : Mathlib.Tactic.ITauto.AndKind} {p : Mathlib.Tactic.ITauto.Proof} {ak_1 : Mathlib.Tactic.ITauto.AndKind}
  {p_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.andLeft ak p = Mathlib.Tactic.ITauto.Proof.andLeft ak_1 p_1 → ak = ak_1 ∧ p = p_1
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_eq_const_of_mem : ∀ {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 : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] {p : P}, p ∈ s → ↑(s.signedInfDist p) = AffineMap.const ℝ P 0
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_zero_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], Set.Iio 0 = ∅
-- Mathlib.Topology.Germ
Filter.Germ.valueAddHom.eq_1 : ∀ {X : Type u_4} {E : Type u_5} [inst : AddMonoid E] [inst_1 : TopologicalSpace X] {x : X},
  Filter.Germ.valueAddHom = { toFun := Filter.Germ.value, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  ↑((AlgebraicGeometry.IsOpenImmersion.opensEquiv f) U) = (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_iUnion_of_finite : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {ι : Type u_4} [Finite ι]
  (f : ι → Set P), asymptoticCone k (⋃ i, f i) = ⋃ i, asymptoticCone k (f i)
-- Batteries.Data.Fin.Lemmas
Fin.findSome?.eq_1 : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → Option α), Fin.findSome? f = Fin.foldl n (fun r i => r <|> f i) none
-- Lean.Parser.Do
Lean.Parser.Term.doDebugAssert.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.RepresentablyCoflat F] {G : CategoryTheory.Functor C D} (α : F ≅ G),
  CategoryTheory.RepresentablyCoflat G
-- Mathlib.Data.ENat.Basic
ENat.lift_one : ENat.lift 1 ⋯ = 1
-- Mathlib.RingTheory.Ideal.Defs
/-- A left ideal `I : Ideal R` is two-sided if it is also a right ideal.  -/
Ideal.IsTwoSided : {α : Type u} → [inst : Semiring α] → Ideal α → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.differentiableOn : ∀ {𝕜 : 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] {f : E → F}
  {s : Set E}, IsBoundedLinearMap 𝕜 f → DifferentiableOn 𝕜 f s
-- Mathlib.Data.Semiquot
Semiquot.pure_le : ∀ {α : Type u_1} {a : α} {s : Semiquot α}, pure a ≤ s ↔ a ∈ s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The associator isomorphism for Day convolution  -/
CategoryTheory.MonoidalCategory.DayConvolution.associator : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F G : CategoryTheory.Functor C V) →
              [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                (H : CategoryTheory.Functor C V) →
                  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H] →
                    [inst_6 :
                        CategoryTheory.MonoidalCategory.DayConvolution F
                          (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] →
                      [inst_7 :
                          CategoryTheory.MonoidalCategory.DayConvolution
                            (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] →
                        [∀ (v : V) (d : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape
                                (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                                (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                          [∀ (v : V) (d : C),
                                CategoryTheory.Limits.PreservesColimitsOfShape
                                  (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                                  (CategoryTheory.MonoidalCategory.tensorRight v)] →
                            CategoryTheory.MonoidalCategory.DayConvolution.convolution
                                (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H ≅
                              CategoryTheory.MonoidalCategory.DayConvolution.convolution F
                                (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)
-- Init.Data.SInt.Lemmas
Int64.toUInt64_le : ∀ {a b : Int64}, 0 ≤ a → a ≤ b → a.toUInt64 ≤ b.toUInt64
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is closed by finite intersections.  -/
MeasureTheory.IsSetAlgebra.biInter_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {ι : Type u_2},
  MeasureTheory.IsSetAlgebra 𝒜 → ∀ {s : ι → Set α} (S : Finset ι), (∀ i ∈ S, s i ∈ 𝒜) → ⋂ i ∈ S, s i ∈ 𝒜
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.one_apply : ∀ (G H : GrpCat) (g : ↑G), (CategoryTheory.ConcreteCategory.hom 1) g = 1