mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.SeparatingRight.toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  M.SeparatingRight → ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingRight
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.op.limitsOfShape J = (P.colimitsOfShape Jᵒᵖ).op
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.IsScalarTower.compatibleSMul : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {R : Type u_14} {S : Type u_15}
  [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂] [inst_6 : Module S M₂]
  [inst_7 : SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂], LinearMap.CompatibleSMul M M₂ R S
-- Mathlib.Data.FunLike.IsApply
IsSubApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Sub β]
  [inst_2 : Sub F], (∀ (f g : F) (x : α), (f - g) x = f x - g x) → IsSubApply F α β
-- Mathlib.Data.Set.Function
/-- Non-dependent version of `Function.update_comp_eq_of_notMem_range'`  -/
Function.update_comp_eq_of_notMem_range : ∀ {α : Sort u_7} {β : Type u_8} {γ : Sort u_9} [inst : DecidableEq β] (g : β → γ) {f : α → β} {i : β} (a : γ),
  i ∉ Set.range f → Function.update g i a ∘ f = g ∘ f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂)[k]! = default
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_subtype_range : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {f : ι → A}, Function.Injective f → (AlgebraicIndependent R Subtype.val ↔ AlgebraicIndependent R f)
-- Lean.DocString.Extension
Lean.ModuleDoc : Type
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instEmptyCollection : {α : Type u} → {β : Type v} → EmptyCollection (Std.HashMap.Raw α β)
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finite_of_finrank_eq_succ : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R] {n : ℕ}, Module.finrank R M = n.succ → Module.Finite R M
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.lift_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5}
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M] [inst_8 : Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M}
  (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁) (x₂ : M₂), (h.lift f') ((f x₁) x₂) = (f' x₁) x₂
-- Init.Data.Vector.Attach
_private.Init.Data.Vector.Attach.0.Vector.unattach.eq_1 : ∀ {n : ℕ} {α : Type u_1} {p : α → Prop} (xs : Vector { x // p x } n), xs.unattach = Vector.map (fun x => ↑x) xs
-- Mathlib.Data.Finset.Slice
Set.Sized.isAntichain : ∀ {α : Type u_1} {A : Set (Finset α)} {r : ℕ}, Set.Sized r A → IsAntichain (fun x1 x2 => x1 ⊆ x2) A
-- Mathlib.Data.PNat.Xgcd
/-- `qp = q - 1`  -/
PNat.XgcdType.qp : PNat.XgcdType → ℕ
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.HasSupport.mk : ∀ {β : Type u_2} {L : SummationFilter β}, (∀ᶠ (s : Finset β) in L.filter, ↑s ⊆ L.support) → L.HasSupport
-- Mathlib.Topology.Algebra.MulAction
ContinuousAt.fun_vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y},
  ContinuousAt f b → ContinuousAt g b → ContinuousAt (fun i => f i +ᵥ g i) b
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.mk : Mathlib.Tactic.Translate.Permutation →
  Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMapClass.mk : ∀ {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  [inst_6 : FunLike F A₁ A₂],
  (∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ) → CompletelyPositiveMapClass F A₁ A₂
-- Init.Data.String.Decode
UInt8.IsUTF8FirstByte.eq_1 : ∀ (c : UInt8), c.IsUTF8FirstByte = (c &&& 128 = 0 ∨ c &&& 224 = 192 ∨ c &&& 240 = 224 ∨ c &&& 248 = 240)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'_hom : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'._auto_3),
  (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom =
    X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Logic.Relation
Relation.eq_comp : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Relation.Comp (fun x1 x2 => x1 = x2) r = r
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanILeanHeaderSetupInfoParams.mk.sizeOf_spec : ∀ (version : ℕ) (isSetupFailure : Bool) (directImports : Array Lean.Lsp.ImportInfo),
  sizeOf { version := version, isSetupFailure := isSetupFailure, directImports := directImports } =
    1 + sizeOf version + sizeOf isSetupFailure + sizeOf directImports
-- Aesop.Search.Expansion.Norm
_private.Aesop.Search.Expansion.Norm.0.Aesop.runNormRuleTac.err : Aesop.NormRule → Aesop.RuleTacInput → {α : Type} → Lean.MessageData → Lean.MetaM α
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.lt_def : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β],
  (fun x1 x2 => x1 < x2) = Filter.Germ.LiftRel fun x1 x2 => x1 < x2
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodEquiv_symm_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H) (q : (G ⧸ A) × H ⧸ B),
  (QuotientGroup.prodEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
Matrix.gram.eq_1 : ∀ {E : Type u_1} {n : Type u_2} (𝕜 : Type u_5) [inst : Inner 𝕜 E] (v : n → E),
  Matrix.gram 𝕜 v = Matrix.of fun i j => inner 𝕜 (v i) (v j)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = true → Std.DTreeMap.Const.get? t a = some (Std.DTreeMap.Const.getD t a fallback)
-- Init.Data.Option.Monadic
Option.elimM_bind : ∀ {m : Type u_1 → Type u_2} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (f : α → m (Option β))
  (y : m γ) (z : β → m γ),
  Option.elimM (x >>= f) y z = do
    let __do_lift ← x
    Option.elimM (f __do_lift) y z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simp_certC.eq_1 : ∀ (k₁ : ℤ) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly)
  (c : ℕ),
  Lean.Grind.CommRing.Stepwise.simp_certC k₁ p₁ k₂ m₂ p₂ p c =
    ((Lean.Grind.CommRing.Poly.mulConstC k₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c).beq' p
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.smul_left_of_tower : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M] [IsScalarTower S R M]
  {B : LinearMap.BilinForm R M} (r : S) (x y : M), (B (r • x)) y = r • (B x) y
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.cmpLT_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp],
  RBTree.RBNode.cmpLT cmp x y ↔ cmp x y = Ordering.lt
