mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} {f : A₀.a ⟶ A₁.a}
  {h :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam}
  {f_1 : A₀.a ⟶ A₁.a}
  {h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f_1) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f_1)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam},
  { f := f, h := h } = { f := f_1, h := h_1 } → f = f_1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.inv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Inv β]
  [inst_3 : ContinuousInv β] (f : C(α, β)) (x : α), f⁻¹ x = (f x)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- Given `F : WalkingSpan ⥤ C`, which is really the same as `span (F.map fst) (F.map snd)`,
and a cocone on `F`, we get a pushout cocone on `F.map fst` and `F.map snd`.  -/
CategoryTheory.Limits.PushoutCocone.ofCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      CategoryTheory.Limits.Cocone F →
        CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
          (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.mk.injEq : ∀ (merged : Lean.Linter.LinterSets) (localEntries : Array (Lean.Name × Lean.NameSet))
  (merged_1 : Lean.Linter.LinterSets) (localEntries_1 : Array (Lean.Name × Lean.NameSet)),
  ({ merged := merged, localEntries := localEntries } = { merged := merged_1, localEntries := localEntries_1 }) =
    (merged = merged_1 ∧ localEntries = localEntries_1)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.coe_range_dense : ∀ {K : Type u_2} [inst : Field K], DenseRange ⇑(algebraMap (RatFunc K) (LaurentSeries K))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W.addY P Q = WeierstrassCurve.Projective.addU P Q
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn.eq_1 : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] (u : ι → Ω → β) (s : Set β)
  (n m : ι) (x : Ω),
  MeasureTheory.hittingBtwn u s n m x = if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i | u i x ∈ s}) else m
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.Faithful.mapMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [F.Faithful], F.mapMon.Faithful
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_subset_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s t : Finset α}, s ⊆ t → s⁻¹ ⊆ t⁻¹
-- Mathlib.Data.Nat.ModEq
Nat.odd_mul_odd_div_two : ∀ {m n : ℕ}, m % 2 = 1 → n % 2 = 1 → m * n / 2 = m * (n / 2) + m / 2
-- Mathlib.Order.Hom.Lex
/-- A linear order is isomorphic to the lexicographic sum of elements less or equal to `x` and
elements greater than `x`.  -/
OrderIso.sumLexIicIoi : {α : Type u_1} → [inst : LinearOrder α] → (x : α) → ↑(Set.Iic x) ⊕ₗ ↑(Set.Ioi x) ≃o α
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertListₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → List ((a : α) × β a) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- The flat-array algorithm `BirdDet.birdDet` computes the same determinant as
`BirdDet.Spec.birdDet`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.birdDet_eq_birdDetSpec : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Array R) (hA : A.size = n * n),
  BirdDet.birdDet n A = BirdDet.Spec.birdDet (Matrix.ofArray A hA)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_fun_smul : ∀ {𝕜 : 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}
  {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 f x → fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x)
-- Mathlib.Computability.Encoding
/-- A binary `Encoding` of `ℕ` in `Bool`.  -/
Computability.encodingNatBool : Computability.Encoding ℕ Bool
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.modifyGet_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {f : σ → α × σ}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  ⦃fun s =>
    have t := f s;
    Q.1 t.1 t.2⦄
    MonadStateOf.modifyGet f ⦃Q⦄
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.instIsLeftAdjointMapOfHasPullbacksAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasPullbacksAlong f], (CategoryTheory.Over.map f).IsLeftAdjoint
-- Lean.DocString.Extension
Lean.VersoModuleDocs.snippets : Lean.VersoModuleDocs → Lean.PersistentArray Lean.VersoModuleDocs.Snippet
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac._auto_1)
  [inst_2 : (S.sc hS k ⋯).HasRightHomology] [inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (S.sc hS k ⋯).pOpcycles
      (CategoryTheory.CategoryStruct.comp (hS.opcyclesToCycles k ⋯) (S.sc hS (k + 1) ⋯).iCycles) =
    S.map' (k + 1) (k + 2) ⋯ ⋯
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_22 : HSub Std.Time.Minute.Offset Std.Time.Day.Offset Std.Time.Minute.Offset
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
instMulPosMonoWithZeroOfMulRightMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α], MulPosMono (WithZero α)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_two : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  autoParam (0 ≤ a) CFC.nnrpow_two._auto_1 → a ^ 2 = a * a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.eta_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T),
  f.eta.hom.right = CategoryTheory.CategoryStruct.id f.right
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.cos (x - ↑n * Real.pi) = (-1) ^ n * Real.cos x
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.done : ProofWidgets.LazyEncodable Lean.Json → ProofWidgets.CheckRequestResponse
-- Mathlib.Data.Tree.Basic
BinaryTree.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (value : α) (left right : BinaryTree α),
  sizeOf (BinaryTree.node value left right) = 1 + sizeOf value + sizeOf left + sizeOf right
