mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.WhiskerRight → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.toOrderHom : {α : Type u_6} → {β : Type u_7} → [inst : Preorder α] → [inst_1 : Preorder β] → PseudoEpimorphism α β → α →o β
-- Lean.Parser.Term
Lean.Parser.Term.ensureTypeOf.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_monoidHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective MonoidHomClass.toMonoidHom
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.eqToHom_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (h : X = Y), (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainAlgHom_id : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], MonoidAlgebra.mapDomainAlgHom R A (MonoidHom.id M) = AlgHom.id R (MonoidAlgebra A M)
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.functorCategory_epimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.Limits.HasPushouts C],
  (CategoryTheory.MorphismProperty.epimorphisms C).functorCategory J =
    CategoryTheory.MorphismProperty.epimorphisms (CategoryTheory.Functor J C)
-- Mathlib.Algebra.Category.BoolRing
BoolRing.of.sizeOf_spec : ∀ (carrier : Type u) [booleanRing : BooleanRing carrier],
  sizeOf { carrier := carrier, booleanRing := booleanRing } = 1 + sizeOf carrier + sizeOf booleanRing
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sum_range_succ₀ : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ℕ), AEMeasurable (f i) μ) → ∀ (n : ℕ), ProbabilityTheory.IndepFun (∑ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.trans_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α ↪ β) (g : β ↪ γ) (h : γ ↪ δ),
  (f.trans g).trans h = f.trans (g.trans h)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForward_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X)
  {X_1 Y : CategoryTheory.Over f} (κ : X_1 ⟶ Y),
  f.iteratedSliceForward.map κ =
    CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left (CategoryTheory.Over.Hom.left κ)) ⋯
-- Lean.Meta.Sym.SymM
/-- Similar to `Meta.isDefEqI`, but the result is cache using pointer equality.  -/
Lean.Meta.Sym.isDefEqI : Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.RingTheory.Ideal.IdempotentFG
/-- A finitely generated idempotent ideal is generated by an idempotent element  -/
Ideal.isIdempotentElem_iff_of_fg : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.FG → (IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = R ∙ e)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.image_univ_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β] (f : β ≃ α),
  Finset.image (⇑f) Finset.univ = Finset.univ
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Auxiliary definition for `uliftYonedaAdjunction`.  -/
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        {A : CategoryTheory.Functor C ℰ} →
          [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] →
            (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ) →
              (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) →
                [L.IsLeftKanExtension α] →
                  (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) →
                    (E : ℰ) → (L.obj P ⟶ E) ≃ (P ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n, c - b = n • p
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.analyticAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  CPolynomialAt 𝕜 f x → AnalyticAt 𝕜 f x
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Whether to show timing information in "tryAtEachStep" tactic analysis output.

When true (default), messages include elapsed time like `(23ms)`.
Set to false in tests to avoid non-deterministic output.
 -/
linter.tacticAnalysis.tryAtEachStep.showTiming : Lean.Option Bool
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_le_size_insertMany : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type v} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.rightUnitor.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R),
  SemimoduleCat.MonoidalCategory.rightUnitor M = (TensorProduct.rid R ↑M).toModuleIsoₛ
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.LeAtTop.mk : ∀ {β : Type u_2} {L : SummationFilter β}, L.filter ≤ Filter.atTop → L.LeAtTop
-- Mathlib.Algebra.Group.Hom.Basic
nsmulAddMonoidHom_apply : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α), (nsmulAddMonoidHom n) x = n • x
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_η : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Center.forget C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Center.forget C).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Center C)))
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.not_mem_of_mem_ofFixingAddSubgroup : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α}
  (x : ↥(SubAddAction.ofFixingAddSubgroup M s)), ↑x ∉ s
-- Mathlib.Tactic.Translate.Reorder
/-- Return the minimum size of an array on which the permutation is valid.  -/
Mathlib.Tactic.Translate.Permutation.range : Mathlib.Tactic.Translate.Permutation → ℕ
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Given a subgroup `𝒢` of `GL n R`, this is the subgroup generated by `𝒢` and `-1`.  -/
Subgroup.adjoinNegOne : {n : Type u_1} →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] → {R : Type u_2} → [inst_2 : Ring R] → Subgroup (GL n R) → Subgroup (GL n R)
-- Mathlib.Topology.Algebra.Order.Field
tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : 𝕜 → α},
  Filter.Tendsto (fun x => f x⁻¹) Filter.atTop l → Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) l
-- Mathlib.ModelTheory.Fraisse
/-- The Fraïssé limit of a class is unique, in that any two Fraïssé limits are isomorphic.  -/
FirstOrder.Language.IsFraisseLimit.nonempty_equiv : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  {N : Type w} [inst_1 : L.Structure N] [inst_2 : Countable ((l : ℕ) × L.Functions l)] [inst_3 : Countable M]
  [inst_4 : Countable N],
  FirstOrder.Language.IsFraisseLimit K M → FirstOrder.Language.IsFraisseLimit K N → Nonempty (L.Equiv M N)
