mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instIsCentralScalar : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : SMul S R] [inst_4 : SMul Sᵐᵒᵖ R] [inst_5 : SMul S M] [inst_6 : SMul Sᵐᵒᵖ M]
  [inst_7 : IsScalarTower S R M] [inst_8 : IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M],
  IsCentralScalar S (AdicCompletion I M)
-- Mathlib.Analysis.Convex.Segment
mem_openSegment_translate : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a : E) {x b c : E}, a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of the Yoneda lemma.  -/
CategoryTheory.largeCurriedYonedaLemma : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅
      (CategoryTheory.evaluation Cᵒᵖ (Type v₁)).comp
        ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type v₁)
              (Type (max u₁ v₁))).obj
          CategoryTheory.uliftFunctor.{u₁, v₁})
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_multiset_count_of_subset : ∀ {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq M] (m : Multiset M) (s : Finset M),
  m.toFinset ⊆ s → m.prod = ∏ i ∈ s, i ^ Multiset.count i m
-- Mathlib.RingTheory.NoetherNormalization
/-- `hom2` is the composition of maps above, from `k[X_0,...X_(n-1)]` to `k[X_0,...X_n]/I`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.hom2 : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} →
      MvPolynomial (Fin (n + 1)) k →
        (I : Ideal (MvPolynomial (Fin (n + 1)) k)) → MvPolynomial (Fin n) k →ₐ[k] MvPolynomial (Fin (n + 1)) k ⧸ I
-- Lean.Data.Options
Lean.Options.empty : Lean.Options
-- Init.Data.List.Monadic
List.anyM_nil : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool}, List.anyM p [] = pure false
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fractRestrict_apply : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (x : E), ↑(ZSpan.fractRestrict b x) = ZSpan.fract b x
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Bijection between a submonoid `H` and its opposite.  -/
Submonoid.equivOp : {M : Type u_2} → [inst : MulOneClass M] → (H : Submonoid M) → ↥H ≃ ↥H.op
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.lift_card_range_le : ∀ {α : Type u} [inst : Small.{v, u} α] {f : α → ZFSet.{v}},
  Cardinal.lift.{u, v} (ZFSet.range f).card ≤ Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors'_cong : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  Associated a b → Associates.factors' a = Associates.factors' b
-- Mathlib.Geometry.Euclidean.Triangle
/-- Converse of pons asinorum, angle-at-point form.  -/
EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₃ p₂ →
    EuclideanGeometry.angle p₂ p₁ p₃ ≠ Real.pi → dist p₁ p₂ = dist p₁ p₃
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.concreteCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.ConcreteCategory (QuadraticModuleCat R) fun V W => V.form →qᵢ W.form
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {_m0 : MeasurableSpace Ω}
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.IndepSet s t κ μ → ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.below.of_subsingleton : ∀ {R : Type u_1} [inst : Ring R]
  {motive : (M : Type u_2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → IsFiniteLength R M → Prop}
  {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Subsingleton M], IsFiniteLength.below ⋯
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_toSignedMeasure : ∀ {X : Type u_2} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G]
  {μ : MeasureTheory.Measure X} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {f : X → G} {s : Set X},
  MeasurableSet s → ∫ᵛ (x : X) in s, f x ∂<•μ.toSignedMeasure = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.injOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.InjOn (↑e) e.source
-- Mathlib.Order.WithBot
WithTop.not_top_le_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), ¬⊤ ≤ ↑a
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_of_mem_unitary : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] [Nontrivial E] {U : E},
  U ∈ unitary E → ‖U‖ = 1
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_of_mem_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ ProbabilityTheory.integrableExpSet X μ → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Coercion of a `CovariantDerivative` to function  -/
CovariantDerivative.instCoeFunForallForallForallContinuousLinearMapIdTangentSpace : {𝕜 : 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 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            CoeFun (CovariantDerivative I F V) fun x =>
                                              ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V]
  [inst_2 : PartialOrder Γ'] [inst_3 : VAdd Γ Γ'] [inst_4 : IsOrderedCancelVAdd Γ Γ'] [inst_5 : Zero R]
  [inst_6 : AddCommMonoid V] (x : HahnSeries Γ R) (y : HahnModule Γ' R V) (a : Γ'),
  ((HahnModule.of R).symm (x • y)).coeff a =
    ∑ ij ∈ Finset.VAddAntidiagonal a ⋯, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_quadratic_lt : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3
-- Init.Data.Array.Lemmas
Array.map_inj : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1}, Array.map f = Array.map g ↔ f = g
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.toBaseIO.match_1.eq_1 : ∀ {ε α : Type} (motive : EST.Out ε IO.RealWorld α → Sort u_1) (a : α) (s : Void IO.RealWorld)
  (h_1 : (a : α) → (s : Void IO.RealWorld) → motive (EST.Out.ok a s))
  (h_2 : (ex : ε) → (s : Void IO.RealWorld) → motive (EST.Out.error ex s)),
  (match EST.Out.ok a s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error ex s => h_2 ex s) =
    h_1 a s
