mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Init.Data.Range.Polymorphic.IntLemmas
Int.zero_ne_getElem!_toList_roo_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toList[i]! ≠ 0 ↔ i < (n - (m + 1)).toNat ∧ m + ↑i ≠ -1
-- Lean.Meta.Tactic.Grind.EMatch
/-- Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
`e` and `c.assignment[bidx]` are in the same equivalence class.
This function assumes `bidx < c.assignment.size`.
Recall that we initialize the assignment array with the number of theorem parameters.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assign? : Lean.Meta.Grind.EMatch.Choice → ℕ → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the reverse direction of `contMDiff_iff_contDiff`. -/
ContDiff.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'}, ContDiff 𝕜 n f → ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey? = some (t.maxKey he)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {p : α},
  Irreducible p → ∀ (k : ℕ), UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Ioo : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : LinearOrder X] [OrderClosedTopology X],
  IsLocallyClosed (Set.Ioo a b)
-- Lean.Util.PPExt
Lean.PrettyPrinter.InfoPerPos : Type
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Server.mk.inj : ∀ {shared shared_1 : Std.Http.Internal.Mock.SharedState✝},
  { shared := shared } = { shared := shared_1 } → shared = shared_1
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_iInf : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {s : ι → Set α},
  l.HasBasis (fun x => True) s → l = ⨅ i, Filter.principal (s i)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor_ne_zero_iff : ∀ {F : Type u_1} [inst : Field F] {x y : F}, Lagrange.basisDivisor x y ≠ 0 ↔ x ≠ y
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_sub : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]), ↑(z1 - z2) = ↑z1 - ↑z2
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.MonOpOpToComon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Comon.MonOpOpToComon C).map f).hom = f.unop.hom.unop
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.findCommonPrefix.findCommon : List Lean.Name → List Lean.Name → Lean.Name
-- Lean.Parser.Command
Lean.Parser.Command.eval.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instNatCastSubtypeMemAddSubgroup : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → NatCast ↥(selfAdjoint R)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_union_of_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Algebra.Order.Group.PosPart
negPart_eq_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a⁻ = 0 ↔ 0 ≤ a
-- Init.Data.String.Iterator
/-- The current UTF-8 byte position in the string `s`.

This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is `(default : Char)`, similar to `String.get` on an invalid position.
 -/
String.Legacy.Iterator.i : String.Legacy.Iterator → String.Pos.Raw
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorDiagonal_inv_hom : ∀ (G : Type u) [inst : Monoid G] (n : ℕ),
  (Action.diagonalSuccIsoTensorDiagonal G n).inv.hom = (Fin.consEquiv fun a => G).symm.toIso.inv
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_pow' : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a : M) {n : ℕ} [NeZero n], UniqueFactorizationMonoid.primeFactors (a ^ n) = UniqueFactorizationMonoid.primeFactors a
-- Mathlib.Algebra.Group.AddChar
AddChar.sub_apply' : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ χ : AddChar A M) (a : A),
  (ψ - χ) a = ψ a / χ a
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
uniqueMDiffOn_iff_uniqueDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, UniqueMDiff[s] ↔ UniqueDiffOn 𝕜 s
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence.  -/
Matrix.reindex : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type v} → m ≃ l → n ≃ o → Matrix m n α ≃ Matrix l o α
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.pi_eq_bot_iff : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (S : (i : ι) → Submonoid (M i)),
  Submonoid.pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.reindex : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α},
  A.IsSymm → ∀ (f : n ≃ m), ((Matrix.reindex f f) A).IsSymm
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instNeg : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] → [NegMemClass σ A] → {𝒜 : ι → σ} → (x : Submonoid A) → Neg (HomogeneousLocalization 𝒜 x)
-- Mathlib.Data.Tree.Basic
/-- The number of internal nodes (i.e. not including leaves) of a binary tree  -/
BinaryTree.numNodes : {α : Type u} → BinaryTree α → ℕ
-- Init.Try
Lean.Parser.Tactic.tryTraceWith : Lean.ParserDescr
-- Init.Data.ByteArray.Lemmas
ByteArray.append_toByteArray_singleton : ∀ {as : ByteArray} {a : UInt8}, as ++ [a].toByteArray = as.push a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).getKey? k = none
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), ReflBEq (β k)],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → m₁.beq m₂ = true
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_isoClosure : ∀ {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.isoClosure.limitsOfShape J = P.limitsOfShape J
-- Mathlib.Data.List.Sigma
List.kerase_sublist : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)), (List.kerase a l).Sublist l
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.OppositeShift.adjunction_unit : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  (CategoryTheory.OppositeShift.adjunction A adj).unit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.OppositeShift.natIsoId D A).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OppositeShift.natTrans A adj.counit)
        (CategoryTheory.NatTrans.OppositeShift.natIsoComp A G F).hom)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂)
  (hi₂ : i₂ < j) {Z : C} (h : F.obj ⟨i₂, hi₂⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.SuccStruct.ofCocone c).map (CategoryTheory.homOfLE hi))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₂ hi₂).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi)) h)
