mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Basic
/-- If `K` and `L` are disjoint compact sets in an R₁ topological space
and `L` is also closed, then `K` and `L` have disjoint neighborhoods.  -/
SeparatedNhds.of_isCompact_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K L : Set X},
  IsCompact K → IsCompact L → IsClosed L → Disjoint K L → SeparatedNhds K L
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α} {k : α},
  l.contains k = false → (Std.HashMap.unitOfList l).getKey! k = default
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Module.End.injective_of_surjective` is the more general version for finite free `A`-modules
not necessarily of the form `Fin n → A`, but this version requires less imports.  -/
Module.End.injective_of_surjective_fin : ∀ {A : Type u_3} [inst : Semiring A] [IsStablyFiniteRing A] {n : ℕ} {f : Module.End A (Fin n → A)},
  Function.Surjective ⇑f → Function.Injective ⇑f
-- Mathlib.GroupTheory.Coset.Basic
mem_leftAddCoset_iff : ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ a +ᵥ s ↔ -a + x ∈ s
-- Lean.Elab.Quotation.Precheck
_private.Lean.Elab.Quotation.Precheck.0.Lean.Elab.Term.Quotation.precheck.hasQuotedIdent : Lean.Syntax → Bool
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_3} (motive : (x : Option α) → ((a : α) → x = some a → β) → Sort u_2)
  (x : (a : α) → none = some a → β) (h_1 : (x : (a : α) → none = some a → β) → motive none x)
  (h_2 : (a : α) → (f : (a_1 : α) → some a = some a_1 → β) → motive (some a) f),
  (match none, x with
    | none, x => h_1 x
    | some a, f => h_2 a f) =
    h_1 x
-- Mathlib.Analysis.Convex.AmpleSet
/-- A set is ample iff its pre-image under a continuous affine equivalence is.  -/
AmpleSet.preimage_iff : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] {E : Type u_2}
  [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E] [inst_5 : TopologicalSpace E] {s : Set F} (L : E ≃ᴬ[ℝ] F),
  AmpleSet (⇑L ⁻¹' s) ↔ AmpleSet s
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**: a semisimple ring is isomorphic to a
product of matrix rings over the opposite of the endomorphism rings of its simple modules.  -/
IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite : ∀ (R : Type u) [inst : Ring R] [IsSemisimpleRing R],
  ∃ n D d,
    (∀ (i : Fin n), IsSimpleModule R ↥(D i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(D i))ᵐᵒᵖ))
-- Mathlib.Data.Finsupp.Order
Finsupp.instSMulPosReflectLE : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Zero β] [inst_2 : Preorder β]
  [inst_3 : SMulZeroClass α β] [SMulPosReflectLE α β], SMulPosReflectLE α (ι →₀ β)
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq_k_eq_toSeq : ∀ (e : Lean.Grind.AC.Expr), e.toSeq_k = e.toSeq
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.hom_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C}, Function.Injective CategoryTheory.Mon.Hom.hom
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousAt_extend : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M}, x ∈ f.source → ContinuousAt (↑(f.extend I)) x
-- Mathlib.Data.Real.ConjExponents
/-- **Alias** of the reverse direction of `NNReal.holderConjugate_coe_iff`. -/
NNReal.HolderConjugate.coe : ∀ {p q : NNReal}, p.HolderConjugate q → (↑p).HolderConjugate ↑q
-- Mathlib.Data.EReal.Operations
EReal.left_distrib_of_nonneg_of_ne_top : ∀ {x : EReal}, 0 ≤ x → x ≠ ⊤ → ∀ (y z : EReal), x * (y + z) = x * y + x * z
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filterMap_eq_false : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).isEmpty = false ↔
      ∃ k, ∃ (h : Std.Internal.List.containsKey k l = true), (f k (Std.Internal.List.getValueCast k l h)).isSome = true)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_two_pi_sub_pi : ∀ (n : ℕ), Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1
-- Mathlib.SetTheory.Cardinal.Basic
/-- The type of cardinals in universe `u` is not `Small.{u}`. This is a version of the Burali-Forti
paradox.  -/
not_small_cardinal : ¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Initial.right_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Algebra F} (h : CategoryTheory.Limits.IsInitial A),
  CategoryTheory.CategoryStruct.comp A.str (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) =
    CategoryTheory.CategoryStruct.id (F.obj A.a)
-- Mathlib.GroupTheory.GroupAction.Defs
instSMulCommClassSubtypeMemSubmonoidSubmonoid : ∀ (M : Type u) (α : Type v) [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction M α],
  SMulCommClass M (↥(FixedPoints.submonoid M α)) α
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isUniformInducing_closure : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformInducing TopologicalSpace.Closeds.closure
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.laplacian_eq_fourierMultiplierCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] [CompleteSpace F] (f : SchwartzMap E F),
  Laplacian.laplacian f = -(2 * Real.pi) ^ 2 • (SchwartzMap.fourierMultiplierCLM F fun x => ‖x‖ ^ 2) f
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCircuit.contract_dep_of_not_subset : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, M.IsCircuit K → ∀ {C : Set α}, ¬K ⊆ C → (M.contract C).Dep (K \ C)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.hasColimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T}
  [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.PreservesColimitsOfShape J G],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CostructuredArrow G X)
-- Init.Data.List.MapIdx
List.mapFinIdx_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : (i : ℕ) → α → i < l.length → β}
  {g : (i : ℕ) → β → i < (l.mapFinIdx f).length → γ},
  (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun i a h => g i (f i a h) ⋯
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- If `α` is a 2-morphism between left adjoints whose conjugate 2-morphism
is an isomorphism, then `α` is an isomorphism. The converse is given in `conjugateEquiv_iso`.
 -/
CategoryTheory.Bicategory.conjugateEquiv_of_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ⟶ l₁)
  [CategoryTheory.IsIso ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α)], CategoryTheory.IsIso α
-- Mathlib.Data.Sum.Basic
Sum.update_elim_inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : α} {x : γ}, Function.update (Sum.elim f g) (Sum.inl i) x = Sum.elim (Function.update f i x) g
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsSeparated
-- Mathlib.LinearAlgebra.Matrix.Rank
Fintype.equivFinOfCardEq.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] {n : ℕ} (h : Fintype.card α = n),
  Fintype.equivFinOfCardEq h = Fintype.equivFinOfCardEq h
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- A specialized version of `UniformOnFun.uniformContinuous_ofFun_toFun` for convenience.  -/
UniformOnFun.uniformContinuous_ofFun_toFun_of_mem : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  ∀ s ∈ 𝔖, UniformContinuous (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑(UniformOnFun.toFun {s}))
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Basis sets for the uniformity of uniform convergence: `gen α β V` is the set of pairs `(f, g)`
of functions `α →ᵤ β` such that `∀ x, (f x, g x) ∈ V`.  -/
UniformFun.gen : (α : Type u_1) → (β : Type u_2) → Set (β × β) → Set (UniformFun α β × UniformFun α β)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.add : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B₁ B₂ : LinearMap.BilinForm R M}, B₁.IsSymm → B₂.IsSymm → (B₁ + B₂).IsSymm
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Creates a `SimpTheorem` from a global theorem.
Because some theorems lead to multiple `SimpTheorems` (in particular conjunctions), returns an array.
 -/
Lean.Meta.mkSimpTheoremFromConst : Lean.Name →
  optParam Bool true →
    optParam Bool false → optParam ℕ 1000 → optParam Bool false → Lean.MetaM (Array Lean.Meta.SimpTheorem)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (z : X ⟶ c.pt) [inst_3 : CategoryTheory.Mono c.ι] {j j' : J} (f : j ⟶ j'),
  (CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F z).map f =
    CategoryTheory.MonoOver.homMk ((CategoryTheory.Limits.pullback c.ι ((CategoryTheory.Functor.const J).map z)).map f)
      ⋯
-- Mathlib.Data.Setoid.Basic
Setoid.ext_iff : ∀ {α : Sort u_3} {s t : Setoid α}, s = t ↔ ∀ (a b : α), s a b ↔ t a b
-- Mathlib.Order.Disjoint
Disjoint.inf_right' : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α), Disjoint a b → Disjoint a (c ⊓ b)
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is an exact sequence, this is the isomorphism from the cokernel
of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`.  -/
CategoryTheory.ComposableArrows.Exact.cokerIsoKer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        {n : ℕ} →
          {S : CategoryTheory.ComposableArrows C (n + 3)} →
            S.Exact →
              (k : ℕ) →
                (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.cokerIsoKer._auto_1) →
                  [inst_3 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)] →
                    [inst_4 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)] →
                      CategoryTheory.Limits.cokernel (S.map' k (k + 1) ⋯ ⋯) ≅
                        CategoryTheory.Limits.kernel (S.map' (k + 2) (k + 3) ⋯ ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq :
    CochainComplex.HomComplex.δ 0 1 β +
        (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) CochainComplex.mappingCone.lift._proof_1 =
      0),
  CochainComplex.mappingCone.lift φ α β eq =
    (CochainComplex.mappingCone.liftCocycle φ α β CochainComplex.mappingCone.lift._proof_2 eq).homOf
-- Mathlib.Analysis.InnerProductSpace.l2Space
Orthonormal.linearIsometryEquiv_symm_apply_single_one : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E} (hv : Orthonormal 𝕜 v)
  [inst_4 : DecidableEq ι] (h : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure) (i : ι),
  ⋯.linearIsometryEquiv.symm (lp.single 2 i 1) = v i
