mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Simps.NotationClass
/-- The method to find the arguments of the class.  -/
Simps.AutomaticProjectionData.findArgs : Simps.AutomaticProjectionData → Lean.Name
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.le_iff_mem_closure : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x y : ProjectiveSpectrum 𝒜), x ≤ y ↔ y ∈ closure {x}
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₂ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x x_1 : data.I₀)
  (j : data.I₁ x x_1), data.toPreOneHypercover.p₂ j = F.map (data.p₂ j)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.instRingEquivClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β], RingEquivClass (α ≃+*o β) α β
-- Init.Data.Fin.Lemmas
Fin.mod_val : ∀ {n : ℕ} (a b : Fin n), ↑(a % b) = ↑a % ↑b
-- Mathlib.SetTheory.ZFC.Class
Class.mem_sUnion : ∀ {x y : Class.{u}}, y ∈ x.sUnion ↔ ∃ z ∈ x, y ∈ z
-- Mathlib.Topology.Compactness.Lindelof
/-- The preimage of a Lindelöf set under an inducing map is a Lindelöf set.  -/
Topology.IsInducing.isLindelof_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → IsClosed (Set.range f) → ∀ {K : Set Y}, IsLindelof K → IsLindelof (f ⁻¹' K)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top map in the oplax right unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            F ⟶
              ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp
                F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, Std.DTreeMap.Const.get (t₁ ∪ t₂) k h' = Std.DTreeMap.Const.get t₂ k ⋯
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_sup_left : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G) [K.Normal], K.relIndex (K ⊔ H) = K.relIndex H
-- Mathlib.Algebra.Symmetrized
SymAlg.instAdd : {α : Type u_1} → [Add α] → Add αˢʸᵐ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → ∀ {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).size = if k ∈ t then t.size else t.size + 1
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.onIocAux_apply : ∀ {α : Type u_1} [inst : LinearOrder α] {G : Type u_3} [inst_1 : AddCommGroup G] {f : α → G} {u v : α},
  u ≤ v → MeasureTheory.AddContent.onIocAux f (Set.Ioc u v) = f v - f u
-- Mathlib.Data.Finset.Filter
Finset.filter_eq_empty_iff : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, Finset.filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isConj_symm : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ.symm ↔ NumberField.ComplexEmbedding.IsConj φ σ
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.consRecOn_ofGroup : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {motive : HNNExtension.NormalWord d → Sort u_4} (g : G)
  (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g))
  (cons :
    (g : G) →
      (u : ℤˣ) →
        (w : HNNExtension.NormalWord d) →
          (h1 : w.head ∈ d.set u) →
            (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
              motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)),
  HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.ofGroup g) ofGroup cons = ofGroup g
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.mem_finAntidiagonal : ∀ {μ : Type u_2} [inst : AddCommMonoid μ] [inst_1 : Finset.HasAntidiagonal μ] [inst_2 : DecidableEq μ] {n : μ} {d : ℕ}
  {f : Fin d → μ}, f ∈ Finset.finAntidiagonal d n ↔ ∑ i, f i = n
-- Init.Data.Array.Sort.Lemmas
Array.map_mergeSort : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {xs : Array α},
  (∀ a ∈ xs, ∀ b ∈ xs, r a b = s (f a) (f b)) → Array.map f (xs.mergeSort r) = (Array.map f xs).mergeSort s
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_finsetProd : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} {s : Finset ι} {p : ι → Polynomial R} {n : ι → ℕ},
  (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X}
  (hf : CategoryTheory.CategoryStruct.comp f f = f)
  {c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f} (i i_1 : CategoryTheory.Limits.IsColimit c),
  i = i_1 →
    CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i =
      CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i_1
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.innerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → InnerProductSpace 𝕜 (UniformSpace.Completion E)
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_two_mul : ∀ {α : Type u_4} {f : α → α}, Function.Involutive f → ∀ (n : ℕ), f^[2 * n] = id
-- Mathlib.Logic.Function.Basic
Function.apply_update : ∀ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i)
  (g : (i : ι) → α i) (i : ι) (v : α i) (j : ι),
  f j (Function.update g i v j) = Function.update (fun k => f k (g k)) i (f i v) j
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (strict : Bool) (h : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof),
  sizeOf { p := p, strict := strict, h := h } = 1 + sizeOf p + sizeOf strict + sizeOf h
