mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_p : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).right.p =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁
          n₂ hn₁' ⋯ ⋯).hom
      (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.smul_def : ∀ {G : Type u_3} [inst : DivInvMonoid G] (g : ConjAct G) (h : G),
  g • h = ConjAct.ofConjAct g * h * (ConjAct.ofConjAct g)⁻¹
-- Lean.Elab.DocString
/-- The parsed value.  -/
Lean.Doc.WithSyntax.val : {α : Type u} → Lean.Doc.WithSyntax α → α
-- Std.Async.Signal
Std.Async.Signal.sigabrt.sizeOf_spec : sizeOf Std.Async.Signal.sigabrt = 1
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below : {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} → {a : ℕ → ℕ} → Nat.Primrec a → Prop
-- Init.Data.Option.Array
Option.size_toArray : ∀ {α : Type u_1} {o : Option α}, o.toArray.size = if o.isSome = true then 1 else 0
-- Mathlib.Util.ParseCommand
/-- `captureException env s input` uses the given `Environment` `env` to parse the `String` `input`
using the `ParserFn` `s`.

This is a variation of `Lean.Parser.runParserCategory`.
 -/
Mathlib.GuardExceptions.captureException : Lean.Environment → Lean.Parser.ParserFn → String → Except String Lean.Syntax
-- Mathlib.Data.Matrix.Basic
/-- The `AlgHom` between spaces of square matrices induced by an `AlgHom` between their
coefficients. This is `Matrix.map` as an `AlgHom`.  -/
AlgHom.mapMatrix : {m : Type u_2} →
  {R : Type u_7} →
    {α : Type u_11} →
      {β : Type u_12} →
        [inst : Fintype m] →
          [inst_1 : DecidableEq m] →
            [inst_2 : CommSemiring R] →
              [inst_3 : Semiring α] →
                [inst_4 : Semiring β] →
                  [inst_5 : Algebra R α] → [inst_6 : Algebra R β] → (α →ₐ[R] β) → Matrix m m α →ₐ[R] Matrix m m β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {k : α},
  t.contains k = false ↔ k ∉ t
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- Given `n+1` objects of `C`, a fan for the last `n` with point `c₁.pt` and
a binary fan on `c₁.pt` and `f 0`, we can build a fan for all `n+1`.

In `extendFanIsLimit` we show that if the two given fans are limits, then this fan is also a
limit.
 -/
CategoryTheory.extendFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {f : Fin (n + 1) → C} →
        (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) →
          CategoryTheory.Limits.BinaryFan (f 0) c₁.pt → CategoryTheory.Limits.Fan f
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.limitConstTerminal_inv_π_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {j : J} {Z : C}
  (h : ((CategoryTheory.Functor.const J).obj (⊤_ C)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from (⊤_ C)) h
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack.eq_3 : ∀ (spec : Float.Model.Format) (s : Float.Model.UnpackedFloat.Sign),
  Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.zero s) = Float.Model.UnpackedFloat.packedZero spec s
-- Mathlib.FieldTheory.PrimitiveElement
Field.FiniteDimensional.of_exists_primitive_element : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  (∃ α, F⟮α⟯ = ⊤) → FiniteDimensional F E
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.MinimalAxioms.mk : ∀ {α : Type u} [inst : CompleteLattice α],
  (∀ (a : α) (s : Set α), a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b) → Order.Frame.MinimalAxioms α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- a family of objects which cover the terminal object  -/
SheafOfModules.LocalGeneratorsData.X : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {M : SheafOfModules R} →
          [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
              (self : M.LocalGeneratorsData) → self.I → C
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_inv' : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f : α → G), s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2)
  (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The length of the new subexpression.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.replacementSize : Mathlib.Tactic.ClickSuggestions.RwKey → ℕ
-- Mathlib.Order.Lattice
Antitone.map_sup_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeInf β] {f : α → β},
  Antitone f → ∀ (x y : α), f (x ⊔ y) ≤ f x ⊓ f y
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_zero : ∀ {M : Type u_4} [inst : AddMonoid M], WithZero.log 0 = 0
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallStrictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.Small.{w, v, u} P]
  (F : CategoryTheory.Functor C D), CategoryTheory.ObjectProperty.Small.{w, v', u'} (P.strictMap F)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- In a non-trivial module, zero is not non-degenerate.  -/
LinearMap.not_separatingLeft_zero : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} (M₁ : Type u_6) (M₂ : Type u_7) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] (I₁ : R₁ →+* R)
  (I₂ : R₂ →+* R) [Nontrivial M₁], ¬LinearMap.SeparatingLeft 0
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.equiv_toLinearMap : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f), ↑h.equiv = TensorProduct.lift f
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.instSMulMulOppositeSubtypeMem : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → SMul Rᵐᵒᵖ ↥I
-- Mathlib.Order.Atoms
/-- Every element other than `⊤` has an atom above it.  -/
IsCoatomic.eq_top_or_exists_le_coatom : ∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderTop α} [self : IsCoatomic α] (b : α),
  b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.ofFactorizationData_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I = h.Z