-- Mathlib.Data.Set.Finite.Basic
Set.card_image_of_inj_on : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Fintype ↑s] {f : α → β} [inst_1 : Fintype ↑(f '' s)],
  (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Fintype.card ↑(f '' s) = Fintype.card ↑s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasStrictFDerivAt.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasStrictFDerivAt f₂ f₂' x → HasStrictFDerivAt (fun x => (f₂ x).2) (ContinuousLinearMap.snd 𝕜 F G ∘SL f₂') x
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function taking values in a complete lattice
and `g` tends to `atBot` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.  -/
Antitone.iSup_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  [OrderTop γ] {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instAddCommGroupHom : (R : Type) → [inst : Ring R] → (X Y : CategoryTheory.Mat R) → AddCommGroup (X ⟶ Y)
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuot_ext : ∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : NonAssocSemiring T] {r : R → R → Prop}
  (f g : RingQuot r →+* T), f.comp (RingQuot.mkRingHom r) = g.comp (RingQuot.mkRingHom r) → f = g
-- Mathlib.RingTheory.Ideal.Height
/-- **Alias** of `IsLocalization.height_under`. -/
IsLocalization.height_comap : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsLocalization S A] (J : Ideal A), (Ideal.under R J).height = J.height
-- Mathlib.Algebra.Ring.Int.Defs
Int.instIsCancelMulZero : IsCancelMulZero ℤ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
/-- If `U` is qcqs, then `Γ(X, D(f)) ≃ Γ(X, U)_f` for every `f : Γ(X, U)`.
This is known as the **Qcqs lemma** in [R. Vakil, *The rising sea*][RisingSea].  -/
AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] (f : ↑(X.presheaf.obj (Opposite.op ⊤))),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f))
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHom_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'),
  (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The inclusion map of the homology of a homological complex into its opcycles.  -/
HomologicalComplex.homologyι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i : ι) → [inst_2 : K.HasHomology i] → K.homology i ⟶ K.opcycles i
-- Mathlib.Order.OrderIsoNat
Nat.exists_subseq_of_forall_mem_union : ∀ {α : Type u_1} {s t : Set α} (e : ℕ → α),
  (∀ (n : ℕ), e n ∈ s ∪ t) → ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instNeg : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Neg R] → Neg (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.subtype_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (L : Sublattice α) (a : ↥L), L.subtype a = ↑a
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.l_inv : {C : Type u} → (X : CategoryTheory.FreeMonoidalCategory C) → X.Hom (CategoryTheory.FreeMonoidalCategory.unit.tensor X)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.norm_le_coeff' : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly) (k : ℤ),
  p = p'.mul k → k > 0 → (Int.Internal.Linear.Poly.denote ctx p ≤ 0 ↔ Int.Internal.Linear.Poly.denote ctx p' ≤ 0)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.add_bddBelow_range_add : ∀ {E : Type u_3} [inst : AddCommGroup E] {p q : NonarchAddGroupSeminorm E} {x : E},
  BddBelow (Set.range fun y => p y + q (x - y))
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.ext_fun_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β},
  κ = η ↔ ∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- For `p : ℝ` with `1 < p`, `fun x ↦ x ^ p` is strictly convex on $[0, +∞)$.  -/
strictConvexOn_rpow : ∀ {p : ℝ}, 1 < p → StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ p
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_eq_zero : ∀ {w : ℕ} {x : BitVec w} {start : ℕ}, BitVec.extractLsb' start 0 x = 0#0
-- Mathlib.Algebra.Group.Defs
/-- A monoid in which multiplication is right-cancellative.  -/
RightCancelMonoid : Type u → Type u
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.φ₁ (CategoryTheory.CategoryStruct.comp S.L₂.f h) =
    CategoryTheory.CategoryStruct.comp S.φ₂ h
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.score : Lean.Meta.LazyDiscrTree.PartialMatch → ℕ
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictDerivAt_exp_smul_const_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.ι_biproductComparison'_assoc : ∀ {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] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : F.obj (⨁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (F.obj ∘ f) j)
      (CategoryTheory.CategoryStruct.comp (F.biproductComparison' f) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.biproduct.ι f j)) h
-- Mathlib.Topology.Constructions.SumProd
ContinuousAt.comp₂_of_eq : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X}
  {y : Y × Z},
  ContinuousAt f y → ContinuousAt g x → ContinuousAt h x → (g x, h x) = y → ContinuousAt (fun x => f (g x, h x)) x
-- Mathlib.Analysis.Normed.Group.Defs
ContinuousENorm.toENorm : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ContinuousENorm E] → ENorm E
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  Submonoid.instCompleteLattice =
    { le := fun x1 x2 => x1 ≤ x2, lt := fun x1 x2 => x1 < x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfInf (Submonoid M) ⋯).toSupSet, isLUB_sSup := ⋯, toInfSet := Submonoid.instInfSet,
      isGLB_sInf := ⋯, toTop := Submonoid.instTop, le_top := ⋯, toBot := Submonoid.instBot, bot_le := ⋯ }
-- Init.Data.String.Defs
String.rawStartPos_eq : ∀ {s : String}, s.rawStartPos = 0
-- Init.System.IOError
IO.Error.mkInterrupted : String → UInt32 → String → IO.Error
-- Lean.Declaration
Lean.ReducibilityHints.isAbbrev : Lean.ReducibilityHints → Bool
-- Mathlib.CategoryTheory.EqToHom
/-- Reducible form of `congrArg_mpr_hom_left`  -/
CategoryTheory.congrArg_cast_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z),
  cast ⋯ q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
