mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : Module R M₁]
  [inst_8 : Module R M₂] [inst_9 : Module R M₃] [inst_10 : Module R N₁] (f₁ : M₁ →ₗ[R] N₁)
  (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃),
  ↑(TensorProduct.assoc R N₁ M₂ M₃).symm ∘ₗ TensorProduct.map f₁ f₂₃ =
    TensorProduct.map (TensorProduct.map f₁ LinearMap.id) LinearMap.id ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.restrict_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S), (s.reindex e).restrict S ⋯ = (s.restrict S hS).reindex e
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_comap : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] (A : ValuationSubring L) (f : K →+* L),
  ↑(A.comap f) = ⇑f ⁻¹' ↑A
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC] (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} {x : ↑X}
  {hxU : x ∈ U} {hxV : x ∈ V} (W : TopologicalSpace.Opens ↑X),
  x ∈ W →
    ∀ (iWU : W ⟶ U) (iWV : W ⟶ V) {sU : CategoryTheory.ToType (F.obj (Opposite.op U))}
      {sV : CategoryTheory.ToType (F.obj (Opposite.op V))},
      (CategoryTheory.ConcreteCategory.hom (F.map iWU.op)) sU =
          (CategoryTheory.ConcreteCategory.hom (F.map iWV.op)) sV →
        (CategoryTheory.ConcreteCategory.hom (F.germ U x hxU)) sU =
          (CategoryTheory.ConcreteCategory.hom (F.germ V x hxV)) sV
-- Mathlib.Order.Category.FinBddDistLat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
FinBddDistLat.Hom.Simps.hom : (X Y : FinBddDistLat) → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Lean.DocString.DeferredCheck
/-- The check was deferred from the `n`th module docstring of the module (0-indexed).  -/
Lean.Doc.DeferredCheckSite.moduleDoc : ℕ → Lean.Doc.DeferredCheckSite
-- Init.Prelude
/-- `a + b` computes the sum of `a` and `b`. See `HAdd`.  -/
Add.add : {α : Type u} → [self : Add α] → α → α → α
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.keyAtIdx! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → ℕ → α
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_iff_of_mono : ∀ {X : SSet} {n : ℕ} {Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_biSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  (s : Finset ι) (N : ι → Submodule R M), (∀ i ∈ s, (N i).FG) → (⨆ i ∈ s, N i).FG
-- Mathlib.Data.Seq.Computation
Computation.destruct_map : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α),
  (Computation.map f s).destruct = Computation.lmap f (Computation.rmap (Computation.map f) s.destruct)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.instBEqSearchStep : {s : String.Slice} → BEq (String.Slice.Pattern.SearchStep s)
-- Mathlib.CategoryTheory.Filtered.Small
/-- The "filtered closure" of an `α`-indexed family of objects in `C` is the set of objects in `C`
obtained by starting with the family and successively adding maxima and coequalizers.  -/
CategoryTheory.IsFiltered.filteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {α : Type w} → (α → C) → CategoryTheory.ObjectProperty C
-- Mathlib.RingTheory.Ideal.Maps
Ideal.smul_restrictScalars : ∀ {R : Type u_4} {S : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (I : Ideal R)
  (N : Submodule S M),
  Submodule.restrictScalars R (Ideal.map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_singleton : ∀ {m n : ℤ}, n = m + 1 → (m<...=n).toArray = #[m + 1]
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertManyIfNew : {α : Type u} →
  {β : α → Type v} →
    {ρ : Type w} →
      [ForIn Id ρ ((a : α) × β a)] →
        [inst : BEq α] →
          [inst_1 : Hashable α] →
            (m : Std.DHashMap.Internal.Raw₀ α β) →
              ρ →
                { m' //
                  ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
                    (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insertIfNew a b)) →
                      P m → P m' }
-- Mathlib.Topology.ContinuousMap.Defs
/-- `ContinuousMapClass F X Y` states that `F` is a type of continuous maps.

You should extend this class when you extend `ContinuousMap`.  -/
ContinuousMapClass : (F : Type u_1) →
  (X : outParam (Type u_2)) →
    (Y : outParam (Type u_3)) → [TopologicalSpace X] → [TopologicalSpace Y] → [FunLike F X Y] → Prop
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux2.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α × List β → Sort u_3) →
      (x : List α × List β) → ((us : List α) → (zs : List β) → motive (us, zs)) → motive x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
ContinuousOn.logb : ∀ {α : Type u_1} {b : ℝ} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α},
  ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn (fun x => Real.logb b (f x)) s
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis.eRk_eq_eRk_insert : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → ∀ (e : α), M.eRk (insert e I) = M.eRk (insert e X)
-- Std.Async.Basic
/-- Runs two computations concurrently and returns the result of the one that finishes first.
The other result is lost and the other task is not cancelled, so the task will continue the execution
until the end.
 -/