-- Init.System.IO
/-- Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is
encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from
the handle may block and/or return data.
 -/
IO.FS.Handle.readBinToEnd : IO.FS.Handle → IO ByteArray
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_3 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (Std.DHashMap.Raw.ofList l).get! k' = cast ⋯ v
-- Init.Data.List.Find
List.IsPrefix.findIdx_eq_of_findIdx_lt_length : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <+: l₂ → List.findIdx p l₁ < l₁.length → List.findIdx p l₂ = List.findIdx p l₁
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_cancelVar : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon)
  (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Mon.denote ctx m =
    Lean.Grind.CommRing.Var.denote ctx x ^ m.degreeOf x * Lean.Grind.CommRing.Mon.denote ctx (m.cancelVar x)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.Hom.s₀`. -/
AlgebraicGeometry.Scheme.Cover.Hom.idx : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} → {F : CategoryTheory.PreZeroHypercover S} → E.Hom F → E.I₀ → F.I₀
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of normed groups, using the sup norm.  -/
Pi.normedCommGroup : {ι : Type u_1} → {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedCommGroup (G i)] → NormedCommGroup ((i : ι) → G i)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_zero : ∀ {x : NNReal} {y : ℝ}, y ≠ 0 → (x ^ y = 0 ↔ x = 0)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.domLCongr_single : ∀ {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α₁ : Type u_9}
  {α₂ : Type u_10} (e : α₁ ≃ α₂) (i : α₁) (m : M), ((Finsupp.domLCongr e) fun₀ | i => m) = fun₀ | e i => m
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedString` from a `ByteArray`, panicking if the byte array is invalid.
 -/
Std.Http.URI.EncodedString.ofByteArray! : {r : UInt8 → Bool} → ByteArray → Std.Http.URI.EncodedString r
-- Mathlib.Analysis.Normed.Order.Lattice
norm_le_norm_of_abs_le_abs : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] {a b : α}, |a| ≤ |b| → ‖a‖ ≤ ‖b‖
-- Mathlib.Control.Monad.Writer
WriterT.run_bind : ∀ {M : Type u → Type v} {α β ω : Type u} [inst : Monad M] (empty : ω) (append : ω → ω → ω) (cmd : WriterT ω M α)
  (f : α → WriterT ω M β),
  (cmd >>= f).run = do
    let x ← cmd.run
    match x with
      | (a, w₁) =>
        (fun x =>
            match x with
            | (b, w₂) => (b, append w₁ w₂)) <$>
          (f a).run
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesColimit : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor K J), (CategoryTheory.ObjectProperty.preservesColimit F).IsClosedUnderIsomorphisms
-- Init.Data.RArray
Lean.RArray.brecOn.eq : ∀ {α : Type u} {motive : Lean.RArray α → Sort u_1} (t : Lean.RArray α)
  (F_1 : (t : Lean.RArray α) → Lean.RArray.below t → motive t),
  Lean.RArray.brecOn t F_1 = F_1 t (Lean.RArray.brecOn.go t F_1).2
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instAddSubmonoidClass : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], AddSubmonoidClass (ClosedSubmodule R M) M
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (μ.withDensity f = 0 ↔ f =ᵐ[μ] 0)
-- Lean.Data.NameTrie
_private.Lean.Data.NameTrie.0.Lean.toKey : Lean.Name → List Lean.NamePart
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiSeparated (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_apply_of_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (ha : p a),
  (Equiv.Perm.ofSubtype f) a = ↑(f ⟨a, ha⟩)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_sUnion : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set (Set R)),
  NonUnitalSubsemiring.closure (⋃₀ s) = ⨆ t ∈ s, NonUnitalSubsemiring.closure t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → (m₁.inter m₂ ⋯).size ≤ m₂.size
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ↑e.symm = (↑e).symm
-- Mathlib.Topology.Order.Basic
exists_Icc_mem_subset_of_mem_nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhdsWithin a (Set.Ici a) → ∃ b, a ≤ b ∧ Set.Icc a b ∈ nhdsWithin a (Set.Ici a) ∧ Set.Icc a b ⊆ s
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.mk.sizeOf_spec : ∀ (module? : Option Lean.DeclarationLocation), sizeOf { module? := module? } = 1 + sizeOf module?
-- Lean.Server.References
/-- Yields all references in `self` for `ident`, as well as the `DocumentUri` that each
reference occurs in.
 -/
