mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_hom_toFunctor_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C × D} (f : X ⟶ Y),
  (CategoryTheory.curryingIso.hom.toFunctor.obj F).map f =
    CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffOn_localFrameCoeff`.

---

If `s` is `C^k` on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
contMDiffOn_localFrame_coeff : ∀ {𝕜 : 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 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  {k : WithTop ℕ∞} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  IsOpen t →
    t ⊆ e.baseSet →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) t →
        ∀ (i : ι),
          ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k
            ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) t
-- Lean.Meta.AppBuilder
/-- Returns `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type.  -/
Lean.Meta.mkMul : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_3 : HSub Std.Time.DateTime Std.Time.Minute.Offset Std.Time.DateTime
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform satisfies `∫ 𝓕 f * conj g = ∫ f * conj (𝓕⁻¹ g)`, which together
with the Fourier inversion theorem yields Plancherel's theorem. The stated version is more
convenient since it does only require integrability of `f` and `g`.

Version where the multiplication is replaced by a general bilinear form `M`.  -/
VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  {F : Type u_5} {G : Type u_6} [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℂ F] [inst_10 : NormedAddCommGroup G]
  [inst_11 : NormedSpace ℂ G] [inst_12 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [inst_14 : TopologicalSpace V]
  [BorelSpace V] [inst_16 : TopologicalSpace W] [inst_17 : MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [SecondCountableTopologyEither W V] [CompleteSpace E] [CompleteSpace F] {f : V → E}
  {g : W → F} (M : E →L⋆[ℂ] F →L[ℂ] G),
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      MeasureTheory.Integrable f μ →
        MeasureTheory.Integrable g ν →
          ∫ (ξ : W), (M (VectorFourier.fourierIntegral e μ L f ξ)) (g ξ) ∂ν =
            ∫ (x : V), (M (f x)) (VectorFourier.fourierIntegral e ν (-L.flip) g x) ∂μ
-- Mathlib.Algebra.Lie.Submodule
/-- The zero module is a Lie submodule of any Lie module.  -/
LieSubmodule.instZero : {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] → Zero (LieSubmodule R L M)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.mk.injEq : ∀ (val : Lean.Expr) (synthOrder : Array ℕ) (val_1 : Lean.Expr) (synthOrder_1 : Array ℕ),
  ({ val := val, synthOrder := synthOrder } = { val := val_1, synthOrder := synthOrder_1 }) =
    (val = val_1 ∧ synthOrder = synthOrder_1)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.equivIsoColimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (i : r ≅ t),
  CategoryTheory.Limits.IsColimit.equivIsoColimit i =
    { toFun := fun h => h.ofIsoColimit i, invFun := fun h => h.ofIsoColimit i.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.step.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (motive : Turing.TM1.Cfg Γ Λ σ → Sort u_4) (var : σ)
  (Tape : Turing.Tape Γ) (h_1 : (var : σ) → (Tape : Turing.Tape Γ) → motive { l := none, var := var, Tape := Tape })
  (h_2 : (l : Λ) → (v : σ) → (T : Turing.Tape Γ) → motive { l := some l, var := v, Tape := T }),
  (match { l := none, var := var, Tape := Tape } with
    | { l := none, var := var, Tape := Tape } => h_1 var Tape
    | { l := some l, var := v, Tape := T } => h_2 l v T) =
    h_1 var Tape
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableSplitInfo : Hashable Lean.Meta.Grind.SplitInfo
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.exists_unsortedEigenvalues_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {μ : 𝕜},
  Module.End.HasEigenvalue T μ → ∃ i, ↑(LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i) = μ
-- Mathlib.Order.Atoms
isCoatomic_iff_forall_isCoatomic_Ici : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α], IsCoatomic α ↔ ∀ (x : α), IsCoatomic ↑(Set.Ici x)
-- Mathlib.Analysis.Convex.Between
wbtw_smul_vadd_smul_vadd_of_nonneg_of_le : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  0 ≤ r₁ → r₁ ≤ r₂ → Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_pow_primes : ∀ {p q : ℕ} (n m : ℕ), Nat.Prime p → Nat.Prime q → p ≠ q → (p ^ n).Coprime (q ^ m)
-- Mathlib.Order.Basic
Pi.lt_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i},
  x < y ↔ x ≤ y ∧ ∃ i, x i < y i
-- Mathlib.Data.Set.MemPartition
memPartition_zero : ∀ {α : Type u_1} (f : ℕ → Set α), memPartition f 0 = {Set.univ}
-- Aesop.Rule
Aesop.RegularRule.safe.sizeOf_spec : ∀ (r : Aesop.SafeRule), sizeOf (Aesop.RegularRule.safe r) = 1 + sizeOf r
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.complete : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  CompleteOrthogonalIdempotents e → ∑ i, e i = 1
-- Mathlib.Data.Set.Image
Set.rangeSplitting_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → StrictMono (Set.rangeSplitting f)
-- Mathlib.Order.Filter.Map
Filter.singleton_mem_pure : ∀ {α : Type u_1} {a : α}, {a} ∈ pure a
-- Mathlib.Order.BoundedOrder.Basic
Pi.instBotForall : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → Bot (α' i)] → Bot ((i : ι) → α' i)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The automorphism group of a root pairing.  -/
RootPairing.Aut : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → RootPairing ι R M N → Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.instEpiGCokernelSequence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelSequence f).g
-- Mathlib.Order.Birkhoff
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice.  -/
LatticeHom.birkhoffSet : {α : Type u_1} →
  [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → LatticeHom α (Set { a // SupIrred a })
-- Mathlib.Order.Minimal
/-- **Alias** of `Set.exists_sdiff_singleton_of_not_minimal`. -/
Set.exists_diff_singleton_of_not_minimal : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) → P s → ¬Minimal P s → ∃ x ∈ s, P (s \ {x})
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.sparseCasesOnCacheExt : Lean.EnvExtension (Lean.PHashMap Lean.Meta.SparseCasesOnKey✝ Lean.Name)
-- Mathlib.Topology.Algebra.Constructions
AddUnits.continuous_coe_neg : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Continuous fun u => ↑(-u)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Auxiliary definition for `HomologicalComplex₂.flipEquivalence`.  -/
HomologicalComplex₂.flipEquivalenceCounitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              (HomologicalComplex₂.flipFunctor C c₂ c₁).comp (HomologicalComplex₂.flipFunctor C c₁ c₂) ≅
                CategoryTheory.Functor.id (HomologicalComplex₂ C c₂ c₁)
-- Lean.CompactedRegion
/-- Frees a compacted region and its contents. No live references to the contents may exist at the
time of invocation.
 -/
Lean.CompactedRegion.free : Lean.CompactedRegion → IO Unit
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_ulift : ∀ (α : Type u_3), ENat.card (ULift.{u_4, u_3} α) = ENat.card α
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMap.eq_1 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X Y : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMap f X Y =
    Quotient.lift (CategoryTheory.FreeMonoidalCategory.projectMapAux f) ⋯
-- Mathlib.CategoryTheory.Filtered.Small
/-- The full subcategory induced by the cofiltered closure of a family is cofiltered.  -/
CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C), CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.Quasicategory.from_innerFibrations : ∀ (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X), SSet.innerFibrations (t.from S)
-- Mathlib.Order.Heyting.Hom
BiheytingHom.toFun_eq_coe_aux : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] {f : BiheytingHom α β},
  ⇑f.toLatticeHom = ⇑f
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.pair_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (X Y Z : C),
  CategoryTheory.ObjectProperty.pair X Y Z ↔ X = Z ∨ Y = Z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.powerBasisAux.eq_1 : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (hx : IsIntegral K x),
  IntermediateField.powerBasisAux hx =
    ((AdjoinRoot.powerBasis ⋯).basis.map ↑(IntermediateField.adjoinRootEquivAdjoin K hx)).reindex (finCongr ⋯)
