mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fromProd_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y),
  ((CategoryTheory.Comma.fromProd L R).map f).right = f.2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙAux.eq_1 : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁],
  cfcₙAux hp₁ a ha =
    ((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp
      ContinuousMapZero.toContinuousMapHom
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eq_some_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  {fallback : β a},
  Std.Internal.List.containsKey a l = true →
    Std.Internal.List.getValueCast? a l = some (Std.Internal.List.getValueCastD a l fallback)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Differentiable.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ},
  Differentiable ℂ f → Differentiable ℂ fun x => Complex.sinh (f x)
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.instCoeByteArray : Coe ByteArray Std.Http.Internal.ChunkedBuffer
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instLeAtTopSymmetricIco : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] [NoTopOrder G], (SummationFilter.symmetricIco G).LeAtTop
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
/-- The particular case of `hasCardinalLT_prod` when all the inputs are in the
same universe `w`. It is used to prove the general case.  -/
hasCardinalLT_prod' : ∀ {T₁ T₂ : Type w} {κ : Cardinal.{w}},
  Cardinal.aleph0 ≤ κ → HasCardinalLT T₁ κ → HasCardinalLT T₂ κ → HasCardinalLT (T₁ × T₂) κ
-- Mathlib.Order.CompleteLattice.Basic
iInf_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α},
  iInf f = ⨅ i, ⨅ (h : p i), f ⟨i, h⟩
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rank_lt : ∀ {self : Batteries.UnionFind} {i : ℕ}, self.parent i ≠ i → self.rank i < self.rank (self.parent i)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.role : Lean.Elab.DocElabKind
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_iff : ∀ {R : Type u_3} [inst : CommRing R], IsJacobsonRing R ↔ ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
-- Std.Data.String.ToInt
String.isInt_toSlice : ∀ {s : String}, s.toSlice.isInt = s.isInt
-- Mathlib.Algebra.Divisibility.Basic
dvd_trans : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
-- Init.Data.List.Basic
List.length.eq_1 : ∀ {α : Type u_1}, [].length = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Y_eq_iff : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → (P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 ↔ P 1 / P 2 ^ 3 = Q 1 / Q 2 ^ 3)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_le_of_left_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => c ≤ x],
  a ≤ c → Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico c b
-- Mathlib.Order.OrderDual
Equiv.top_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Top β], ⊤ = e.symm ⊤
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.lid_comp_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : N →ₗ[R] R),
  ↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M f = TensorProduct.lift (LinearMap.lsmul R M ∘ₗ f)
-- Mathlib.Data.Int.Fib.Basic
Int.fib_add_two : ∀ (n : ℤ), Int.fib (n + 2) = Int.fib n + Int.fib (n + 1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {he : t.isEmpty = false} {hc : Std.DTreeMap.Internal.Impl.contains (t.minKey he) t = true},
      t.getKey (t.minKey he) hc = t.minKey he
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonServerInfo.fromJson : Lean.Json → Except String Lean.Lsp.ServerInfo
-- Mathlib.SetTheory.Cardinal.Pigeonhole
Cardinal.infinite_pigeonhole_set : ∀ {β α : Type u} {s : Set β} (f : ↑s → α),
  ∀ θ ≤ Cardinal.mk ↑s,
    Cardinal.aleph0 ≤ θ →
      Cardinal.mk α < θ.ord.cof → ∃ a t, ∃ (h : t ⊆ s), θ ≤ Cardinal.mk ↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.prev : ∀ (α : Type u_2) [inst : AddGroup α] [inst_1 : One α] (i : α), (ComplexShape.up α).prev i = i - 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lieSpan.eq_1 : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (s : Set M), LieSubmodule.lieSpan R L s = sInf {N | s ⊆ ↑N}
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The initial object of `Top` is `PEmpty`.  -/
TopCat.initialIsoPEmpty : ⊥_ TopCat ≅ TopCat.of PEmpty.{u + 1}
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfSurjective_symm_apply : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f) (a : A),
  (Ideal.quotientKerAlgEquivOfSurjective hf).symm (f a) = (Ideal.Quotient.mk (RingHom.ker f)) a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceToSingleton : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is `r`-Hölder over a bounded space, then it is also `s`-Hölder when `s ≤ r`.