-- Mathlib.Topology.Defs.Basic
/-- This prevents `toTopology t x` being printed as `{ ofTopology := x }`
by `delabStructureInstance`.  -/
WithTopology.delabToTopology : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).getKey? a = none
-- Mathlib.Algebra.Order.Module.Field
Mathlib.Meta.Positivity.smul_ne_zero_of_pos_of_ne_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : Semiring α] [IsDomain α] [inst_2 : AddCommMonoid β] [inst_3 : Module α β]
  [Module.IsTorsionFree α β] {a : α} {b : β} [inst_5 : Preorder α], 0 < a → b ≠ 0 → a • b ≠ 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.mul_toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {n : Type u_11} {m : Type u_12} {n' : Type u_13}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁'] [inst_10 : Module R M₁']
  (b₁' : Module.Basis n' R M₁') [inst_11 : Fintype n'] [inst_12 : DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R)
  (M : Matrix n' n R),
  M * (LinearMap.toMatrix₂ b₁ b₂) B = (LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ (Matrix.toLin b₁' b₁) M.transpose)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.equiv_symm_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (ofVal : R), (WithVal.equiv v).symm ofVal = WithVal.toVal v ofVal
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k},
  (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_mul_le_pow : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X},
  Set.MapsTo T F F →
    ∀ [U.IsSymm] (m n : ℕ), Dynamics.coverMincard T F (U.comp U) (m * n) ≤ Dynamics.coverMincard T F U m ^ n
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: The `L^r` norm of the product of two functions is bounded by the
product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`.  -/
NNReal.Lr_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q r : ℝ},
  p.HolderTriple q r →
    (∑ i ∈ s, (f i * g i) ^ r) ^ (1 / r) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.map_mk_eq : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M} {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N),
  MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → MulArchimedeanClass.mk (f a) = MulArchimedeanClass.mk (f b)
-- Init.Data.Float.Float
instLTFloat : LT Float
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.sigma_J : UpperHalfPlane.σ UpperHalfPlane.J = Complex.conjCAE
-- Mathlib.Tactic.Ring.Common
/-- A total order on normalized expressions.
This is not an `Ord` instance because it is heterogeneous.
 -/
Mathlib.Tactic.Ring.Common.ExProd.cmp : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a → Mathlib.Tactic.Ring.Common.ExProd bt sα b → Ordering
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.d₂ : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (self : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
      self.simplex =
    e₀₁.edge
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toList_roc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...=n).toList[i]?.isSome = true) = (i < (n - m).toNat)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
MulPosReflectLT.toMulPosReflectLE : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsRightCancelMulZero α] [MulPosReflectLT α],
  MulPosReflectLE α
-- Mathlib.Tactic.DepRewrite
/-- Like `visitAndCast`, but does not insert casts at the top level.
The expected types of certain subterms are computed from `et?`.  -/
Mathlib.Tactic.DepRewrite.visit : Lean.Expr → Option Lean.Expr → Mathlib.Tactic.DepRewrite.M Lean.Expr
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.entryAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → ℕ → α × β → α × β
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.final_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.IsConnected D], (CategoryTheory.Prod.fst C D).Final
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_ofNat : ∀ {α : Type u_1} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : NormedRing R]
  [inst_1 : NormedSpace ℝ R] [CompleteSpace R] (n : ℕ) [inst_3 : n.AtLeastTwo] (f : α → R),
  μ[OfNat.ofNat n * f | m] =ᵐ[μ] OfNat.ofNat n * μ[f | m]
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM'.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.mk : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieRingModule L N] →
                        (toLieModuleHom : M →ₗ⁅R,L⁆ N) →
                          (invFun : N → M) →
                            Function.LeftInverse invFun (↑toLieModuleHom).toFun →
                              Function.RightInverse invFun (↑toLieModuleHom).toFun → M ≃ₗ⁅R,L⁆ N
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instSub : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Sub (SlashInvariantForm Γ k)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instPartialOrder : {M : Type u_1} → [inst : Add M] → PartialOrder (AddCon M)
-- Init.Data.Rat.Basic
Rat.normalize.dvd_num : ∀ {num : ℤ} {den g : ℕ}, g = num.natAbs.gcd den → ↑g ∣ num
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If the base ring is a field, then any injective linear map induces an injective map on
exterior powers.  -/
exteriorPower.map_injective_field : ∀ {n : ℕ} {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_4}
  [inst_2 : Field K] [inst_3 : Module K M] [inst_4 : Module K N] {f : M →ₗ[K] N},
  Function.Injective ⇑f → Function.Injective ⇑(exteriorPower.map n f)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.min! ∈ t}, t.get t.min! hc = t.min!
-- Init.Data.String.Modify
String.Pos.Raw.IsValid.set_of_le : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos} {q : String.Pos.Raw},
  String.Pos.Raw.IsValid s q → q ≤ p.offset → String.Pos.Raw.IsValid (p.set c hp) q
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.map_iInf : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] {ι : Sort u_1} [Nonempty ι] [inst_15 : IsScalarTower R B B] [inst_16 : SMulCommClass R B B]
  [inst_17 : StarModule R B] (f : F),
  Function.Injective ⇑f →
    ∀ (S : ι → NonUnitalStarSubalgebra R A),
      NonUnitalStarSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalStarSubalgebra.map f (S i)
-- Init.GrindInstances.Ring.UInt
UInt16.instOfNat.eq_1 : ∀ {n : ℕ}, UInt16.instOfNat = { ofNat := UInt16.ofNat n }
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKeyD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a fallback a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKeyD a fallback (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then a_1 else Std.DHashMap.Internal.AssocList.getKeyD a fallback es
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.mapHomologicalComplexXIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n m : ℤ)
  (hnm : n + 1 = m),
  CochainComplex.mappingCone.mapHomologicalComplexXIso φ H n =
    CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.mk.inj : ∀ {casesTypes : Lean.Meta.Grind.CasesTypes} {extThms : Lean.Meta.Grind.ExtTheorems} {funCC : Lean.NameSet}
  {ematch : Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem}
  {inj : Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem} {casesTypes_1 : Lean.Meta.Grind.CasesTypes}
  {extThms_1 : Lean.Meta.Grind.ExtTheorems} {funCC_1 : Lean.NameSet}
  {ematch_1 : Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem}
  {inj_1 : Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem},
  { casesTypes := casesTypes, extThms := extThms, funCC := funCC, ematch := ematch, inj := inj } =
      { casesTypes := casesTypes_1, extThms := extThms_1, funCC := funCC_1, ematch := ematch_1, inj := inj_1 } →
    casesTypes = casesTypes_1 ∧ extThms = extThms_1 ∧ funCC = funCC_1 ∧ ematch = ematch_1 ∧ inj = inj_1
-- Mathlib.Analysis.Calculus.SmoothSeries
fderiv_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {x₀ : E},
  Summable u →
    (∀ (n : α), Differentiable 𝕜 (f n)) →
      (∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n) →
        (Summable fun n => f n x₀) → (fderiv 𝕜 fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), fderiv 𝕜 (f n) x
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.isUnit : ∀ {n : Type u_2} [inst : Fintype n] {K : Type u_5} [inst_1 : Field K] [inst_2 : PartialOrder K] [inst_3 : StarRing K]
  [inst_4 : DecidableEq n] {M : Matrix n n K}, M.PosDef → IsUnit M
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.instHasPullbacksToPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks], E.toPreOneHypercover.HasPullbacks
-- Init.Data.UInt.Lemmas
UInt16.div_one : ∀ {a : UInt16}, a / 1 = a
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_right_eq_Ico_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert b (Set.Ico a b) = Set.Ico a (Order.succ b)
-- Lean.Parser.Extension
Lean.Parser.getParserCategory? : Lean.Environment → Lean.Name → Option Lean.Parser.ParserCategory
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 3 → H) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₃ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 3)) x) =
    ((Rep.Hom.hom φ).compLeft (G × G × G))
      ((LinearMap.funLeft k (↑A) (Prod.map (⇑f) (Prod.map ⇑f ⇑f)))
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₃ A).hom) x))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions : Type
-- Init.MetaTypes
/-- When `true` (default: `false`), unfolds applications of functions defined by pattern matching, when one of the patterns applies.
This can be enabled using the `simp!` syntax.
 -/
Lean.Meta.DSimp.Config.autoUnfold : Lean.Meta.DSimp.Config → Bool
-- Init.NotationExtra
unexpandMkArray8 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The restriction map `F.obj U ⟶ Π F.obj (U i)` gives a cone over the equalizer diagram
for the sheaf condition. The sheaf condition asserts this cone is a limit cone.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.fork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.Fork (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)
                (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.continuous_arccos : Continuous Real.arccos
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor reflects effective epimorphisms if morphisms that are mapped to epimorphisms are
themselves effective epimorphisms.
 -/
CategoryTheory.Functor.ReflectsEffectiveEpis.reflects : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsEffectiveEpis]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.EffectiveEpi (F.map f) → CategoryTheory.EffectiveEpi f
-- Mathlib.Data.Matrix.Basis
Matrix.sum_single_ofNat : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommMonoidWithOne α] [inst_2 : Fintype m] (n : ℕ)
  [inst_3 : n.AtLeastTwo], ∑ i, Matrix.single i i (OfNat.ofNat n) = OfNat.ofNat n