mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainTermGoalParams : Lean.ToJson Lean.Lsp.PlainTermGoalParams
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDerivWithin_mul_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {A : Type u_3} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A]
  {f g : E → A} {N : WithTop ℕ∞},
  ContDiffOn 𝕜 N f s →
    ContDiffOn 𝕜 N g s →
      UniqueDiffOn 𝕜 s →
        ∀ {x : E},
          x ∈ s →
            ∀ {n : ℕ},
              ↑n ≤ N →
                ‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) s x‖ ≤
                  ∑ i ∈ Finset.range (n + 1),
                    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_map_of_equiv : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (e : α ≃ β) (n : ℕ),
  (SimpleGraph.map (⇑e) G).cliqueSet n = Finset.map e.toEmbedding '' G.cliqueSet n
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
Unitization.lift_range_le : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : Semiring C]
  [inst_6 : Algebra R C] {f : A →ₙₐ[R] C} {S : Subalgebra R C},
  (Unitization.lift f).range ≤ S ↔ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mk.inj : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} {inst : Semiring A} {inst_1 : Semiring B}
  {inst_2 : SetLike σ A} {inst_3 : SetLike τ B} {𝒜 : ι → σ} {ℬ : ι → τ} {toRingHom : A →+* B}
  {map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom x ∈ ℬ i} {toRingHom_1 : A →+* B}
  {map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom_1 x ∈ ℬ i},
  { toRingHom := toRingHom, map_mem := map_mem } = { toRingHom := toRingHom_1, map_mem := map_mem_1 } →
    toRingHom = toRingHom_1
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryRightEquiv_symm_apply' : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×n]→L[𝕜] G →L[𝕜] G')
  (v : Fin (n + 1) → G), ((continuousMultilinearCurryRightEquiv' 𝕜 n G G').symm f) v = (f (Fin.init v)) (v (Fin.last n))
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.rank_bot_le_rank_of_isScalarTower : ∀ (R : Type u) (R' : Type u') [inst : Semiring R] [inst_1 : Semiring R'] (T : Type u') [inst_2 : Module R R']
  [inst_3 : NonAssocSemiring T] [inst_4 : Module R T] [inst_5 : Module R' T] [IsScalarTower R' T T] [FaithfulSMul R' T]
  [IsScalarTower R R' T], Module.rank R R' ≤ Module.rank R T
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.instIterator : {m : Type w → Type w'} → {α : Type w} → [Pure m] → Std.Iterator (Std.Iterators.Types.ArrayIterator α) m α
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.clm_postcomp : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃}
  {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.postcomp F₁ (f y)) s
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.mkSimprocExt : autoParam Lean.Name Lean.Meta.Simp.mkSimprocExt._auto_1 →
  Option (IO.Ref Lean.Meta.Simprocs) → IO Lean.Meta.Simp.SimprocExtension
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `C` has a terminal object and binary products, then it has finite products.  -/
CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.HasTerminal C], CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Map a configuration across a function, given `f : Γ → Γ'` a map of the alphabets and
`g : Λ → Λ'` a map of the machine states.  -/
Turing.TM0.Cfg.map : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {Γ' : Type u_2} →
      [inst_1 : Inhabited Γ'] →
        {Λ : Type u_3} → {Λ' : Type u_4} → Turing.PointedMap Γ Γ' → (Λ → Λ') → Turing.TM0.Cfg Γ Λ → Turing.TM0.Cfg Γ' Λ'
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_inj : ∀ {a b : UInt8}, a.toUInt32 = b.toUInt32 ↔ a = b
-- Mathlib.FieldTheory.KummerExtension
KummerExtension.«termK[_√_]» : Lean.ParserDescr
-- Lean.Meta.MatchUtil
Lean.Meta.matchHelper? : {α : Type} → Lean.Expr → (Lean.Expr → Lean.MetaM (Option α)) → Lean.MetaM (Option α)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.retract_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g) {Z_1 : C} (h_1 : (CategoryTheory.Arrow.mk f).right ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right h.i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right h.r) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) h_1
-- Mathlib.CategoryTheory.Limits.Unit
/-- A trivial cocone for a functor into `PUnit`. `punitCoconeIsLimit` shows it is a colimit.  -/
CategoryTheory.Limits.punitCocone : {J : Type v} →
  [inst : CategoryTheory.Category.{v', v} J] →
    {F : CategoryTheory.Functor J (CategoryTheory.Discrete PUnit.{u_1 + 1})} → CategoryTheory.Limits.Cocone F
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.mk.sizeOf_spec : ∀ (userName : Lean.Name) (type value : Lean.Expr) (binderInfo : Lean.BinderInfo) (kind : Lean.LocalDeclKind),
  sizeOf { userName := userName, type := type, value := value, binderInfo := binderInfo, kind := kind } =
    1 + sizeOf userName + sizeOf type + sizeOf value + sizeOf binderInfo + sizeOf kind
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.get! a = (t.get? a).get!
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.IterM.foldM (fun d b => if f b = true then g d b else pure d) init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filter f it) ⦃Q⦄
-- Mathlib.Order.CompleteLattice.Basic
le_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i),
  f i j ≤ ⨆ i, ⨆ j, f i j
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_zero : Encodable.decode 0 = some false
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftUnitor_hom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).hom
-- Init.Data.Hashable
instHashableUSize : Hashable USize
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toSubmonoid_strictMono : ∀ {G : Type u_1} [inst : Group G], StrictMono Subgroup.toSubmonoid
-- Mathlib.Order.UpperLower.Fibration
Relation.Fibration.isUpperSet_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LE α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f → ∀ {s : Set α}, IsUpperSet s → IsUpperSet (f '' s)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {f : ι → E → 𝔸} {l : List ι} {x : E},
  (∀ i ∈ l, DifferentiableAt 𝕜 (fun x => f i x) x) →
    fderiv 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) x =
      ∑ i,
        (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
          MulOpposite.op (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod • fderiv 𝕜 (fun x => f l[i] x) x
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance1.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
      a = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a_1 x b) y c → False) →
    (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
        a = RBTree.RBNode.node RBTree.RBColor.red a_1 x (RBTree.RBNode.node RBTree.RBColor.red b y c) → False) →
      (match a, x, b with
        | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d =>
          h_1 a x b y c z d
        | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d =>
          h_2 a x b y c z d
        | a, x, b => h_3 a x b) =
        h_3 a x b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.distinct_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) t.toList
-- Init.Data.Vector.Range
Vector.range'_eq_map_range : ∀ {s n : ℕ}, Vector.range' s n = Vector.map (fun x => s + x) (Vector.range n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, List.map Sigma.fst t.toList = t.keys
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_filter_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool}, (Std.ExtHashSet.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom : Inhabited Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mul_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LinearOrderedCommMonoidWithZero α]
  [inst_1 : LinearOrderedCommMonoidWithZero β] [inst_2 : LinearOrderedCommMonoidWithZero γ] (g₁ g₂ : β →*₀o γ)
  (f : α →*₀o β), (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
-- Mathlib.Topology.Algebra.Monoid
continuous_nsmul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] (n : ℕ), Continuous fun a => n • a
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presheaf.isSheaf_sup : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (K L : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.Presheaf.IsSheaf (K ⊔ L).toGrothendieck P ↔
    CategoryTheory.Presheaf.IsSheaf K.toGrothendieck P ∧ CategoryTheory.Presheaf.IsSheaf L.toGrothendieck P
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, (Std.ExtDHashMap.filter f m).get? k = Option.filter (f k) (m.get? k)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.addCommute_subtype_of_addCommute : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G},
  (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) →
    ∀ (i j : ι), i ≠ j → ∀ (x : ↥(H i)) (y : ↥(H j)), AddCommute ((H i).subtype x) ((H j).subtype y)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.isProbabilityMeasure : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ],
  ProbabilityTheory.HasLaw X μ P → MeasureTheory.IsProbabilityMeasure P
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_tmod_right : ∀ (a b : ℤ), (-(a * b)).tmod a = 0
-- Mathlib.Data.NNRat.Defs
NNRat.den_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).den = 1
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The forgetful functor from the category of algebras, forgetting the algebraic structure.  -/
CategoryTheory.Endofunctor.Algebra.forget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Algebra F) C
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Given an `R`-algebra `S` and an `S`-algebra `T` with pre-submersive presentations,
this is the canonical pre-submersive presentation of `T` as an `R`-algebra.  -/
Algebra.PreSubmersivePresentation.comp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {ι' : Type u_1} →
                {σ' : Type u_2} →
                  {T : Type u_3} →
                    [inst_3 : CommRing T] →
                      [inst_4 : Algebra R T] →
                        [inst_5 : Algebra S T] →
                          [IsScalarTower R S T] →
                            Algebra.PreSubmersivePresentation S T ι' σ' →
                              Algebra.PreSubmersivePresentation R S ι σ →
                                Algebra.PreSubmersivePresentation R T (ι' ⊕ ι) (σ' ⊕ σ)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.findSomeRevM?.find : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (α → m (Option β)) → (as : Array α) → (i : ℕ) → i ≤ as.size → m (Option β)
-- Mathlib.Topology.Neighborhoods
IsClosed.compl_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsClosed s → x ∉ s → sᶜ ∈ nhds x
-- Mathlib.Analysis.Normed.Group.Uniform
NormedAddGroup.to_isIsometricVAdd : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], IsIsometricVAdd E E
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_min : ∀ {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : LinearOrder M] (f g : α → M),
  (Function.mulSupport fun x => min (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.Algebra.Group.Subgroup.Order
abs_mem_iff : ∀ {S : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : LinearOrder G] {x : SetLike S G} [NegMemClass S G] {H : S}
  {x_1 : G}, |x_1| ∈ H ↔ x_1 ∈ H
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
Preorder.coconeOfUpperBound.congr_simp : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {x x_1 : C} (e_x : x = x_1) (h : x ∈ upperBounds (Set.range F.obj)),
  Preorder.coconeOfUpperBound F h = Preorder.coconeOfUpperBound F ⋯
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Zero loci of prime ideals are closed irreducible sets in the Zariski topology and any closed
irreducible set is a zero locus of some prime ideal.
 -/
PrimeSpectrum.pointsEquivIrreducibleCloseds : (R : Type u) → [inst : CommSemiring R] → PrimeSpectrum R ≃o (TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R))ᵒᵈ
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovDist.eq_1 : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovDist μ ν = (MeasureTheory.levyProkhorovEDist μ ν).toReal
-- Init.Data.Int.LemmasAux
Int.max_self_assoc' : ∀ {m n : ℤ}, max n (max m n) = max n m
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiable_proj : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E], MDiff Bundle.TotalSpace.proj
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by inclusion of the first factor.  -/
ContinuousMonoidHom.inl : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A →ₜ* A × B
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.isCongruenceSubgroup_trans : ∀ (H K : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)),
  H ≤ K → CongruenceSubgroup.IsCongruenceSubgroup H → CongruenceSubgroup.IsCongruenceSubgroup K