See `MemHolder.of_le'` for the version in a pseudoemetric space.  -/
MemHolder.of_le : ∀ {Y : Type u_2} [inst : PseudoEMetricSpace Y] {r : NNReal} {X : Type u_3} [inst_1 : PseudoMetricSpace X]
  [hX : BoundedSpace X] {f : X → Y} {s : NNReal}, MemHolder r f → s ≤ r → MemHolder s f
-- Mathlib.Order.Filter.Pointwise
Filter.smul_tendsto_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Group γ] [inst_1 : MulAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, Filter.Tendsto (c • m) f (c • g) ↔ Filter.Tendsto m f g
-- Mathlib.Analysis.Normed.Group.Basic
enorm_add₃_le : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] {a b c : E},
  ‖a + b + c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.surjective_or_eq_zero : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} [ρ.IsIrreducible] (g : σ.IntertwiningMap ρ),
  Function.Surjective ⇑g ∨ g = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- The scaling of a finset `s` by a scalar `a`: `a • s = {a • x | x ∈ s}`.  -/
Finset.smulFinset : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [SMul α β] → SMul α (Finset β)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
  [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {x : E}, AnalyticAt 𝕜' f x → AnalyticAt 𝕜 f x
-- Lean.Expr
/-- Return `some p` if `e` is an annotated pattern (`inaccessible?` or `patternWithRef?`)  -/
Lean.patternAnnotation? : Lean.Expr → Option Lean.Expr
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.findAtom_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α], IsPredArchimedean.findAtom ⊥ = ⊥
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.superset : ∀ {α : Type u_2} {M : Matroid α} {S T : Set α},
  M.Spanning S → S ⊆ T → autoParam (T ⊆ M.E) Matroid.Spanning.superset._auto_1 → M.Spanning T
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_zero : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R], IsAlgebraic R 0
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_ofNat_of_le_of_lt : ∀ {w v x : ℕ}, w ≤ v → x < 2 ^ w → BitVec.setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x
-- Lean.Data.Lsp.Basic
/-- The `workspace/applyEdit` request is sent from the server to the client to modify resource on the client side.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#applyWorkspaceEditParams)  -/
Lean.Lsp.ApplyWorkspaceEditParams : Type
-- Mathlib.GroupTheory.Commutator.Basic
commutator.eq_1 : ∀ (G : Type u_1) [inst : Group G], commutator G = ⁅⊤, ⊤⁆
-- Mathlib.Topology.MetricSpace.Bounded
/-- The diameter of a closed ball of radius `r` is at most `2 r`.  -/
Metric.diam_closedBall : ∀ {α : Type u} {x : α} [inst : PseudoMetricSpace α] {r : ℝ}, 0 ≤ r → Metric.diam (Metric.closedBall x r) ≤ 2 * r
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forgetId_inv_app : ∀ (W : Type v') [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] (C : Type u₁)
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  (CategoryTheory.EnrichedFunctor.forgetId W C).inv.app X = CategoryTheory.CategoryStruct.id X
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_add : ∀ {a b c : ℤ}, a ∣ b → a ∣ c → a ∣ b + c
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.comp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.FormallyUnramified → g.FormallyUnramified → (g.comp f).FormallyUnramified
-- Mathlib.Topology.VectorBundle.Basic
/-- The projection on the base of a vector bundle created from core is continuous  -/
VectorBundleCore.continuous_proj : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
  Continuous Z.proj
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.quotient_obj_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  Function.Surjective (HomotopyCategory.Plus.quotient C).obj
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_withConstants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S) {x : M},
  x ∈ S.withConstants h ↔ x ∈ S
-- Mathlib.RingTheory.RootsOfUnity.Basic
mem_rootsOfUnity_iff_isRoot : ∀ {R : Type u_4} [inst : CommRing R] (k : ℕ) (ζ : Rˣ), ζ ∈ rootsOfUnity k R ↔ (Polynomial.X ^ k - 1).IsRoot ↑ζ
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalNonAssocCommRingQuotient : {R : Type u_1} → [inst : NonUnitalNonAssocCommRing R] → (c : RingCon R) → NonUnitalNonAssocCommRing c.Quotient
-- Init.Data.List.Lex
/-- Variant of `lex_eq_true_iff` using an arbitrary comparator.  -/
List.lex_eq_true_iff_lex : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] (lt : α → α → Bool),
  l₁.lex l₂ lt = true ↔ List.Lex (fun x y => lt x y = true) l₁ l₂