-- Mathlib.Geometry.RingedSpace.OpenImmersion
IsOpenMap.functor.eq_1 : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)),
  hf.functor =
    { obj := fun U => { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U, is_open' := ⋯ },
      map := fun {U V} h => IsOpenMap.functorMap ⋯ ⋯ ⋯, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.funSplitAt_apply : ∀ (Y : Type u_2) [inst : TopologicalSpace Y] {ι : Type u_7} [inst_1 : DecidableEq ι] (i : ι)
  (f : (j : ι) → (fun a => Y) j), (Homeomorph.funSplitAt Y i) f = (f i, fun j => f ↑j)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instIsIsoHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} {f : M ⟶ N} [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- Auxiliary definition for `rotateTrianglehIso`.  -/
CochainComplex.mappingCone.rotateHomotopyEquivComm₂Homotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            Homotopy
              (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).mor₃
                (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom)
              (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.id_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.Hom.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isLittleO_completion_right : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (f =o[l] fun x => ↑(g x)) ↔ f =o[l] g
-- Init.Grind.ToInt
Lean.Grind.ToInt.mk : {α : Type u} →
  {range : outParam Lean.Grind.IntInterval} →
    (toInt : α → ℤ) → (∀ (x y : α), toInt x = toInt y → x = y) → (∀ (x : α), toInt x ∈ range) → Lean.Grind.ToInt α range
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.functorPushforward_overForget_arrows : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Sieve Y),
  CategoryTheory.Presieve.functorPushforward (CategoryTheory.Over.forget X) S.arrows =
    CategoryTheory.Presieve.map (CategoryTheory.Over.forget X) S.arrows
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredColimits : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {κ : Cardinal.{w}} {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.IsCardinalAccessibleCategory C κ], CategoryTheory.HasCardinalFilteredColimits C κ
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.nhds_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], nhds 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), Filter.principal (Set.Iio γ)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.toLinearMap_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i),
  (f.toLinearMap m i) x = f (Function.update m i x)
-- Mathlib.Data.Set.Card
Set.encard_eq_encard_iff_encard_sdiff_eq_encard_sdiff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.minimal : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → Minimal M.Dep C
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instMax : {R : Type u} → {M : Type v} → [inst : VAdd R M] → Max (SubAddAction R M)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span is the `sInf` of subspaces containing the given points.  -/
AffineSubspace.affineSpan_eq_sInf : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s : Set P), affineSpan k s = sInf {s' | s ⊆ ↑s'}
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_finset_of_fintype : ∀ {α : Type u} [inst : Fintype α], Cardinal.mk (Finset α) = 2 ^ Fintype.card α
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {l : List (α × β)},
  (m.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) m l)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_pos : ∀ {n : ℕ} (b : BitVec n), 0 < b.toNat ↔ 0#n < b
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : SemilatticeSup β] [inst_1 : OrderBot β] {P : β → Prop} (Pbot : P ⊥)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : { x // P x }), (SupBotHom.subtypeVal Pbot Psup) x = ↑x
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_eq_extend : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ s = MeasureTheory.extend (fun t _ht => μ t) s
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.isPrefix_aig : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} (aig : Std.Sat.AIG α) (input : β aig len),
  Std.Sat.AIG.IsPrefix aig.decls (f aig input).aig.decls
-- Mathlib.Algebra.Polynomial.Laurent
/-- The ring homomorphism `C`, including `R` into the ring of Laurent polynomials over `R` as
the constant Laurent polynomials.  -/
LaurentPolynomial.C : {R : Type u_1} → [inst : Semiring R] → R →+* LaurentPolynomial R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.symm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Lean.Elab.Do.Basic
/-- Extracts `MonadInfo` and monadic result type `α` from the expected type of a `do` block `m α`.  -/
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.extractMonadInfo : Lean.Elab.Do.DoOps → Option Lean.Expr → Lean.Elab.TermElabM (Lean.Elab.Do.MonadInfo × Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (X : ℕ → C) →
            (x : (n : ℕ) → (F.obj (Opposite.op n)).obj.obj (Opposite.op (X n))) →
              (map : (n : ℕ) → X (n + 1) ⟶ X n) →
                (∀ (n : ℕ), CategoryTheory.EffectiveEpi (map n)) →
                  (∀ (n : ℕ),
                      (CategoryTheory.ConcreteCategory.hom
                            ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op (X (n + 1)))))
                          (x (n + 1)) =
                        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map (map n).op)) (x n)) →
                    CategoryTheory.coherentTopology.struct✝ F
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The topology associated to a basis of submodules in an algebra.  -/
SubmodulesRingBasis.topology : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → {B : ι → Submodule R A} → [Nonempty ι] → SubmodulesRingBasis B → TopologicalSpace A
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_def_of_ne_zero : ∀ {x : ℂ}, x ≠ 0 → ∀ (y : ℂ), x ^ y = Complex.exp (Complex.log x * y)
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_of_val_units : ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} (h : IsUnit ↑a), h.unit = a
-- Aesop.Index.Basic
Aesop.IndexMatchResult.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (rule : α) (locations : Array Aesop.IndexMatchLocation)
  (patternSubsts? : Option (Array Aesop.Substitution)),
  sizeOf { rule := rule, locations := locations, patternSubsts? := patternSubsts? } =
    1 + sizeOf rule + sizeOf locations + sizeOf patternSubsts?