-- Lean.Elab.Term.TermElabM
/-- Execute `x` using `levelNames` as the universe level parameter names. See `getLevelNames`.  -/
Lean.Elab.Term.withLevelNames : {α : Type} → List Lean.Name → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Order.CompleteLattice.Basic
iInf_Prop_eq : ∀ {ι : Sort u_4} {p : ι → Prop}, ⨅ i, p i = ∀ (i : ι), p i
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instIsRightCancelAddOfAddOpposite : ∀ {M : Type u_1} [inst : Add Mᵃᵒᵖ] [IsRightCancelAdd Mᵃᵒᵖ], IsRightCancelAdd Mᵈᵃᵃ
-- Mathlib.Order.Preorder.Chain
IsChain.image_relIso_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ≃r r'},
  IsChain r' (⇑φ '' s) ↔ IsChain r s
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The **Cauchy-Schwarz inequality** for positive semidefinite forms.  -/
LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) → ∀ (x y : M), (B x) y * (B y) x ≤ (B x) x * (B y) y
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.read_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ : Type u}
  {epost : EPred} (post : ρ → ρ → Pred), ⦃ fun r => post r r ⦄ MonadReaderOf.read ⦃ post; epost ⦄
-- Lean.Elab.Match
Lean.Elab.Term.PatternVarDecl.mk.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf { fvarId := fvarId } = 1 + sizeOf fvarId
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = none ↔ t.isEmpty = true
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- A version of `fderivWithin_comp` that is useful to rewrite the composition of two derivatives
into a single derivative. This version always applies, but creates a new side-goal `f x = y`.  -/
fderivWithin_fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E}
  {t : Set F},
  DifferentiableWithinAt 𝕜 g t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          f x = y → ∀ (v : E), (fderivWithin 𝕜 g t y) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerFun_sModEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsPrecomplete I R] {x : Perfection (R ⧸ I) p} {y : R} {n : ℕ},
  (Ideal.Quotient.mk I) y = (Perfection.coeff (R ⧸ I) p n) x → x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.parentName? : Lean.Elab.Term.LetRecToLift → Option Lean.Name
-- Mathlib.Order.UpperLower.Relative
isRelLowerSet_Icc_ge : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {c : α}, IsRelLowerSet (Set.Icc c a) fun x => c ≤ x
-- Batteries.Data.String.Lemmas
String.utf8GetAux_add_right_cancel : ∀ (s : List Char) (i p n : ℕ),
  String.Pos.Raw.utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } =
    String.Pos.Raw.utf8GetAux s { byteIdx := i } { byteIdx := p }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_drop : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.drop n).edges = List.drop n p.edges
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.submodule_eq_top_iff : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M}, LinearMap.IsProj m f → (m = ⊤ ↔ f = LinearMap.id)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont : Type
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- An ideal of `R` such that `I.den • I = I.num`, see `FractionalIdeal.den` and
`FractionalIdeal.den_mul_self_eq_num`.  -/
FractionalIdeal.num : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P → Ideal R
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.getThenInsertIfNew? a b = t_1.getThenInsertIfNew? a b_1
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    Module.Flat R ↥A ∨ Module.Flat R ↥B →
      (∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Init.Data.Int.Pow
Int.one_pow : ∀ {n : ℕ}, 1 ^ n = 1
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence.  -/
CoalgEquivClass.toCoalgEquiv : {F : Type u_5} →
  {R : Type u_6} →
    {A : Type u_7} →
      {B : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : AddCommMonoid B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : EquivLike F A B] → [CoalgEquivClass F R A B] → F → A ≃ₗc[R] B
-- Mathlib.Data.Finset.Sort
Finset.sort.eq_1 : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], s.sort r = s.val.sort r
-- Lean.Meta.Tactic.SolveByElim
/-- Process the `intro` and `constructor` options by implementing the `discharger` tactic.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.processOptions : Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Meta.SolveByElim.SolveByElimConfig
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.mk.injEq : ∀ (applyEdit? : Option Bool) (workspaceEdit? : Option Lean.Lsp.WorkspaceEditClientCapabilities)
  (applyEdit?_1 : Option Bool) (workspaceEdit?_1 : Option Lean.Lsp.WorkspaceEditClientCapabilities),
  ({ applyEdit? := applyEdit?, workspaceEdit? := workspaceEdit? } =
      { applyEdit? := applyEdit?_1, workspaceEdit? := workspaceEdit?_1 }) =
    (applyEdit? = applyEdit?_1 ∧ workspaceEdit? = workspaceEdit?_1)