-- Std.Data.DTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Const.toArray : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → Array (α × β)
-- Mathlib.Topology.NhdsSet
nhdsSet.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), nhdsSet s = sSup (nhds '' s)
-- Std.Do.PredTrans
/-- The predicate transformer is conjunctive: `t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂`.
So the stronger the postcondition, the stronger the resulting precondition.
 -/
Std.Do.PredTrans.conjunctiveRaw : ∀ {ps : Std.Do.PostShape} {α : Type u} (self : Std.Do.PredTrans ps α), Std.Do.PredTrans.Conjunctive self.trans
-- Lean.Meta.Tactic.UnifyEq
_private.Lean.Meta.Tactic.UnifyEq.0.Lean.Meta.unifyEq?.injection : Lean.MVarId →
  Lean.FVarId →
    Lean.Meta.FVarSubst →
      Option Lean.Name →
        Lean.LocalDecl →
          (Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.MVarId)) →
            Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Meta.UnifyEqResult)
-- Mathlib.CategoryTheory.Limits.Preserves.Ulift
/-- The functor `uliftFunctor : Type u ⥤ Type (max u v)` creates `u`-small limits.
 -/
CategoryTheory.Limits.Types.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}
-- Mathlib.NumberTheory.Dioph
/-- Deleting the first component preserves the Diophantine property.  -/
Dioph.«termD∃» : Lean.ParserDescr
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_fn_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective DFunLike.coe
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminormAux_smul : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (a : 𝕜),
  PiTensorProduct.projectiveSeminormAux ((FreeAddMonoid.map fun y => (a * y.1, y.2)) p) =
    ‖a‖ * PiTensorProduct.projectiveSeminormAux p
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceEditClientCapabilities.mk.inj : ∀ {documentChanges? : Option Bool} {changeAnnotationSupport? : Option Lean.Lsp.ChangeAnnotationSupport}
  {resourceOperations? : Option (Array String)} {documentChanges?_1 : Option Bool}
  {changeAnnotationSupport?_1 : Option Lean.Lsp.ChangeAnnotationSupport}
  {resourceOperations?_1 : Option (Array String)},
  { documentChanges? := documentChanges?, changeAnnotationSupport? := changeAnnotationSupport?,
        resourceOperations? := resourceOperations? } =
      { documentChanges? := documentChanges?_1, changeAnnotationSupport? := changeAnnotationSupport?_1,
        resourceOperations? := resourceOperations?_1 } →
    documentChanges? = documentChanges?_1 ∧
      changeAnnotationSupport? = changeAnnotationSupport?_1 ∧ resourceOperations? = resourceOperations?_1
-- Mathlib.Order.CompleteLattice.Basic
iSup_const_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {a : α}, ⨆ x, a ≤ a
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id η).as.app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeActionResolveData.mk.inj : ∀ {params : Lean.Lsp.CodeActionParams} {providerName : Lean.Name} {providerResultIndex : ℕ}
  {params_1 : Lean.Lsp.CodeActionParams} {providerName_1 : Lean.Name} {providerResultIndex_1 : ℕ},
  { params := params, providerName := providerName, providerResultIndex := providerResultIndex } =
      { params := params_1, providerName := providerName_1, providerResultIndex := providerResultIndex_1 } →
    params = params_1 ∧ providerName = providerName_1 ∧ providerResultIndex = providerResultIndex_1
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_exists_morphismRestrict : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}, (∀ (x : ↥Y), ∃ U, x ∈ U ∧ P (f ∣_ U)) → P f
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_mono_right : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (K : Subgroup G), Monotone fun t => K.prod t
-- Batteries.Recycling.RBTree.Basic
/-- The result of `toStream` on a `Values`.  -/
RBTree.RBMap.Values.Stream : Type u_1 → Type u_2 → Type (max u_2 u_1)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.congr_simp : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v v_1 : Valuation A Γ)
  (e_v : v = v_1) [hv : v.IsRankOneDiscrete] (π π_1 : A), π = π_1 → v.IsUniformizer π = v_1.IsUniformizer π_1
-- Init.Data.Array.Lemmas
Array.exists_push_of_ne_empty : ∀ {α : Type u_1} {xs : Array α}, xs ≠ #[] → ∃ ys a, xs = ys.push a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} {fallback : γ} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filterMap! f t) k fallback =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.dep.visitApp : (Lean.FVarId → Bool) → (Lean.MVarId → Bool) → Lean.Expr → Lean.DependsOn.M✝ Bool
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.l_inv_hom : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.l_inv X).comp (CategoryTheory.FreeMonoidalCategory.Hom.l_hom X))
    (CategoryTheory.FreeMonoidalCategory.Hom.id X)