-- Mathlib.Order.RelClasses
/-- Derive a `WellFoundedRelation` instance from a `WellFoundedGT` instance.  -/
WellFoundedGT.toWellFoundedRelation : {α : Type u} → [inst : LT α] → [WellFoundedGT α] → WellFoundedRelation α
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  {m : M} {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ →
    ∀ (n : ℕ), ⁅e, ((LieModule.toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((LieModule.toEnd R L M) f ^ n) m
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_top : ∀ {c : Cardinal.{u}}, Cardinal.toENat c = ⊤ ↔ Cardinal.aleph0 ≤ c
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mul_of_top_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {f φ : α → 𝕜}, MeasureTheory.Integrable f μ → MeasureTheory.MemLp φ ⊤ μ → MeasureTheory.Integrable (φ * f) μ
-- Init.Data.Array.Range
Array.zipIdx_map_fst : ∀ {α : Type u_1} (i : ℕ) (xs : Array α), Array.map Prod.fst (xs.zipIdx i) = xs
-- Lean.Setup
/-- The type of module package identifiers.

This is a `String` that is used to disambiguate native symbol prefixes between
different packages \(and different versions of the same package\).
 -/
Lean.PkgId : Type
-- Mathlib.Topology.AlexandrovDiscrete
alexandrovDiscrete_iff_nhds : ∀ {α : Type u_3} [inst : TopologicalSpace α], AlexandrovDiscrete α ↔ ∀ (a : α), nhds a = Filter.principal (nhdsKer {a})
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec.eq_1 : ∀ {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)) (n : ℕ),
  Nat.binaryRec zero bit n =
    if n0 : n = 0 then ⋯ ▸ zero
    else
      have x := bit (1 &&& n != 0) (n >>> 1) (Nat.binaryRec zero bit (n >>> 1));
      ⋯ ▸ x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.lift_base_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
  (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) {Z : C}
  (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base arrows) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.r_le : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}, HasFPowerSeriesOnBall f p x r → r ≤ p.radius
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.congrTable : (self : Lean.Meta.Grind.GoalState) → Lean.Meta.Grind.CongrTable self.enodeMap
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddRightCancelMonoidOfAddOpposite : {M : Type u_1} → [AddRightCancelMonoid Mᵃᵒᵖ] → AddRightCancelMonoid Mᵈᵃᵃ
-- Mathlib.Algebra.Order.Ring.Idempotent
SemilatticeInf.mk.congr_simp : ∀ {α : Type u} [toPartialOrder : PartialOrder α] [toPartialOrder_1 : PartialOrder α]
  (e_toPartialOrder : toPartialOrder = toPartialOrder_1) (inf inf_1 : α → α → α) (e_inf : inf = inf_1)
  (inf_le_left : ∀ (a b : α), inf a b ≤ a) (inf_le_right : ∀ (a b : α), inf a b ≤ b)
  (le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c),
  { toPartialOrder := toPartialOrder, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf } =
    { toPartialOrder := toPartialOrder_1, inf := inf_1, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Lean.Server.FileWorker.Utils
_private.Lean.Server.FileWorker.Utils.0.Lean.Server.FileWorker.mkCmdSnaps.go : Lean.Language.Lean.CommandParsedSnapshot →
  Lean.Server.ServerTask (Except IO.Error (Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot))
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `CommGroup.isMulTorsion_quotient_range_powMonoidHom`. -/
CommGroup.isTorsion_quotient_range_powMonoidHom : ∀ (G : Type u_1) [inst : CommGroup G] {n : ℕ}, n ≠ 0 → IsMulTorsion (G ⧸ (powMonoidHom n).range)
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.reduce : Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
equal to the corresponding factor `g i` of another finite product, then
`∏ i ∈ s, f i ≤ ∏ i ∈ s, g i`.  -/
Finset.prod_le_prod' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f g : ι → N} {s : Finset ι}
  [MulLeftMono N], (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
-- Mathlib.Order.Filter.AtTopBot.ModEq
Nat.frequently_mod_eq : ∀ {d n : ℕ}, d < n → ∃ᶠ (m : ℕ) in Filter.atTop, m % n = d
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.createLocalPreDiscrTree : {α : Type} →
  Lean.Core.Context →
    Lean.NameGenerator →
      Lean.Environment →
        Lean.Meta.LazyDiscrTree.ImportData →
          (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
            BaseIO (Lean.Meta.LazyDiscrTree.PreDiscrTree α)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.inverse_counitInv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D),
  CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) =
    CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.Result.mk.sizeOf_spec : ∀ (expr : Mathlib.Tactic.BicategoryLike.NormalExpr) (proof : Lean.Expr),
  sizeOf { expr := expr, proof := proof } = 1 + sizeOf expr + sizeOf proof
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A function or predicate over `X` and `S` can be lifted to `X[S⁻¹]` if it is invariant
under expansion on the left.  -/
OreLocalization.liftExpand : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_3} →
          [inst_2 : MulAction R X] →
            {C : Sort u_2} →
              (P : X → ↥S → C) →
                (∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩) → OreLocalization S X → C
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Unexpander for `AddMonoidAlgebra`.  -/
AddMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Homology.DerivedCategory.Linear
DerivedCategory.instLinearSingleFunctor : ∀ (R : Type t) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : HasDerivedCategory C] (n : ℤ),
  CategoryTheory.Functor.Linear R (DerivedCategory.singleFunctor C n)