-- Mathlib.GroupTheory.Commutator.Basic
commutator_eq_bot : ∀ (G : Type u_1) [inst : Group G] [hG : IsMulCommutative G], commutator G = ⊥
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.toFilter : {α : Type u_2} → Ultrafilter α → Filter α
-- Std.Time.Time.PlainTime
/-- Creates a new `PlainTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value.
 -/
Std.Time.PlainTime.withMilliseconds : Std.Time.PlainTime → Std.Time.Millisecond.Ordinal → Std.Time.PlainTime
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.all.sizeOf_spec : sizeOf Lean.Meta.ApplyNewGoals.all = 1
-- Mathlib.Analysis.Complex.Trigonometric
/-- `Real.cosh` is always positive  -/
Real.cosh_pos : ∀ (x : ℝ), 0 < Real.cosh x
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_subtype : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), Subgroup.comap K.subtype H = H.subgroupOf K
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (semiringInst : Lean.Expr)
  (addFn? mulFn? powFn? natCastFn? : Option Lean.Expr) (id_1 : ℕ) (type_1 : Lean.Expr) (u_1 : Lean.Level)
  (semiringInst_1 : Lean.Expr) (addFn?_1 mulFn?_1 powFn?_1 natCastFn?_1 : Option Lean.Expr),
  ({ id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?, powFn? := powFn?,
        natCastFn? := natCastFn? } =
      { id := id_1, type := type_1, u := u_1, semiringInst := semiringInst_1, addFn? := addFn?_1, mulFn? := mulFn?_1,
        powFn? := powFn?_1, natCastFn? := natCastFn?_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          semiringInst = semiringInst_1 ∧
            addFn? = addFn?_1 ∧ mulFn? = mulFn?_1 ∧ powFn? = powFn?_1 ∧ natCastFn? = natCastFn?_1)
-- Lean.Expr
Lean.Nat.mkInstAdd : Lean.Expr
-- Mathlib.CategoryTheory.Sites.Finite
CategoryTheory.Pretopology.finite_toPrecoverage : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.Pretopology.finite C).toPrecoverage = CategoryTheory.Precoverage.finite C
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.localizationAway_jacobian : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  (Algebra.PreSubmersivePresentation.localizationAway S r).jacobian = (algebraMap R S) r
-- Init.MetaTypes
/-- If true (default: false), then once `givenNames` is exhausted, stop extracting lets. Otherwise continue extracting lets.  -/
Lean.Meta.ExtractLetsConfig.onlyGivenNames : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a left Kan extension of `F` along `L`, then this
is the induced bijection `(F' ⟶ G) ≃ (F ⟶ L ⋙ G)` for all `G`.  -/
CategoryTheory.Functor.homEquivOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] → (G : CategoryTheory.Functor D H) → (F' ⟶ G) ≃ (F ⟶ L.comp G)
-- Std.Http.Data.Response
/-- Builds an HTTP Response.
 -/
Std.Http.Response.Builder : Type
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkip?_prop_eq_none_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  pos.revSkip? P = none ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_inv_comp_iCycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).inv (groupHomology.iCycles A 1) =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (groupHomology.chainsIso₁ A).inv
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
orderOf_eq_card_of_zpowers_eq_top : ∀ {G : Type u_2} [inst : Group G] {g : G}, Subgroup.zpowers g = ⊤ → orderOf g = Nat.card G
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.zero_of_le_dist : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, f.rOut ≤ dist x c → ↑f x = 0
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : AddCommGroup A] [inst_12 : LieAddGroup I (↑⊤) A]
  (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
  instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U =
    { toAddGroup := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U, add_comm := ⋯ }
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets contains the whole set.  -/
MeasureTheory.IsSetAlgebra.univ_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → Set.univ ∈ 𝒜
-- Mathlib.Data.Num.Lemmas
Num.add_to_nat : ∀ (m n : Num), ↑(m + n) = ↑m + ↑n
-- Mathlib.Order.Monotone.Monovary
/-- `f` antivaries with `g` on `s` if `g i < g j` implies `f j ≤ f i` for all `i, j ∈ s`.  -/
AntivaryOn : {ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Preorder α] → [Preorder β] → (ι → α) → (ι → β) → Set ι → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.functor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C)
  {x x_1 : C} (g : x ⟶ x_1),
  (CategoryTheory.Limits.coprod.functor.obj X).map g =
    CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The sequence with `n`-th term `n ^ s * n! / (s * (s + 1) * ... * (s + n))`, for real `s`. We