-- Mathlib.Order.Heyting.Basic
lt_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α} [Nontrivial α], a < aᶜ ↔ a = ⊥
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The sum of `f` over `insert a s` is the same as
the sum over `s`, as long as `f a = 0`.  -/
Finset.sum_insert_zero : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  f a = 0 → ∑ x ∈ insert a s, f x = ∑ x ∈ s, f x
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.inr_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr P.i = P.i₁
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentItem),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)
-- Mathlib.RingTheory.RingHomProperties
/-- The categorical `MorphismProperty` associated to a property of ring homs expressed
non-categorical terms.  -/
RingHom.toMorphismProperty : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  CategoryTheory.MorphismProperty CommRingCat
-- Mathlib.Algebra.Order.Floor.Defs
Nat.gc_ceil_coe : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorSemiring α],
  GaloisConnection Nat.ceil Nat.cast
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
/-- The projective dimension of an object in an abelian category.  -/
CategoryTheory.projectiveDimension : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → WithBot ℕ∞
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.mod.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive 0 x)
  (h_2 : (n n_1 : ℕ) → n = n_1.succ → (m : ℕ) → motive n_1.succ m),
  (match 0, x with
    | 0, x => h_1 x
    | n@h:n_1.succ, m => h_2 n n_1 h m) =
    h_1 x
-- Mathlib.Data.Sym.Sym2
_private.Mathlib.Data.Sym.Sym2.0.Sym2.perm_card_two_iff : ∀ {α : Type u_1} {a₁ b₁ a₂ b₂ : α}, [a₁, b₁].Perm [a₂, b₂] ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
-- Mathlib.Order.KrullDimension
Order.bot_lt_krullDim_iff : ∀ {α : Type u_1} [inst : Preorder α], ⊥ < Order.krullDim α ↔ Nonempty α
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv
      (CategoryTheory.Limits.pullback.snd 0 0) =
    CategoryTheory.Limits.prod.snd
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isOrdinal_succ : ∀ {x : ZFSet.{u_1}}, x.IsOrdinal → (insert x x).IsOrdinal
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_inv_eq_iff_eq_mul : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit b → (a * b⁻¹ = c ↔ a = c * b)
-- Mathlib.Order.Filter.Prod
Filter.prod_mem_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot],
  s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g