-- Lean.Meta.Sym.Arith.Types
/-- Non-commutative semirings.  -/
Lean.Meta.Sym.Arith.State.ncSemirings : Lean.Meta.Sym.Arith.State → Array Lean.Meta.Sym.Arith.Semiring
-- Aesop.Forward.State
Aesop.InstMap.map : Aesop.InstMap → Lean.PHashMap Aesop.SlotIndex (Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp))
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.congrLeft_apply : ∀ (M : Type u_5) {M₂ : Type u_7} {M₃ : Type u_8} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] {R : Type u_9} (S : Type u_10) [inst_3 : Semiring R] [inst_4 : Semiring S]
  [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : Module R M] [inst_8 : Module S M]
  [inst_9 : SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) (a : M₂ →ₗ[R] M),
  (LinearEquiv.congrLeft M S e) a = (e.arrowCongrAddEquiv (LinearEquiv.refl R M)).toFun a
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_add : ∀ {d : ℤ} (z w : ℤ√d), (z + w).im = z.im + w.im
-- Mathlib.Data.Finset.PImage
Finset.pimage_some : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → β)
  [inst_1 : (x : α) → Decidable (Part.some (f x)).Dom], Finset.pimage (fun x => Part.some (f x)) s = Finset.image f s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.size_toArray : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.toArray.size = r.size
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go.match_3.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (b fuel : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (b fuel : ℕ) → motive b fuel.succ),
  (match b, fuel.succ with
    | x, 0 => h_1 x
    | b, fuel.succ => h_2 b fuel) =
    h_2 b fuel
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Server.mk.injEq : ∀ (shared shared_1 : Std.Http.Internal.Mock.SharedState✝),
  ({ shared := shared } = { shared := shared_1 }) = (shared = shared_1)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- The inverse of an integral element in a division ring over a field is also integral.  -/
IsIntegral.inv : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → IsIntegral R x⁻¹
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interFst_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (x : (E.inter F).I₀),
  (E.interFst F).h₀ x =
    CategoryTheory.Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).snd)
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The canonical bijection `SmallHom.{w} W X Y ≃ (L.obj X ⟶ L.obj Y)`
when `L` is a localization functor for `W : MorphismProperty C` and
that `HasSmallLocalizedHom.{w} W X Y` holds.  -/
CategoryTheory.Localization.SmallHom.equiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (L : CategoryTheory.Functor C D) →
            [L.IsLocalization W] →
              {X Y : C} →
                [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
                  CategoryTheory.Localization.SmallHom W X Y ≃ (L.obj X ⟶ L.obj Y)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofQuotient_var : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) (g : relations.G),
  (Module.Relations.Solution.ofQuotient relations).var g = relations.toQuotient fun₀ | g => 1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t₁ t₂ : Set β}, s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCocone_ι_app_mk : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  B.toCocone.ι.app { as := j } = B.ι j
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroIsoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero],
  P.isoClosure.ContainsZero
-- Mathlib.Geometry.Convex.Cone.Dual
/-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map `p x`.  -/
PointedCone.dual_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (x : M), PointedCone.dual p {x} = PointedCone.comap (p x) (PointedCone.positive R R)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₃_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1),
  (X.sc₃ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.toOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), ⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
  (s : Set α),
  MeasurableSet s → MeasureTheory.VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure
-- Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
SymmetricAlgebra.comul_ι : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  CoalgebraStruct.comul ((SymmetricAlgebra.ι R M) x) =
    (SymmetricAlgebra.ι R M) x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (SymmetricAlgebra.ι R M) x
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_orderMonoidWithZeroHom_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β) (a : α), ↑f a = f a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.inv f) z) h) =
    h
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instAddCommMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddCommMonoid N],
  ZeroHom.instAddCommMonoid = { toAddMonoid := ZeroHom.instAddMonoid, add_comm := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- If `x` lies within an orthogonal family `v`, it can be expressed as a sum of projections.  -/
OrthogonalFamily.sum_projection_of_mem_iSup : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] {V : ι → Submodule 𝕜 E} [inst_4 : ∀ (i : ι), CompleteSpace ↥(V i)],
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ x ∈ iSup V, ∑ i, (V i).starProjection x = x
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_factorsThrough : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m),
  ((DirichletCharacter.changeLevel hm) χ).FactorsThrough n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.differentiableOn_derivWeierstrassP : ∀ (L : PeriodPair), DifferentiableOn ℂ L.derivWeierstrassP (↑L.lattice)ᶜ
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.mk.inj : ∀ {elimInfo : Lean.Elab.Term.ElabElimInfo} {expectedType : Lean.Expr} {elimInfo_1 : Lean.Elab.Term.ElabElimInfo}
  {expectedType_1 : Lean.Expr},
  { elimInfo := elimInfo, expectedType := expectedType } = { elimInfo := elimInfo_1, expectedType := expectedType_1 } →
    elimInfo = elimInfo_1 ∧ expectedType = expectedType_1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_smul_right : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : Zero R]
  [inst_6 : SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ'} (hs : s.IsPWO),
  ((HahnModule.of R).symm y).support ⊆ s →
    ((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.Topology.MetricSpace.Pseudo.Basic
/-- If a map is continuous on a separable set `s`, then the image of `s` is also separable.  -/
ContinuousOn.isSeparable_image : ∀ {β : Type v} {α : Type u_2} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
  [inst_2 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (f '' s)
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_xor : ∀ (a b : UInt8), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.MeasureTheory.Function.EssSup
essSup_uniformOn_eq_ciSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α]
  [MeasurableSingletonClass α] [Finite α],
  BddAbove (Set.range f) → essSup f (ProbabilityTheory.uniformOn Set.univ) = ⨆ a, f a
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_of_eq_det_one_mul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A B : Matrix n n R}
  (C : Matrix n n R), C.det = 1 → A = C * B → A.det = B.det
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.zsmul` -/
Function.HasFiniteSupport.fun_zsmul : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (n : ℤ), Function.HasFiniteSupport fun i => n • f i
-- Mathlib.Algebra.FiniteSupport.Defs
Function.hasFiniteMulSupport_one : ∀ {α : Type u_1} {M : Type u_2} [inst : One M], Function.HasFiniteMulSupport fun x => 1
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D.eq_1 : ∀ (n : ℕ),
  CartanMatrix.D n =
    Matrix.of fun i j =>
      if i = j then 2
      else
        if n ≤ 2 then 0
        else
          if ↑i + 1 = ↑j ∧ ↑j + 2 < n then -1
          else
            if ↑j + 1 = ↑i ∧ ↑i + 2 < n then -1
            else
              if ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n) then -1
              else if ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n) then -1 else 0
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentDataAsCoalgebra f) (i : ι),
  (CategoryTheory.CategoryStruct.id D).hom i = CategoryTheory.CategoryStruct.id (D.obj i)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_erase_top : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (s : Finset α),
  (s.erase ⊤).inf id = s.inf id
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_iff_ne_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t.min?.isSome = true ↔ t ≠ ∅
-- Mathlib.Analysis.Normed.Group.Int
NNReal.natCast_natAbs : ∀ (n : ℤ), ↑n.natAbs = ‖n‖₊
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.coeff_map_eq_comp : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
  (Polynomial.map f p).coeff = ⇑f ∘ p.coeff
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.checkAux.check : Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Unit Lean.MetaM Unit
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.associator_hom_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₁₂ : Type u_4} {C₂₃ : Type u_5} {D₁ : Type u_6} {D₂ : Type u_7}
  {D₃ : Type u_8} {D₁₂ : Type u_9} {D₂₃ : Type u_10} {C : Type u_11} {D : Type u_12}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃]
  [inst_6 : CategoryTheory.Category.{v_7, u_4} C₁₂] [inst_7 : CategoryTheory.Category.{v_8, u_5} C₂₃]
  [inst_8 : CategoryTheory.Category.{v_9, u_9} D₁₂] [inst_9 : CategoryTheory.Category.{v_10, u_10} D₂₃]
  [inst_10 : CategoryTheory.Category.{v_11, u_11} C] [inst_11 : CategoryTheory.Category.{v_12, u_12} D]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) (L₃ : CategoryTheory.Functor C₃ D₃)
  (L₁₂ : CategoryTheory.Functor C₁₂ D₁₂) (L₂₃ : CategoryTheory.Functor C₂₃ D₂₃) (L : CategoryTheory.Functor C D)
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂)
  (W₃ : CategoryTheory.MorphismProperty C₃) (W₁₂ : CategoryTheory.MorphismProperty C₁₂)
  (W₂₃ : CategoryTheory.MorphismProperty C₂₃) [inst_12 : W₁.ContainsIdentities] [inst_13 : W₂.ContainsIdentities]
  [inst_14 : W₃.ContainsIdentities] [inst_15 : L₁.IsLocalization W₁] [inst_16 : L₂.IsLocalization W₂]
  [inst_17 : L₃.IsLocalization W₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (iso : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃)
  (F₁₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ D₁₂))
  (G' : CategoryTheory.Functor D₁₂ (CategoryTheory.Functor D₃ D))
  (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂₃ D))
  (G₂₃' : CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ D₂₃)) [inst_18 : ⋯], ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp (t.minKey ⋯) k).isLE = true