-- Init.Data.Array.Erase
Array.eraseP_of_forall_mem_not : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (∀ a ∈ xs, ¬p a = true) → xs.eraseP p = xs
-- Lean.Exception
/-- Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
This tag is used by the 'import unknown identifier' code action to detect messages that should
prompt the code action.
The end position of the range of an unknown identifier message should always point at the end of the
unknown identifier.

If `declHint` is specified, a corresponding hint is added to the message in case the name refers to
a private declaration that is not accessible in the current context.
 -/
Lean.mkUnknownIdentifierMessage : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadError m] → Lean.MessageData → optParam Lean.Name Lean.Name.anonymous → m Lean.MessageData
-- Mathlib.Data.Matrix.Basic
Matrix.algebraMap_eq_diagonalRingHom : ∀ {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α],
  algebraMap R (Matrix n n α) = (Matrix.diagonalRingHom n α).comp (algebraMap R (n → α))
-- Mathlib.Order.Atoms
GaloisCoinsertion.isCoatom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u),
  l ⊤ = ⊤ → (∀ (b : β), IsCoatom b → l (u b) = b) → ∀ (b : β), IsCoatom (u b) ↔ IsCoatom b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGE?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t₂
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Core function that delaborates a negative integer literal (a `Neg.neg` applied to `OfNat.ofNat`).
 -/
Lean.PrettyPrinter.Delaborator.delabNegIntCore : optParam Bool false → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.fintypeQuotientRightRel.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} [inst_1 : Fintype (α ⧸ s)],
  QuotientAddGroup.fintypeQuotientRightRel =
    Fintype.ofEquiv (α ⧸ s) (QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s).symm
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.ciSup_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι},
  (∃ x ∈ s, sSup ∅ ≤ f x) → ⨆ i ∈ s, f i ∈ Finset.image f s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k fallback : α},
  (Std.DHashMap.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.DHashMap.Const.get m x_2 ⋯)).getD fallback
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover),
  AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱 =
    ⨆ i,
      AlgebraicGeometry.Scheme.Hom.opensRange
        ((AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_div : ∀ (m n : ℕ), ↑(m / n) = ↑m / ↑n
-- Mathlib.Data.Finset.Sups
Finset.singleton_infs_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {a b : α}, {a} ⊼ {b} = {a ⊓ b}
-- Mathlib.Algebra.Module.Equiv.Basic
/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
linear isomorphism between the two function spaces.

See `LinearEquiv.arrowCongrAddEquiv` for the additive version of this isomorphism that works
over a not necessarily commutative semiring.  -/
LinearEquiv.arrowCongr : {R₁ : Type u_9} →
  {R₂ : Type u_10} →
    {R₁' : Type u_12} →
      {R₂' : Type u_13} →
        {M₁ : Type u_17} →
          {M₂ : Type u_18} →
            {M₁' : Type u_20} →
              {M₂' : Type u_21} →
                [inst : Semiring R₁] →
                  [inst_1 : Semiring R₂] →
                    [inst_2 : CommSemiring R₁'] →
                      [inst_3 : CommSemiring R₂'] →
                        [inst_4 : AddCommMonoid M₁] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : AddCommMonoid M₁'] →
                              [inst_7 : AddCommMonoid M₂'] →
                                [inst_8 : Module R₁ M₁] →
                                  [inst_9 : Module R₂ M₂] →
                                    [inst_10 : Module R₁' M₁'] →
                                      [inst_11 : Module R₂' M₂'] →
                                        {σ₁₂ : R₁ →+* R₂} →
                                          {σ₂₁ : R₂ →+* R₁} →
                                            {σ₁'₂' : R₁' →+* R₂'} →
                                              {σ₂'₁' : R₂' →+* R₁'} →
                                                {σ₁₁' : R₁ →+* R₁'} →
                                                  {σ₂₂' : R₂ →+* R₂'} →
                                                    {σ₂₁' : R₂ →+* R₁'} →
                                                      {σ₁₂' : R₁ →+* R₂'} →
                                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                                            [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                                                              [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                                                                [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] →
                                                                  [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] →
                                                                    [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] →
                                                                      [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] →
                                                                        (M₁ ≃ₛₗ[σ₁₂] M₂) →
                                                                          (M₁' ≃ₛₗ[σ₁'₂'] M₂') →
                                                                            (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₛₗ[σ₁'₂']
                                                                              M₂ →ₛₗ[σ₂₂'] M₂'
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.beta : Lean.Option Bool
-- Lean.Elab.DocString
Lean.Doc.instBEqSuggestionMode : BEq Lean.Doc.SuggestionMode
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : MulOne M] [inst_1 : MulOne N] (toOneHom : OneHom M N)
  (map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y) (toOneHom_1 : OneHom M N)
  (map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y),
  ({ toOneHom := toOneHom, map_mul' := map_mul' } = { toOneHom := toOneHom_1, map_mul' := map_mul'_1 }) =
    (toOneHom = toOneHom_1)