Std.Async.Async.race : {α : Type} →
  [Inhabited α] →
    Std.Async.Async α → Std.Async.Async α → optParam Task.Priority Task.Priority.default → Std.Async.Async α
-- Init.Data.AC
Lean.Data.AC.ContextInformation.isIdem : {α : Sort u} → [self : Lean.Data.AC.ContextInformation α] → α → Bool
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (hom : M.X ⟶ N.X) [isMonHom_hom : CategoryTheory.IsMonHom hom] (hom_1 : M.X ⟶ N.X)
  (isMonHom_hom_1 : CategoryTheory.IsMonHom hom_1),
  ({ hom := hom, isMonHom_hom := isMonHom_hom } = { hom := hom_1, isMonHom_hom := isMonHom_hom_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_η : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.AddMon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.StructuredArrow.projectSubobject_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Limits.HasFiniteLimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T}
  (P : CategoryTheory.Subobject A),
  ∃ q, CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionContext.mk : Array Lean.Lsp.Diagnostic →
  Option (Array Lean.Lsp.CodeActionKind) → Option Lean.Lsp.CodeActionTriggerKind → Lean.Lsp.CodeActionContext
-- Lean.Parser.Command
Lean.Parser.Command.classTk.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_4 : Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h₂.opcyclesIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.opcyclesIso.hom γ.φQ
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of the forward direction of `Polynomial.splits_X_mul`. -/
Polynomial.Splits.of_X_mul : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R], (Polynomial.X * f).Splits → f.Splits
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.multiset_noncommSum_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (g : Multiset G) (comm : {x | x ∈ g}.Pairwise AddCommute),
  (∀ a ∈ g, a ∈ K) → g.noncommSum comm ∈ K
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanQuadrant.pathConnectedSpace : ∀ {n : ℕ}, PathConnectedSpace (EuclideanQuadrant n)
-- Mathlib.Topology.Order
continuous_id_iff_le : ∀ {α : Type u} {t t' : TopologicalSpace α}, Continuous id ↔ t ≤ t'
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.instIsWellOrderContinuousCompOfPreservesWellOrderContinuousOfShape : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (J : Type w) [inst_2 : LinearOrder J] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D)
  [F.IsWellOrderContinuous] [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G],
  (F.comp G).IsWellOrderContinuous
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_X_inr : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₂),
  (MvPolynomial.sumAlgEquiv R S₁ S₂) (MvPolynomial.X (Sum.inr c)) = MvPolynomial.C (MvPolynomial.X c)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_list_eq_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, t.insertMany l = List.foldl (fun acc p => acc.insert p.fst p.snd) t l
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I)
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i)))
      (CategoryTheory.CategoryStruct.comp X.cofanPtIsoSelf.inv h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i) h