-- Mathlib.Algebra.Group.Basic
sub_sub_eq_add_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α), a - (b - c) = a + c - b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V} (p : G.Walk u₁ v₁) (q : G.Walk u₂ v₂),
  p.IsSubwalk q = ∃ ru rv, q = (ru.append p).append rv
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km fallback : α},
        Std.Internal.List.minKeyD l fallback = km ↔
          Std.Internal.List.getKey? km l = some km ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Mathlib.Combinatorics.HalesJewett
/-- **Alias** of the reverse direction of `Combinatorics.Line.toSubspace_isMono`. -/
Combinatorics.Line.IsMono.toSubspace : ∀ {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line (η → α) ι} {C : (ι × η → α) → κ},
  Combinatorics.Line.IsMono
      (fun x =>
        C fun x_1 =>
          match x_1 with
          | (i, e) => x i e)
      l →
    Combinatorics.Subspace.IsMono C l.toSubspace
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.ext : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A} {x y : F.Hom G},
  x.hom = y.hom → x = y
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_toArray_roc : ∀ {a b : ℤ}, (a<...=b).toArray.size = (b - a).toNat
-- Init.Data.List.Lemmas
List.head_filterMap_of_eq_some : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.head w) = some b),
  (List.filterMap f l).head ⋯ = b
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_matrix_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup n ℤ),
  ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g) = (↑g).map ⇑(Int.castRingHom R)
