mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaForget_inv_app_app_hom_apply : ∀ (X : AddCommMonCatᵒᵖ) (X_1 : AddCommMonCat) (f : Opposite.unop X ⟶ X_1),
  (CategoryTheory.ConcreteCategory.hom ((AddCommMonCat.coyonedaForget.inv.app X).app X_1)) f = AddCommMonCat.Hom.hom f
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.of_surjectiveOnStalks : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (p : Ideal S) [inst_5 : p.IsPrime] [Algebra.QuasiFiniteAt R p]
  (f : S →ₐ[R] T),
  f.SurjectiveOnStalks → ∀ (q : Ideal T) [inst_7 : q.IsPrime], p = Ideal.comap f.toRingHom q → Algebra.QuasiFiniteAt R q
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.instAwayCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenHomToOpen : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R),
  IsLocalizedModule.Away f (ModuleCat.Hom.hom (AlgebraicGeometry.tilde.toOpen M (PrimeSpectrum.basicOpen f)))
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.eq_right : ∀ {α : Type u_2} [inst : CommMonoid α] [IsCancelMul α] {s : Set α},
  ThreeGPFree s → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c
-- Init.Data.Array.Erase
Array.eraseIdx_set : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} {hi : i < xs.size} {j : ℕ} {hj : j < (xs.set i a hi).size},
  (xs.set i a hi).eraseIdx j hj =
    if h' : j < i then (xs.eraseIdx j ⋯).set (i - 1) a ⋯
    else if h'' : j = i then xs.eraseIdx i hi else (xs.eraseIdx j ⋯).set i a ⋯
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.ext_iff : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  {p q : AlgebraNorm R S}, p = q ↔ ∀ (x : S), p x = q x
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toRingEquiv_unop : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ),
  (AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv
-- Mathlib.AlgebraicGeometry.Group.Abelian
AlgebraicGeometry.instIsClosedImmersionLeftSchemeOneOverSpecOf : ∀ {K : Type u} [inst : Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K)))
  [inst_1 : CategoryTheory.GrpObj G],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)
-- Init.Data.SInt.Basic
instXorOpInt32 : XorOp Int32
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDeriv_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E}, ω₁ =ᶠ[nhds x] ω₂ → extDeriv ω₁ x = extDeriv ω₂ x
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_chars : ∀ {s : String.Slice}, s.chars.toList = s.copy.toList
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.vadd_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : VAdd α M] (a : α) (f : β → M) (g : ι → β),
  (a +ᵥ f) ∘ g = a +ᵥ f ∘ g
-- Mathlib.Algebra.BigOperators.Fin
List.prod_take_ofFn : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin n → M) (i : ℕ),
  (List.take i (List.ofFn f)).prod = ∏ j with ↑j < i, f j
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x
-- Mathlib.Data.Set.Basic
Set.notMem_subset : ∀ {α : Type u} {a : α} {s t : Set α}, s ⊆ t → a ∉ t → a ∉ s
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Preprocessor.mk.sizeOf_spec : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase) (transform : Lean.Expr → Lean.MetaM (List Lean.Expr)),
  sizeOf { toPreprocessorBase := toPreprocessorBase, transform := transform } = 1 + sizeOf toPreprocessorBase
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_natCast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : AddLeftMono α]
  [inst_3 : ZeroLEOneClass α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.Data.Set.Image
/-- If preimage of each singleton under `f : α → β` is either empty or the whole type,
then `f` is a constant.  -/
Set.exists_eq_const_of_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β] {f : α → β},
  (∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = Set.univ) → ∃ b, f = Function.const α b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.map_eq_empty_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ}, Std.ExtHashMap.map f m = ∅ ↔ m = ∅
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find_root_2 : ∀ (self : Batteries.UnionFind) (x : Fin self.size), ↑↑(self.find x).snd = self.rootD ↑x
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closed : ∀ {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X],
  ∀ A ⊆ C,
    IsClosed A ↔
      (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) ∧
        IsClosed (A ∩ D)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If a short complex `S` is equipped with a splitting, then `S.X₁` is the kernel of `S.g`.  -/