-- Mathlib.Order.LatticeIntervals
Set.Ico.disjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a b : α} [inst_1 : Fact (a < b)] {x y : ↑(Set.Ico a b)},
  Disjoint x y ↔ ↑x ⊓ ↑y = a
-- Lean.Parser.Term
/-- `@x` disables automatic insertion of implicit parameters of the constant `x`.
`@e` for any term `e` also disables the insertion of implicit lambdas at this position.
 -/
Lean.Parser.Term.explicit : Lean.Parser.Parser
-- Mathlib.Data.Finset.Order
Finset.exists_le : ∀ {α : Type u} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] (s : Finset α), ∃ M, ∀ i ∈ s, i ≤ M
-- Mathlib.Geometry.Manifold.Riemannian.Basic
_private.Mathlib.Geometry.Manifold.Riemannian.Basic.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.NumberTheory.Modular
ModularGroup.lcRow0Extend.congr_simp : ∀ {cd cd_1 : Fin 2 → ℤ} (e_cd : cd = cd_1) (hcd : IsCoprime (cd 0) (cd 1)),
  ModularGroup.lcRow0Extend hcd = ModularGroup.lcRow0Extend ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Decidable.mul_lt_mul'' : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a b c d : M₀} [PosMulMono M₀]
  [PosMulStrictMono M₀] [MulPosStrictMono M₀] [DecidableLE M₀], a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.coeff_expand : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0
-- Mathlib.Order.SymmDiff
/-- **Alias** of `top_symmDiff`. -/
top_symmDiff' : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff ⊤ a = ￢a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_mul_le_of_one_le_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, a * b ≤ c → 1 ≤ b → a ≤ c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α} {h : a ∈ m}, m.getKey a h = m.getKey! a
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isBigO_completion_right : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (f =O[l] fun x => ↑(g x)) ↔ f =O[l] g
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsAffineSigmaObjScheme : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Finite σ] [∀ (i : σ), AlgebraicGeometry.IsAffine (g i)],
  AlgebraicGeometry.IsAffine (∐ g)
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.range_dualMap_dual_eq_span_singleton : ∀ {R : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  (f : Module.Dual R M₁), (LinearMap.dualMap f).range = R ∙ f
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_rcc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_eq_bot : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂}, f.ker = ⊥ ↔ Function.Injective ⇑f
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Icc_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Set.Icc l u = S}
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeDiscreteOfIsClosedUnderFiniteCoproductsOfFinite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteCoproducts] (J : Type u_2) [Finite J],
  P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.ofCocomplex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (Z : C),
  CategoryTheory.InjectiveResolution.ofCocomplex Z =
    CochainComplex.mk' (CategoryTheory.Injective.under Z)
      (CategoryTheory.Injective.syzygies (CategoryTheory.Injective.ι Z))
      (CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)) fun {X₀ X₁} f =>
      ⟨CategoryTheory.Injective.syzygies f, ⟨CategoryTheory.Injective.d f, ⋯⟩⟩
-- Lean.Data.Lsp.Client
Lean.Lsp.instToJsonRegistrationParams.toJson : Lean.Lsp.RegistrationParams → Lean.Json
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_not : ∀ (a : BitVec 8), { toBitVec := ~~~a } = ~~~{ toBitVec := a }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.toArray.size = m.size
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced.shiftIso.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (L : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C A) (M : Type u_4) [inst_3 : AddMonoid M]
  [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M] (F' : M → CategoryTheory.Functor D A)
  (e' e'_1 : (m : M) → L.comp (F' m) ≅ G.shift m),
  e' = e'_1 →
    ∀ [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
      [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
      [inst_9 : L.CommShift M] (n a a' : M) (ha' : n + a = a'),
      CategoryTheory.Functor.ShiftSequence.induced.shiftIso L G M F' e' n a a' ha' =
        CategoryTheory.Functor.ShiftSequence.induced.shiftIso L G M F' e'_1 n a a' ha'
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Computation of the `g'` field of `RightHomologyData.canonical`.  -/
CategoryTheory.ShortComplex.RightHomologyData.canonical_g' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.RightHomologyData.canonical S).g' = S.fromOpcycles