-- Mathlib.Data.Finsupp.Single
Finsupp.coe_update : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) [inst_1 : DecidableEq α],
  ⇑(f.update a b) = Function.update (⇑f) a b
-- Mathlib.Algebra.Lie.OfAssociative
LieAlgebra.ad_apply : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L),
  ((LieAlgebra.ad R L) x) y = ⁅x, y⁆
-- Init.Data.Int.DivMod.Bootstrap
Int.one_dvd : ∀ (n : ℤ), 1 ∣ n
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.not_isLeftInversion_mul_right_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ {w : W}, ¬cs.IsLeftInversion (t * w) t ↔ cs.IsLeftInversion w t
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.toStalk.eq_1 : ∀ (R : Type u) [inst : CommRing R] (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  AlgebraicGeometry.StructureSheaf.toStalk R x =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op ⊤))))
      ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ ⊤ x trivial)
-- Init.Data.Array.Lemmas
Array.flatten_flatten : ∀ {α : Type u_1} {xss : Array (Array (Array α))}, xss.flatten.flatten = (Array.map Array.flatten xss).flatten
-- Aesop.Rule.Name
Aesop.BuilderName.tactic.sizeOf_spec : sizeOf Aesop.BuilderName.tactic = 1
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_g₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (c.ofArrowIso e).g₁ = CategoryTheory.CategoryStruct.comp c.g₁ (CategoryTheory.Arrow.leftFunc.map e.hom)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.adj_counit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.adj.counit = ContinuousGeneratedByCat.adjCounit
-- Mathlib.CategoryTheory.EpiMono
/-- Split epimorphisms are also absolute epimorphisms.  -/
CategoryTheory.SplitEpi.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y : C} →
          {f : X ⟶ Y} → CategoryTheory.SplitEpi f → (F : CategoryTheory.Functor C D) → CategoryTheory.SplitEpi (F.map f)
-- Mathlib.Data.Set.Function
Set.InjOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β}, s₁ ⊆ s₂ → Set.InjOn f s₂ → Set.InjOn f s₁