CategoryTheory.ShortComplex.Splitting.fIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Limits.HasZeroObject C] →
          S.Splitting → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.or.inj : ∀ {a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.IProp}, a.or a_1 = a_2.or a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.symm_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (h : CategoryTheory.Arrow.LeftHomotopy f g), h.symm.hom = -h.hom
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instIsLocalizationPlusQuotientInverseImageHomologicalComplexIntUpHomotopyEquivalencesι : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.Plus.quotient C).IsLocalization
    ((HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C))
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.right_notMem_uIoo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ∉ Set.uIoo a b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_5.splitter : (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1) →
  (expr : Std.Tactic.BVDecide.BVLogicalExpr) →
    ((var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var)) →
      ((val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val)) →
        ((expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not) →
          ((discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs)) →
            ((g : Std.Tactic.BVDecide.Gate) →
                (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
                  motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)) →
              motive expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM f init t = Array.foldlM (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The canonical map from the coproduct induced by `f` to `S` as an isomorphism in
`CompHausLike P`.  -/
CompHausLike.LocallyConstant.sigmaIso : {P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} →
        (r : LocallyConstant (↑Q.toTop) Z) →
          [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
            CompHausLike.finiteCoproduct (CompHausLike.LocallyConstant.fiber r) ≅ Q
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.toNatModule : {α : Type u} → [I : Lean.Grind.Semiring α] → Lean.Grind.NatModule α
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.DiagnosticsState.mk.sizeOf_spec : ∀ (stickyDiagsRef : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic))
  (diags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic) (isIncremental : Bool) (publishedDiagsAmount : ℕ),
  sizeOf
      { stickyDiagsRef := stickyDiagsRef, diags := diags, isIncremental := isIncremental,
        publishedDiagsAmount := publishedDiagsAmount } =
    1 + sizeOf stickyDiagsRef + sizeOf diags + sizeOf isIncremental + sizeOf publishedDiagsAmount
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.coprime : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  IsCoprime (FermatLastTheoremForThreeGen.Solution'.a✝ self) (FermatLastTheoremForThreeGen.Solution'.b✝ self)
-- Mathlib.RingTheory.Jacobson.Ring
MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R] {σ : Type u_2} [Finite σ] {S : Type u_3} [inst_3 : Field S]
  (f : MvPolynomial σ R →+* S), Function.Surjective ⇑f → (f.comp MvPolynomial.C).IsIntegral
-- Mathlib.Computability.RE
/-- If `P` is computable, and if for every `x` there exists an `n` such that `P x n` holds,
then the function mapping `x` to the minimal such `n` (using `Nat.find`) is computable.
This formally bridges `Partrec.rfind` with total unbounded search.  -/
Computable.find : ∀ {α : Type u_1} [inst : Primcodable α] {P : α → ℕ → Prop} [inst_1 : DecidableRel P],
  (ComputablePred fun p => P p.1 p.2) → ∀ (hP_ex : ∀ (x : α), ∃ n, P x n), Computable fun x => Nat.find ⋯
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.peek k a q with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_2 (Turing.TM2.Stmt.peek k a q) k a q ⋯
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} (i : ↥b.support),
  RootPairing.GeckConstruction.h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x => ↑(P.pairingIn ℤ x ↑i))