-- Mathlib.Data.Prod.Lex
/-- Variant of `Prod.Lex.lt_iff` for partial orders.  -/
Prod.Lex.lt_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {x y : Lex (α × β)},
  x < y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 < (ofLex y).2)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_blockDiagonal : ∀ {m : Type u_1} {n : Type u_2} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : Ring 𝔸] [inst_5 : TopologicalSpace 𝔸] [inst_6 : IsTopologicalRing 𝔸] [T2Space 𝔸]
  [Algebra ℚ 𝔸] (v : m → Matrix n n 𝔸),
  NormedSpace.exp (Matrix.blockDiagonal v) = Matrix.blockDiagonal (NormedSpace.exp v)
-- Mathlib.Data.Fintype.Quotient
/-- Recursion principle for quotients indexed by a finite type.  -/
Quotient.finRecOn : {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] →
      {α : ι → Sort u_2} →
        {S : (i : ι) → Setoid (α i)} →
          {C : ((i : ι) → Quotient (S i)) → Sort u_4} →
            (q : (i : ι) → Quotient (S i)) →
              (f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧) →
                (∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), ⋯ ▸ f a = f b) → C q
-- Mathlib.Data.NNReal.Basic
NNReal.coe_list_prod : ∀ (l : List NNReal), ↑l.prod = (List.map NNReal.toReal l).prod
-- Mathlib.Analysis.Convex.Exposed
ContinuousLinearMap.toExposed.isExposed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {l : StrongDual 𝕜 E} {A : Set E},
  IsExposed 𝕜 A (ContinuousLinearMap.toExposed l A)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₂_obj_p_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (i : ℕ),
  (AlgebraicTopology.DoldKan.N₂.obj P).p.f i =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f i) (P.p.app (Opposite.op { len := i }))
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.sub_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsUpperSet s → IsUpperSet (s - t)
-- Mathlib.Order.Grade
GradeMinOrder.mk : {𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        [toGradeOrder : GradeOrder 𝕆 α] → (∀ ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a)) → GradeMinOrder 𝕆 α
-- Mathlib.Algebra.Module.PointwisePi
smul_pi_subset : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → SMul K (R i)] (r : K) (s : Set ι)
  (t : (i : ι) → Set (R i)), r • s.pi t ⊆ s.pi (r • t)
-- Mathlib.Order.Hom.Lattice
InfHom.instMin.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β],
  InfHom.instMin = { min := fun f g => { toFun := ⇑f ⊓ ⇑g, map_inf' := ⋯ } }
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) (J : Type u_3) [inst_1 : CategoryTheory.Category.{v_3, u_3} J]
  {X Y : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X ⟶ Y) (j : J),
  ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).map τ).app j =
    data.mapZ
      (CategoryTheory.Arrow.homMk ((CategoryTheory.Arrow.Hom.left τ).app j) ((CategoryTheory.Arrow.Hom.right τ).app j)
        ⋯)
-- Mathlib.Data.Multiset.ZeroCons
/-- Companion to `Multiset.rec` with more convenient argument order.  -/
Multiset.recOn : {α : Type u_1} →
  {C : Multiset α → Sort u_3} →
    (m : Multiset α) →
      C 0 →
        (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) →
          (∀ (a a' : α) (m : Multiset α) (b : C m),
              C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) →
            C m
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData_Q : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).RightHomologyData),
  (HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).Q = h.Q
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.equivPolynomialSelf_apply_eq : ∀ {R : Type u_2} [inst : CommRing R] (p : PolynomialModule R R),
  PolynomialModule.equivPolynomialSelf p = PolynomialModule.equivPolynomial p
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. (See
`Orientation.inner_mul_inner_add_areaForm_mul_areaForm` for the "applied" form.)  -/
Orientation.inner_mul_inner_add_areaForm_mul_areaForm' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x : E),
  inner ℝ a x • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLTOffset : LT Std.Time.Second.Offset
-- Init.Data.Int.Order
Int.max_le : ∀ {a b c : ℤ}, max a b ≤ c ↔ a ≤ c ∧ b ≤ c