Lean.Server.References.allRefsFor : Lean.Server.References →
  Lean.Lsp.RefIdent → Array (Lean.Lsp.DocumentUri × Lean.Name × Lean.Lsp.RefInfo × Lean.Lsp.Decls)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides one amongst `S'.a + S'.b`,
`S'.a + η * S'.b` and `S'.a + η ^ 2 * S'.b`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ 2 ∣ FermatLastTheoremForThreeGen.Solution'.a✝ S' + FermatLastTheoremForThreeGen.Solution'.b✝ S' ∨
    (hζ.toInteger - 1) ^ 2 ∣
        FermatLastTheoremForThreeGen.Solution'.a✝ S' + ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ S' ∨
      (hζ.toInteger - 1) ^ 2 ∣
        FermatLastTheoremForThreeGen.Solution'.a✝ S' + ↑⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution'.b✝ S'
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Ici : ∀ (x : ℝ), Real.toEReal '' Set.Ici x = Set.Ico ↑x ⊤
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (self.s (n + 1)) (X.left.δ i.succ) =
    CategoryTheory.CategoryStruct.comp (X.left.δ i) (self.s n)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posSemidef_transpose_iff : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  {M : Matrix n n R'}, M.transpose.PosSemidef ↔ M.PosSemidef
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_left_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The natural transformation
`F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory` induced by
a natural transformation `F ⟶ G` between additive functors.  -/
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {F G : CategoryTheory.Functor C D} →
                [inst_5 : F.Additive] →
                  [inst_6 : G.Additive] →
                    (F ⟶ G) → (F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} (e : G ≅ H) [inst_3 : CategoryTheory.GrpObj G]
  [inst_4 : CategoryTheory.IsCommMonObj G] [inst_5 : CategoryTheory.GrpObj H] [inst_6 : CategoryTheory.IsCommMonObj H]
  [inst_7 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.CommGrp.mkIso' e).hom.hom.hom.hom = e.hom
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_iSup : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid M),
  AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.elabDo : Lean.Elab.Term.TermElab
-- Std.Data.HashMap.Lemmas
Std.HashMap.union_insert_right_equiv_insert_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α × β}, (m₁ ∪ m₂.insert p.1 p.2).Equiv ((m₁ ∪ m₂).insert p.1 p.2)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {sq₁ sq₂ : CategoryTheory.Square C} →
      (τ₁ : sq₁.X₁ ⟶ sq₂.X₁) →
        (τ₂ : sq₁.X₂ ⟶ sq₂.X₂) →
          (τ₃ : sq₁.X₃ ⟶ sq₂.X₃) →
            (τ₄ : sq₁.X₄ ⟶ sq₂.X₄) →
              autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
                  CategoryTheory.Square.Hom.comm₁₂._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
                    CategoryTheory.Square.Hom.comm₁₃._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
                      CategoryTheory.Square.Hom.comm₂₄._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄)
                        CategoryTheory.Square.Hom.comm₃₄._autoParam →
                      sq₁.Hom sq₂