will show that this tends to `Γ(s)` as `n → ∞`.  -/
Real.GammaSeq : ℝ → ℕ → ℝ
-- Init.Data.RArray
Lean.RArray.size : {α : Type u} → Lean.RArray α → ℕ
-- Init.Data.List.Lemmas
List.foldr_map_hom : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)
-- ProofWidgets.Component.FilterDetails
ProofWidgets.instRpcEncodableFilterDetailsProps : Lean.Server.RpcEncodable ProofWidgets.FilterDetailsProps
-- Mathlib.CategoryTheory.CatCommSq
/-- The vertical identity `CatCommSq`  -/
CategoryTheory.CatCommSq.vId : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        (T : CategoryTheory.Functor C₁ C₂) →
          CategoryTheory.CatCommSq T (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) T
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the top, bottom, suprema, and infima along a Galois insertion  -/
GaloisInsertion.liftBoundedOrder : {α : Type u} →
  {β : Type v} →
    {l : α → β} →
      {u : β → α} →
        [inst : PartialOrder β] → [inst_1 : Preorder α] → [BoundedOrder α] → GaloisInsertion l u → BoundedOrder β
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableOn.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ},
  DifferentiableOn ℝ f s → (∀ x ∈ s, f x ≠ 0 ∨ 1 ≤ p) → DifferentiableOn ℝ (fun x => f x ^ p) s
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.equivMatrix_apply : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n] (I : TwoSidedIdeal R), TwoSidedIdeal.equivMatrix I = TwoSidedIdeal.matrix n I
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_empty_left : ∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (a : α) → DecidablePred (r a)] (t : Finset β),
  Rel.interedges r ∅ t = ∅
-- Mathlib.Data.Set.Lattice
/-- This rather trivial consequence of `iInter_subset` is convenient with `apply`, and has `i`
explicit for this purpose.  -/
Set.iInter_subset_of_subset : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α} (i : ι), s i ⊆ t → ⋂ i, s i ⊆ t
-- Mathlib.Data.Finset.Slice
Set.sized_powersetCard : ∀ {α : Type u_1} (s : Finset α) (r : ℕ), Set.Sized r ↑(Finset.powersetCard r s)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.instIsSeparatedOfIsAffine : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X], X.IsSeparated
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.normedAddGroup : {E : Type u_2} → [NormedGroup E] → NormedAddGroup (Additive E)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.eqToHom_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (P : CategoryTheory.MorphismProperty T)
  (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (h : X = Y),
  (CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
-- Lean.Elab.Quotation
/-- Pattern is not quite sure yet; include unchanged in both branches  -/
Lean.Elab.Term.Quotation.MatchResult.undecided : Lean.Elab.Term.Quotation.MatchResult
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).isEmpty =
    l.isEmpty
-- Mathlib.Topology.Homotopy.TopCat.ToSSet
/-- If two morphisms `f : X ⟶ Y` and `g : X ⟶ Y` in `TopCat` are homotopic, then so
are their images by the functor `TopCat.toSSet : TopCat ⥤ SSet`.  -/
TopCat.Homotopy.toSSet : {X Y : TopCat} → {f g : X ⟶ Y} → TopCat.Homotopy f g → SSet.Homotopy (TopCat.toSSet.map f) (TopCat.toSSet.map g)
-- Lean.Meta.CollectMVars
/-- Similar to `getMVars`, but removes delayed assignments.  -/
Lean.Meta.getMVarsNoDelayed : Lean.Expr → Lean.MetaM (Array Lean.MVarId)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k k' : α},
  m.get? k = some k' ↔ ∃ (h : k ∈ m), m.get k h = k'
-- Mathlib.Data.Vector.Basic
/-- Define `motive v₁ v₂ v₃` by case-analysis on `v₁ : Vector α n`, `v₂ : Vector β n`, and
`v₃ : Vector γ n`.  -/
List.Vector.casesOn₃ : {α : Type u_1} →
  {m : ℕ} →
    {β : Type u_6} →
      {γ : Type u_7} →
        {motive : {n : ℕ} → List.Vector α n → List.Vector β n → List.Vector γ n → Sort u_8} →
          (v₁ : List.Vector α m) →
            (v₂ : List.Vector β m) →
              (v₃ : List.Vector γ m) →
                motive List.Vector.nil List.Vector.nil List.Vector.nil →
                  ({n : ℕ} →
                      (x : α) →
                        (y : β) →
                          (z : γ) →
                            (xs : List.Vector α n) →
                              (ys : List.Vector β n) →
                                (zs : List.Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) →
                    motive v₁ v₂ v₃
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
nonneg_of_le_add_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightReflectLE α] {a b : α}, b ≤ a + b → 0 ≤ a
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHAddOffset_4 : HAdd Std.Time.PlainTime Std.Time.Hour.Offset Std.Time.PlainTime
-- Init.Data.Nat.Bitwise.Lemmas
Nat.zero_testBit : ∀ (i : ℕ), Nat.testBit 0 i = false
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.sigmaIsoHom_inj : ∀ {S : Type u_1} {Y : Type u_2} (f : S → Y) [inst : TopologicalSpace S],
  Function.Injective ⇑(TopologicalSpace.Fiber.sigmaIsoHom f)
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `SyntaxNodeKind`s that are allowed to follow a flexible tactic:
`simp`, `simp_all`, `simpa`, `dsimp`, `grind`, `constructor`, `congr`, `done`, `rfl`, `ac_rfl`,
`omega` and `lia`, `grobner`
`abel` and `abel!`, `group`, `ring` and `ring!`, `module`, `field_simp` and `field`, `norm_num`,
`linarith`, `nlinarith` and `nlinarith!`, `norm_cast`, `tauto`,
`aesop`, `cfc_tac` (and `cfc_zero_tac` and `cfc_cont_tac`),
`continuity` and `measurability`, `finiteness`, `finiteness?`,
`split`, `split_ifs`.
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.flexible : Std.HashSet Lean.Name
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsMulComplexConjInv_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (u : (NumberField.RingOfIntegers K)ˣ),
  ↑((NumberField.IsCMField.unitsMulComplexConjInv K) u) = u * ((NumberField.IsCMField.unitsComplexConj K) u)⁻¹
-- Mathlib.Data.PNat.Basic
instAddPNat : Add ℕ+
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subRight.eq_1 : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  IsometryEquiv.subRight c = { toEquiv := Equiv.subRight c, isometry_toFun := ⋯ }
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_nnratCast : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ≥0), ‖↑q‖₊ = ↑q
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α},
  MeasurableSet s → ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.truncateToReal_nonneg : ∀ {t x : ENNReal}, 0 ≤ t.truncateToReal x