-- Lean.Environment
Lean.MonadEnv.mk : {m : Type → Type} → m Lean.Environment → ((Lean.Environment → Lean.Environment) → m Unit) → Lean.MonadEnv m
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact_le_cofinite : ∀ {X : Type u} [inst : TopologicalSpace X], Filter.cocompact X ≤ Filter.cofinite
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) =
    CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
      (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toList_rcc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...=n).toList[i]?.isSome = true) = (i < (n + 1 - m).toNat)
-- Mathlib.Order.Bounds.Basic
IsGLB.exists_between' : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → a ∉ s → a < b → ∃ c ∈ s, a < c ∧ c < b
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_strictMono : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → StrictMono (Ordinal.enumOrd s)
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.instAdditiveCommaFst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive], (CategoryTheory.Comma.fst L R).Additive
-- Mathlib.Tactic.CategoryTheory.Bicategory.Basic
/-- Normalize the both sides of an equality.  -/
Mathlib.Tactic.Bicategory.tacticBicategory_nf : Lean.ParserDescr
-- Mathlib.Algebra.Group.Semiconj.Defs
AddSemiconjBy.eq_1 : ∀ {M : Type u_2} [inst : Add M] (a x y : M), AddSemiconjBy a x y = (a + x = y + a)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X : C} {p₁ p₂ : R ⟶ X}
  {toReflexiveRelation : CategoryTheory.ReflexiveRelation p₁ p₂} {s : R ⟶ R}
  {symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam}
  {symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam}
  {c : CategoryTheory.Limits.PullbackCone p₂ p₁} {isLimit : CategoryTheory.Limits.IsLimit c} {t : c.pt ⟶ R}
  {transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam}
  {transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam}
  {toReflexiveRelation_1 : CategoryTheory.ReflexiveRelation p₁ p₂} {s_1 : R ⟶ R}
  {symmetry₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam}
  {symmetry₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam}
  {c_1 : CategoryTheory.Limits.PullbackCone p₂ p₁} {isLimit_1 : CategoryTheory.Limits.IsLimit c_1} {t_1 : c_1.pt ⟶ R}
  {transitivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₁ = CategoryTheory.CategoryStruct.comp c_1.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam}
  {transitivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₂ = CategoryTheory.CategoryStruct.comp c_1.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam},
  { toReflexiveRelation := toReflexiveRelation, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂, c := c,
        isLimit := isLimit, t := t, transitivity₁ := transitivity₁, transitivity₂ := transitivity₂ } =
      { toReflexiveRelation := toReflexiveRelation_1, s := s_1, symmetry₁ := symmetry₁_1, symmetry₂ := symmetry₂_1,
        c := c_1, isLimit := isLimit_1, t := t_1, transitivity₁ := transitivity₁_1, transitivity₂ := transitivity₂_1 } →
    toReflexiveRelation = toReflexiveRelation_1 ∧ s = s_1 ∧ c = c_1 ∧ isLimit ≍ isLimit_1 ∧ t ≍ t_1
-- Mathlib.Algebra.Group.Semiconj.Defs
AddSemiconjBy.nsmul_right : ∀ {M : Type u_2} [inst : AddMonoid M] {a x y : M}, AddSemiconjBy a x y → ∀ (n : ℕ), AddSemiconjBy a (n • x) (n • y)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.orderIsoRpow.eq_1 : ∀ (y : ℝ) (hy : 0 < y),
  ENNReal.orderIsoRpow y hy = StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_get_bind : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s : σ) (f : σ → m α),
  (do
      set s
      let s' ← get
      f s') =
    do
    set s
    f s
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instInhabited : {α : Type u} → [inst : AddMonoid α] → Inhabited (AddConjClasses α)
-- Mathlib.Data.Set.Basic
Set.inter_ofPred_eq_sep : ∀ {α : Type u} (s : Set α) (p : α → Prop), s ∩ {a | p a} = {a | a ∈ s ∧ p a}
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString_eq.match_1_4.splitter : (motive : Option String → String → Sort u_1) →
  (x : Option String) →
    (x_1 : String) → ((sl : String) → motive none sl) → ((str sl : String) → motive (some str) sl) → motive x x_1
-- Mathlib.Order.Filter.Prod
Filter.Eventually.diag_of_prod_left : ∀ {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop},
  (∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.equivMatrix_symm_apply_ringCon : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n] (J : TwoSidedIdeal (Matrix n n R)),
  (TwoSidedIdeal.equivMatrix.symm J).ringCon = J.ringCon.ofMatrix
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.IsTwoBlockDiagonal.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α]
  (A : Matrix (n ⊕ o) (l ⊕ m) α), A.IsTwoBlockDiagonal = (A.toBlocks₁₂ = 0 ∧ A.toBlocks₂₁ = 0)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Reindexing a simplex along an `Equiv` of index types does not change the circumsphere.  -/
Affine.Simplex.circumsphere_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).circumsphere = s.circumsphere