-- Mathlib.Data.Nat.Nth
Nat.nth_count_eq_sInf : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.nth p (Nat.count p n) = sInf {i | p i ∧ n ≤ i}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A functor preserves zero morphisms if it sends zero morphisms to zero morphisms.  -/
CategoryTheory.Functor.PreservesZeroMorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasZeroMorphisms D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Data.Finset.Card
Finset.card_inter_add_card_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).card + (s \ t).card = s.card
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`.  -/
CategoryTheory.CosimplicialObject.truncationCompTrunc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n m : ℕ} →
      (h : m ≤ n) →
        (CategoryTheory.CosimplicialObject.truncation n).comp
            (CategoryTheory.CosimplicialObject.Truncated.trunc C n m ⋯) ≅
          CategoryTheory.CosimplicialObject.truncation m
-- Lean.Util.Trace
Lean.TraceElem.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (msg : Lean.MessageData), sizeOf { ref := ref, msg := msg } = 1 + sizeOf ref + sizeOf msg
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_bit_true : ∀ (n : ℕ), (Nat.bit true n).bitIndices = 0 :: List.map (fun x => x + 1) n.bitIndices
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- morphisms  -/
CategoryTheory.SmallCategoryOfSet.hom : {Ω : Type w} → (self : CategoryTheory.SmallCategoryOfSet Ω) → ↑self.obj → ↑self.obj → Set Ω
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.cotangentComplexAux_injective : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  Function.Injective ⇑P.cotangentComplexAux
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  (Std.DTreeMap.filterMap f t).getD k fallback = ((t.get? k).bind (f k)).getD fallback
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.uniformContinuous_coe_fun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)], UniformContinuous DFunLike.coe
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x y : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n),
  R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.toCloseds_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α],
  Function.Injective TopologicalSpace.Compacts.toCloseds
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optIdent : Lean.Parser.Parser
-- Mathlib.RingTheory.LaurentSeries
RatFunc.coeToLaurentSeries : {F : Type u} → [inst : Field F] → Coe (RatFunc F) (LaurentSeries F)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.ext_ring_iff : ∀ {R : Type u_1} {S : Type u_5} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₃]
  [inst_3 : Module S M₃] {σ : R →+* S} {f g : R →ₛₗ[σ] M₃}, f = g ↔ f 1 = g 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSMulZeroClass : {M : Type u_1} →
  {X : Type u_2} →
    [inst : Zero X] →
      [inst_1 : SMulZeroClass M X] →
        [inst_2 : TopologicalSpace X] → [ContinuousConstSMul M X] → SMulZeroClass M (SeparationQuotient X)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.quotEquivOfEqBot_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (hp : p = ⊥) (x : M), (p.quotEquivOfEqBot hp).symm x = Submodule.Quotient.mk x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The projection on the components of a wide pullback cone.  -/
CategoryTheory.Limits.WidePullbackCone.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} →
        {Y : ι → C} → {f : (i : ι) → Y i ⟶ X} → (s : CategoryTheory.Limits.WidePullbackCone f) → (i : ι) → s.pt ⟶ Y i
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} [inst_2 : SizeOf C] (f : X.fst ⟶ Y.fst)
  (comm :
    autoParam
      (∀ (U : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U) (Y.snd.β U).hom =
          CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f))
      CategoryTheory.Center.Hom.comm._autoParam),
  sizeOf { f := f, comm := comm } = 1 + sizeOf f
-- Mathlib.Computability.Partrec
Partrec.option_some_iff : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ},
  (Partrec fun a => Part.map some (f a)) ↔ Partrec f
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.coe_opAddEquiv : ∀ {M : Type u_1} [inst : AddCommMonoid M], ⇑AddOpposite.opAddEquiv = AddOpposite.op
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A spanning subgraph of an acyclic graph is acyclic.  -/
SimpleGraph.IsAcyclic.anti : ∀ {V : Type u_1} {G G' : SimpleGraph V}, G ≤ G' → G'.IsAcyclic → G.IsAcyclic
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_map : ∀ {K : Type u_6} {V : Type u_7} {W : Type u_8} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup W] [inst_4 : Module K W] {F : Type u_9}
  [inst_5 : EquivLike F (Module.End K V) (Module.End K W)] [AlgEquivClass F K (Module.End K V) (Module.End K W)] (f : F)
  (x : Module.End K V), (LinearMap.trace K W) (f x) = (LinearMap.trace K V) x
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_strictMono : StrictMono ⇑Ordinal.preOmega
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.injective_respectsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.injective C).RespectsIso
-- Mathlib.Data.Nat.Prime.Basic
Nat.prime_mul_iff : ∀ {a b : ℕ}, Nat.Prime (a * b) ↔ Nat.Prime a ∧ b = 1 ∨ Nat.Prime b ∧ a = 1
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  [inst_1 : SizeOf C] (s' : X.right ⟶ X.left.obj (Opposite.op { len := 0 }))
  (s : (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 }))
  (s'_comp_ε :
    autoParam
      (CategoryTheory.CategoryStruct.comp s' (X.hom.app (Opposite.op { len := 0 })) =
        CategoryTheory.CategoryStruct.id X.right)
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε._autoParam)
  (s₀_comp_δ₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (s 0) (X.left.δ 1) =
        CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) s')
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁._autoParam)
  (s_comp_δ₀ :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (s n) (X.left.δ 0) =
          CategoryTheory.CategoryStruct.id (X.left.obj (Opposite.op { len := n })))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀._autoParam)
  (s_comp_δ :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 2)),
        CategoryTheory.CategoryStruct.comp (s (n + 1)) (X.left.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.δ i) (s n))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ._autoParam)
  (s_comp_σ :
    autoParam
      (∀ (n : ℕ) (i : Fin (n + 1)),
        CategoryTheory.CategoryStruct.comp (s n) (X.left.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.left.σ i) (s (n + 1)))
      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ._autoParam),
  sizeOf
      { s' := s', s := s, s'_comp_ε := s'_comp_ε, s₀_comp_δ₁ := s₀_comp_δ₁, s_comp_δ₀ := s_comp_δ₀,
        s_comp_δ := s_comp_δ, s_comp_σ := s_comp_σ } =
    1 + sizeOf s' + sizeOf s'_comp_ε + sizeOf s₀_comp_δ₁
-- Init.Data.List.Count
List.countP_append : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, List.countP p (l₁ ++ l₂) = List.countP p l₁ + List.countP p l₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v
-- Init.Data.List.Lemmas
List.mem_set : ∀ {α : Type u_1} {l : List α} {i : ℕ}, i < l.length → ∀ (a : α), a ∈ l.set i a
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F] {X : C}
  {f g : X ⟶ CategoryTheory.Limits.end_ F},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.end_.π F j) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.end_.π F j)) →
    f = g
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceTextDocumentIdentifier : Lean.Lsp.FileSource Lean.Lsp.TextDocumentIdentifier
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_succ_ofBool : ∀ (b : Bool) (i : ℕ), (BitVec.ofBool b)[i + 1]? = none
-- Lean.Expr
/-- Return `p ∧ q`  -/
Lean.mkAnd : Lean.Expr → Lean.Expr → Lean.Expr