-- Mathlib.Topology.Defs.Induced
Topology.IsInducing.mk : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  tX = TopologicalSpace.induced f tY → Topology.IsInducing f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of `⊤` is the whole module as a submodule.  -/
AffineSubspace.direction_top : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], ⊤.direction = ⊤
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.refineOneHypercover_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀)
  (k : (F i j).I₀),
  (E.refineOneHypercover F).p₁ k =
    CategoryTheory.CategoryStruct.comp ((F i j).f k) (CategoryTheory.Limits.pullback.fst (E.f i) (E.f j))
-- Mathlib.Data.W.Basic
WType.mk.injEq : ∀ {α : Type u_1} {β : α → Type u_2} (a : α) (f : β a → WType β) (a_1 : α) (f_1 : β a_1 → WType β),
  (WType.mk a f = WType.mk a_1 f_1) = (a = a_1 ∧ f ≍ f_1)
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Use:
```
attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
  CategoryTheory.Discrete.discreteCases
```
to locally give `cat_disch` the ability to call `cases` on
`Discrete` and `(_ : Discrete _) ⟶ (_ : Discrete _)` hypotheses.
 -/
CategoryTheory.Discrete.discreteCases : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- A `2`-square consists of a natural transformation `T ⋙ R ⟶ L ⋙ B`
involving fours functors `T`, `L`, `R`, `B` that are on the
top/left/right/bottom sides of a square of categories.  -/
CategoryTheory.TwoSquare : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                CategoryTheory.Functor C₁ C₂ →
                  CategoryTheory.Functor C₁ C₃ →
                    CategoryTheory.Functor C₂ C₄ → CategoryTheory.Functor C₃ C₄ → Type (max u₁ v₄)
-- Mathlib.LinearAlgebra.LinearIndependent.BaseChange
/-- This is an auxiliary lemma dominated by `linearIndependent_algebraMap_comp_iff`.  -/
_private.Mathlib.LinearAlgebra.LinearIndependent.BaseChange.0.LinearIndependent.linearIndependent_algebraMap_comp_aux : ∀ {ι : Type u_1} {ι' : Type u_2} [Finite ι'] {K : Type u_3} (L : Type u_4) [inst : Field K] [inst_1 : Field L]
  [inst_2 : Algebra K L] {v : ι → ι' → K}, LinearIndependent K v → LinearIndependent L fun i => ⇑(algebraMap K L) ∘ v i
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- The map from a normed space with the weak topology into the weak-star bidual, as a continuous
linear map. Built using `LinearEquiv.arrowCongr` to properly bundle the topology changes via
`toWeakSpace` and `StrongDual.toWeakDual`.  -/
NormedSpace.inclusionInDoubleDualWeak : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (X : Type u_2) →
      [inst_1 : SeminormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → WeakSpace 𝕜 X →L[𝕜] WeakDual 𝕜 (StrongDual 𝕜 X)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_two : ∀ (x : ℝ), x ^ 2 = x ^ 2
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.Raw.keysIter.eq_1 : ∀ {α β : Type u} (m : Std.HashMap.Raw α β), m.keysIter = m.inner.keysIter
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_pos_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosStrictMono α],
  b < c → 0 < a → b * a < c * a
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i` on a neighbourhood `u` of `x`, if a section `t` has differentiable
coefficients at `x` w.r.t. `s i`, then `t` is differentiable at `x`.  -/
IsLocalFrameOn.mdifferentiableAt_of_coeff : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {x : M} {t : (x : M) → V x} [VectorBundle 𝕜 F V] (hs : IsLocalFrameOn I F 1 s u) [FiniteDimensional 𝕜 F],
  (∀ (i : ι), MDiffAt ((LinearMap.piApply (hs.coeff i)) t) x) → u ∈ nhds x → MDiffAt (T% t) x
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_add_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α},
  interior s + t ⊆ interior (s + t)
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.dfinsuppSum : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : Mul M]
  [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon M)
  (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c (h i 0) 0) →
    (∀ (i : ι), c (h' i 0) 0) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.sum h) (g.sum h')
-- Lean.Parser.Do
Lean.Parser.Term.doIfCond.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_const : ∀ {β : Type u_2} (α : Type u_5) [inst : MeasurableSpace α] [Nonempty α] (b : β),
  (MeasureTheory.SimpleFunc.const α b).range = {b}
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.isoEquivHomeo_symm_apply : ∀ {X Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  CompactlyGenerated.isoEquivHomeo.symm f = CompactlyGenerated.isoOfHomeo f
-- Mathlib.CategoryTheory.Monoidal.Category
/-- right whiskering for morphisms  -/
CategoryTheory.MonoidalCategoryStruct.whiskerRight : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      {X₁ X₂ : C} →
        (X₁ ⟶ X₂) →
          (Y : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.mk : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toFun : X → Y) → autoParam (Continuous toFun) ContinuousMap.continuous_toFun._autoParam → C(X, Y)