-- Mathlib.Order.Filter.Map
Filter.le_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β}, (∀ s ∈ f, m '' s ∈ g) → g ≤ Filter.map m f
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Construct an isomorphism between two objects in a monoidal category
out of unitors and associators.  -/
CategoryTheory.monoidalIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X Y : C) → [CategoryTheory.MonoidalCoherence X Y] → X ≅ Y
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_neg : ∀ {R : Type u_10} {M : Type u_11} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Set M),
  Submodule.span R (-s) = Submodule.span R s
-- Mathlib.Algebra.Polynomial.Eval.SMul
/-- `Polynomial.eval` as linear map  -/
Polynomial.leval : {R : Type u_1} → [inst : Semiring R] → R → Polynomial R →ₗ[R] R
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_le_centralizer_centralizer : ∀ {R : Type u_1} [inst : NonUnitalRing R] (s : Set R),
  NonUnitalSubring.closure s ≤ NonUnitalSubring.centralizer ↑(NonUnitalSubring.centralizer s)
-- Mathlib.Topology.Semicontinuity.Basic
/-- Given a family of lower semicontinuous functions `f : ι → α → β` such that
for each `x : α`, there is a choice `M x : ι` such that the maximum value of
evaluation at `x` is achieved by the function `f (M x)`, then the pointwise
maximum of the family `f` is lower semicontinuous.
In the statement we restrict to subsets `I : Set ι` and `s : Set α` for more generality.  -/
lowerSemicontinuousOn_of_forall_isMaxOn_and_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {ι : Type u_4} {f : ι → α → β}
  [inst_1 : Preorder β] {I : Set ι},
  (∀ i ∈ I, LowerSemicontinuousOn (f i) s) →
    ∀ {M : α → ι},
      (∀ x ∈ s, M x ∈ I) → (∀ x ∈ s, IsMaxOn (fun y => f y x) I (M x)) → LowerSemicontinuousOn (fun x => f (M x) x) s