-- Mathlib.Algebra.Notation.Support
Function.compl_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M}, (Function.support f)ᶜ = {x | f x = 0}
-- Mathlib.Tactic.Monotonicity.Attr
Mathlib.Tactic.Monotonicity.mono.side : Lean.ParserDescr
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromCommLeftNeg.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M),
  S.fromCommLeftNeg = { toFun := S.fromLeftNeg, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Lean.Expr.Basic
/-- Checks whether this `ConstantInfo` is a theorem.  -/
Lean.ConstantInfo.isThm : Lean.ConstantInfo → Bool
-- Init.Data.Ord.Basic
Ordering.not_isGE_eq_isLT : ∀ {o : Ordering}, (!o.isGE) = o.isLT
-- Init.Data.SInt.Lemmas
instCommutativeInt32HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Data.EReal.Inv
EReal.abs_zero : EReal.abs 0 = 0
-- Mathlib.Data.EReal.Operations
EReal.sub_add_cancel : ∀ {a : EReal} {b : ℝ}, a - ↑b + ↑b = a
-- Lean.Meta.Tactic.Grind.Types
/-- Node represented by this ENode.  -/
Lean.Meta.Grind.ENode.self : Lean.Meta.Grind.ENode → Lean.Expr
-- Init.Data.Array.Basic
/-- Applies a function to each element of the array, returning the resulting array of values.

Examples:
* `#[a, b, c].map f = #[f a, f b, f c]`
* `#[].map Nat.succ = #[]`
* `#["one", "two", "three"].map (·.length) = #[3, 3, 5]`
* `#["one", "two", "three"].map (·.reverse) = #["eno", "owt", "eerht"]`
 -/
Array.map : {α : Type u} → {β : Type v} → (α → β) → Array α → Array β
-- Init.Core
/-- A Boolean equality test coincides with propositional equality.

In other words:
* `a == b` implies `a = b`.
* `a == a` is true.
 -/
LawfulBEq : (α : Type u) → [BEq α] → Prop
-- Mathlib.Analysis.BoxIntegral.Basic
/-- **Henstock-Sacks inequality**. Let `r₁ r₂ : ℝⁿ → (0, ∞)` be a function such that for any tagged
*partition* of `I` subordinate to `rₖ`, `k=1,2`, the integral sum of `f` over this partition differs
from the integral of `f` by at most `εₖ`. Then for any two tagged *prepartition* `π₁ π₂` subordinate
to `r₁` and `r₂` respectively and covering the same part of `I`, the integral sums of `f` over these
prepartitions differ from each other by at most `ε₁ + ε₂`.

The actual statement

- uses `BoxIntegral.Integrable.convergenceR` instead of a predicate assumption on `r`;
- uses `BoxIntegral.IntegrationParams.MemBaseSet` instead of “subordinate to `r`” to
  account for additional requirements like being a Henstock partition or having a bounded
  distortion.

See also `BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq` and
`BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet`.
 -/
BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  {c₁ c₂ : NNReal} {ε₁ ε₂ : ℝ} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.Integrable I l f vol),
  0 < ε₁ →
    0 < ε₂ →
      l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁ →
        l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂ →
          π₁.iUnion = π₂.iUnion → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε₁ + ε₂
-- Mathlib.Analysis.Asymptotics.Defs
/-- If each term `A i` of a sum `IsBigO` of `B i`, then the sum of the `A i` `IsBigO` of the sum
of the norms of the `B i`.  -/
Asymptotics.IsBigOWith.sum_congr : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {C : ι → ℝ} {s : Finset ι} {B : ι → α → ℝ},
  (∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) (B i)) →
    Asymptotics.IsBigOWith (sSup (C '' ↑s)) l (fun H => ∑ i ∈ s, A i H) fun H => ∑ i ∈ s, ‖B i H‖
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The standard coordinates of `𝔸(n; S)`.  -/
AlgebraicGeometry.AffineSpace.coord : {n : Type u} → (S : AlgebraicGeometry.Scheme) → n → ↑((AlgebraicGeometry.AffineSpace n S).presheaf.obj (Opposite.op ⊤))
-- Init.Data.Int.DivMod.Lemmas
Int.zero_fmod : ∀ (b : ℤ), Int.fmod 0 b = 0
-- Mathlib.Tactic.TermCongr
/-- Walks along both `lhs` and `rhs` simultaneously to create a congruence lemma between them.

Where they are desynchronized, we fall back to the base case (using `CongrResult.mkDefault'`)
since it's likely due to unification with the expected type,
from `_` placeholders or implicit arguments being filled in.
 -/