-- Lean.Meta.ExprLens
_private.Lean.Meta.ExprLens.0.Lean.Core.viewBindersCoord : ℕ → Lean.Expr → Option (Lean.Name × Lean.Expr)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) →
    (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range =
      (Rep.Hom.hom (Rep.leftRegular k G).norm).ker
-- Mathlib.Topology.Specialization
Specialization.toEquiv_inj : ∀ {α : Type u_1} {a b : α}, Specialization.toEquiv a = Specialization.toEquiv b ↔ a = b
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.uniq : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self : D.IsTerminal e) {j : J}
  (hj : D.P j) {φ : j ⟶ e}, D.W φ → self.lift hj = φ
-- Mathlib.Analysis.Complex.Basic
Complex.conjLIE_toCLE : ↑Complex.conjLIE = Complex.conjCLE
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.MonadSatisfying.instEStateM.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 :
    (a : α) → (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.ok a s'_1 → motive (EStateM.Result.ok a s'_1))
  (h_2 :
    (e_1 : ε) →
      (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.error e_1 s'_1 → motive (EStateM.Result.error e_1 s'_1)),
  (match w : EStateM.Result.error e s' with
    | EStateM.Result.ok a s'_1 => h_1 a s'_1 w
    | EStateM.Result.error e_1 s'_1 => h_2 e_1 s'_1 w) =
    h_2 e s' ⋯
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- Isometry from an inner product space `E` to the direct sum of the eigenspaces of some
self-adjoint operator `T` on `E`.  -/
LinearMap.IsSymmetric.diagonalization : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} →
            [inst_3 : FiniteDimensional 𝕜 E] →
              T.IsSymmetric → E ≃ₗᵢ[𝕜] PiLp 2 fun μ => ↥(Module.End.eigenspace T (↑T 1 μ))
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_sum_self : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) (c : ι → R), ⇑(b.repr (∑ i, c i • b i)) = c
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank_snd : ∀ {X S T : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.IsAffine S]
  [inst_1 : AlgebraicGeometry.IsAffine T] (g : T ⟶ S) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f]
  (x : ↥T),
  AlgebraicGeometry.IsAffine.finrank✝ (CategoryTheory.Limits.pullback.snd f g) x =
    AlgebraicGeometry.IsAffine.finrank✝ f (g x)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instPartialOrder : {Ω : Type u_1} →
  {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → PartialOrder (MeasureTheory.Filtration ι m)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.equivQuotMaximalIdealPow.eq_1 : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (n : ℕ),
  IsLocalization.AtPrime.equivQuotMaximalIdealPow p Rₚ n =
    AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ (p ^ n) (Algebra.ofId R (Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n)) ⋯)
      (Ideal.Quotient.liftₐ (IsLocalRing.maximalIdeal Rₚ ^ n) (IsLocalization.liftAlgHom ⋯) ⋯) ⋯ ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If `2` is invertible in the coefficient ring,
a quadratic map is nondegenerate
iff its associated bilinear map is nondegenerate.  -/
QuadraticMap.nondegenerate_associated_iff : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} [inst_5 : Invertible 2],
  LinearMap.Nondegenerate (QuadraticMap.associated Q) ↔ QuadraticMap.Nondegenerate
-- Lean.Expr
Lean.Int.mkInstPowNat : Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial_eq_rename_comp : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (i : σ),
  Polynomial.toMvPolynomial i = (MvPolynomial.rename fun x => i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).mor₃ = X.δ'.app j
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraEquivUnder_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `f` and `f'` are two isomorphic morphisms and `f` is a transfinite composition
of morphisms in `W : MorphismProperty C`, then so is `f'`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    W.TransfiniteCompositionOfShape J f →
                      {X' Y' : C} →
                        {f' : X' ⟶ Y'} →
                          (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') →
                            W.TransfiniteCompositionOfShape J f'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_Spec_inv : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec R).isoSpec.inv = AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.addEquivProdDirectSum_symm_apply_toFun : ∀ {ι : Type v} {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)]
  (f : (fun i => α i) none × Π₀ (i : ι), (fun i => α i) (some i)) (i : Option ι),
  (DirectSum.addEquivProdDirectSum.symm f) i =
    match i with
    | none => f.1
    | some val => f.2 val
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardClusterStateStats : Inhabited Aesop.ForwardClusterStateStats
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_of_not_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β}
  {g : C(↑s, β)}, ¬ContinuousOn f s → ContinuousMap.mkD (s.domRestrict f) g = g
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.mulOp_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : Mᵐᵒᵖ →ₙ+ Nᵐᵒᵖ) (a : M),
  (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
-- Init.Data.SInt.Lemmas
Int32.div_zero : ∀ {a : Int32}, a / 0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_of_mem_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      l.contains k = false → k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) → k ∈ t
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.exists_eval_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, f.Splits → f.degree ≠ 0 → ∃ a, Polynomial.eval a f = 0