Mathlib.Tactic.TermCongr.mkCongrOf : ℕ → ℕ → Lean.Expr → Lean.Expr → Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.uniformContinuous : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], UniformContinuous Subtype.val
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is isomorphic to its image under an `AlgHom`
(which is automatically injective).  -/
IntermediateField.equivMap : {F : Type u_4} →
  [inst : Field F] →
    {E : Type u_5} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type u_6} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                (L : IntermediateField F E) → (f : E →ₐ[F] K) → ↥L ≃ₐ[F] ↥(IntermediateField.map f L)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  a ∈ m ↔ (m.get? a).isSome = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.mk.injEq : ∀ {X : Type u_5} [inst : TopologicalSpace X] (toSetoid : Setoid X)
  (isOpen_setOfPred_rel : ∀ (x : X), IsOpen (Set.ofPred (toSetoid x))) (toSetoid_1 : Setoid X)
  (isOpen_setOfPred_rel_1 : ∀ (x : X), IsOpen (Set.ofPred (toSetoid_1 x))),
  ({ toSetoid := toSetoid, isOpen_setOfPred_rel := isOpen_setOfPred_rel } =
      { toSetoid := toSetoid_1, isOpen_setOfPred_rel := isOpen_setOfPred_rel_1 }) =
    (toSetoid = toSetoid_1)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instIsScalarTowerSubtypeMem_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  {E : Type u_4} [inst_3 : Field E] [inst_4 : Algebra L E] (T : IntermediateField (↥S) E) [inst_5 : Algebra K E]
  [inst_6 : IsScalarTower K L E], IsScalarTower K ↥S ↥T
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommMonCat)
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- A charted space over a T1 space is T1. Note that this is *not* true for T2 (for instance for
the real line with a double origin).  -/
ChartedSpace.t1Space : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M] [T1Space H],
  T1Space M
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ioo_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c ≤ a → c ∉ Set.Ioo a b
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_comp_map : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  {N' : Type u5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N']
  (f : M →ₗ[R] N) (g : N →ₗ[R] N'), (ExteriorAlgebra.map g).comp (ExteriorAlgebra.map f) = ExteriorAlgebra.map (g ∘ₗ f)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_findIdxM? : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type u} (f : γ → α → m Bool)
  (xs : Array α), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.findIdxM? (f x) xs
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousAt.sdiv : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] [inst_5 : TopologicalSpace α] {f g : α → P} {x : α},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => f x /ₛ g x) x
-- Mathlib.LinearAlgebra.Projection
/-- If `q` is a complement of `p`, then `M ⧸ p ≃ q`. The forward direction sends a quotient class
to its projection onto `q` along `p`; the backward direction sends an element of `q` to its class
in `M ⧸ p`.  -/
Submodule.quotientEquivOfIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → (E ⧸ p) ≃ₗ[R] ↥q
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.neg_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ), (-f) n = -f n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokenType.toJson : Lean.Lsp.SemanticTokenType → Lean.Json
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F : C ⥤ D` commutes with shifts, this expresses the compatibility of `F.mapTriangle`
with the equivalences `Pretriangulated.triangleOpEquivalence` on `C` and `D`.
 -/
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                (T : CategoryTheory.Pretriangulated.Triangle C) →
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence D).functor.obj
                      (Opposite.op (F.mapTriangle.obj T)) ≅
                    F.op.mapTriangle.obj
                      ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T))
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.coe_top : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] {x : CompleteLattice β}, ⇑⊤ = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.edge_symm : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.symm.edge = d.edge
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- When `adj : F ⊣ G` is an adjunction, with `F` oplax monoidal and `G` lax-monoidal,
this typeclass expresses compatibilities between the adjunction and the (op)lax
monoidal structures.  -/
CategoryTheory.Adjunction.IsMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} → (F ⊣ G) → [F.OplaxMonoidal] → [G.LaxMonoidal] → Prop
-- Mathlib.GroupTheory.Subgroup.Simple
isSimpleAddGroup_iff : ∀ (A : Type u_2) [inst : AddGroup A],
  IsSimpleAddGroup A ↔ Nontrivial A ∧ ∀ (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤
-- Init.Prelude
instInhabitedOption : {α : Type u_1} → Inhabited (Option α)