mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.LazyDiscrTree
/-- Create a discriminator tree for imported environment.  -/
Lean.Meta.LazyDiscrTree.createImportedDiscrTree : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [Lean.MonadLog m] →
        [Lean.AddMessageContext m] →
          [Lean.MonadOptions m] →
            [MonadLiftT BaseIO m] →
              Lean.Core.Context →
                Lean.NameGenerator →
                  Lean.Environment →
                    (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
                      optParam ℕ 1000 → m (Lean.Meta.LazyDiscrTree α)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.TreeMap.minEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Option (α × β)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (p : Fin n → Polynomial R),
  (∀ (i : Fin n), (p i).natDegree = ↑i) →
    (∀ (i : Fin n), (p i).Monic) → (Matrix.vandermonde v).det = (Matrix.of fun i j => Polynomial.eval (v i) (p j)).det
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.union_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Mathlib.Data.Complex.Basic
Complex.star_def : star = ⇑(starRingEnd ℂ)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.rightHomologyData_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.rightHomologyData.H = 0
-- Mathlib.Algebra.Algebra.Hom.Rat
/-- The equivalence between `RingHom` and `ℚ`-algebra homomorphisms.  -/
RingHom.equivRatAlgHom : (R : Type u_1) →
  (S : Type u_2) →
    [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Algebra ℚ R] → [inst_3 : Algebra ℚ S] → (R →+* S) ≃ (R →ₐ[ℚ] S)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommAlgCat R), (CategoryTheory.forget (CommAlgCat R)).obj A = ↑A
-- Mathlib.Data.Set.Lattice
Set.sInter_eq_univ : ∀ {α : Type u_1} {S : Set (Set α)}, ⋂₀ S = Set.univ ↔ ∀ s ∈ S, s = Set.univ
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (N : ℕ),
  Polynomial.reflect N (Polynomial.C r) = Polynomial.C r * Polynomial.X ^ N
-- Lean.Meta.Tactic.Grind.Types
/-- Sources for `grind.ematch.diagnostics` that generated this instance.  -/
Lean.Meta.Grind.DelayedTheoremInstance.sources : Lean.Meta.Grind.DelayedTheoremInstance → List Lean.Meta.Grind.EMatchDiagNode
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_0_ne_zero : ∀ (R : Type u_1) [inst : CommRing R] [CharZero R] (n ν : ℕ),
  ν ≤ n → Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0
-- Init.Control.Lawful.Instances
ExceptT.ext : ∀ {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ExceptT ε m α}, x.run = y.run → x = y
-- Mathlib.Algebra.Group.Units.Defs
isUnit_of_mul_isUnit_right : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {x y : M}, IsUnit (x * y) → IsUnit y
-- Mathlib.Order.Bounds.Basic
isLUB_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsLUB s a → (a ≤ b ↔ b ∈ upperBounds s)
-- Std.Sync.CancellationToken
Std.CancellationToken.state : Std.CancellationToken → Std.Mutex Std.CancellationToken.State
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.instInhabited : {G : Type u_1} → {X : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → Inhabited (DiscreteTiling.Prototile G X)
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instRightDistribClass : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [RightDistribClass R], RightDistribClass Rᵒᵈ
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.det_fromBlocks_one₁₁ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α),
  (Matrix.fromBlocks 1 B C D).det = (D - C * B).det
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.oreDiv_add_char' : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] {r r' : X} (s s' : ↥S) (rb sb : R),
  sb * ↑s = rb * ↑s' → ∀ (h' : sb * ↑s ∈ S), r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.distinguished_cocone_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₃] {X Y : C} (a : X ⟶ Y),
  P X →
    P Y →
      ∃ Z,
        ∃ (_ : P Z),
          ∃ b c,
            CategoryTheory.Pretriangulated.Triangle.mk a b c ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ) (x : R),
  (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n)) =
    (2 * ↑k + 3) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The carrier set is closed under scalar multiplication.  -/
SubMulAction.smul_mem' : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
  x ∈ self.carrier → c • x ∈ self.carrier
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLEGE a b h).map φ).hom₃ = (t.truncGE b).map φ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.instInhabited : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → Inhabited v.Completion
-- Mathlib.Data.Nat.Count
Nat.count_le : ∀ (p : ℕ → Prop) [inst : DecidablePred p] {n : ℕ}, Nat.count p n ≤ n
-- Std.Tactic.Do.Syntax
/-- Like `intro`, but introducing stateful hypotheses into the stateful context of the `Std.Do.SPred`
proof mode.
That is, given a stateful goal `(hᵢ : Hᵢ)* ⊢ₛ P → T`, `mintro h` transforms
into `(hᵢ : Hᵢ)*, (h : P) ⊢ₛ T`.

Furthermore, `mintro ∀s` is like `intro s`, but preserves the stateful goal.
That is, `mintro ∀s` brings the topmost state variable `s:σ` in scope and transforms
`(hᵢ : Hᵢ)* ⊢ₛ T` (where the entailment is in `Std.Do.SPred (σ::σs)`) into
`(hᵢ : Hᵢ s)* ⊢ₛ T s` (where the entailment is in `Std.Do.SPred σs`).

Beyond that, `mintro` supports the full syntax of `mcases` patterns
(`mintro pat = (mintro h; mcases h with pat`), and can perform multiple
introductions in sequence.
 -/
Lean.Parser.Tactic.mintro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderBraiding.toIsMonoidalStable : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {P : CategoryTheory.MorphismProperty C} [self : P.IsStableUnderBraiding],
  P.IsMonoidalStable
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.eq_def : ∀ (x : Substring.Raw) (x_1 : ℕ) (x_2 : String.Pos.Raw),
  x.nextn x_1 x_2 =
    match x, x_1, x_2 with
    | x, 0, p => p
    | ss, i.succ, p => ss.nextn i (ss.next p)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.id_appTop : ∀ {X : AlgebraicGeometry.Scheme},
  AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.homMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f f_1 : A.X ⟶ B.X) (e_f : f = f_1) [inst_2 : CategoryTheory.IsMonHom f],
  CategoryTheory.Grp.homMk f = CategoryTheory.Grp.homMk f_1
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion at `x` is `C^n` at `x`.  -/
Manifold.IsImmersionAt.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAt I J n f x → ContMDiffAt I J n f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.union_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF), m₁.Equiv m₂ → (m₁.union m₃ ⋯ ⋯).Equiv (m₂.union m₃ ⋯ ⋯)
-- Mathlib.Data.Num.Lemmas
Num.add_ofNat' : ∀ (m n : ℕ), Num.ofNat' (m + n) = Num.ofNat' m + Num.ofNat' n
-- Mathlib.Topology.Defs.Sequences
/-- In a sequential space, a sequentially closed set is closed.  -/
IsSeqClosed.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SequentialSpace X] {s : Set X}, IsSeqClosed s → IsClosed s
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionSemiHomClass.toAddActionHom.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {F : Type u_8} [inst_2 : FunLike F X Y] [inst_3 : AddActionSemiHomClass F φ X Y] (f : F),
  ↑f = { toFun := ⇑f, map_vadd' := ⋯ }
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.ext_aux : ∀ {F : PFunctor.{uA, uB}} [inst : Inhabited F.M] [inst_1 : DecidableEq F.A] {n : ℕ} (x y z : F.M),
  PFunctor.M.Agree' n z x →
    PFunctor.M.Agree' n z y →
      (∀ (ps : PFunctor.Approx.Path F), n = List.length ps → PFunctor.M.iselect ps x = PFunctor.M.iselect ps y) →
        x.approx (n + 1) = y.approx (n + 1)
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- Returns `true` if `e` is an application that is a projection to a parent structure.
If `explicit` is `true`, then requires that the structure have no parameters.
 -/
Lean.PrettyPrinter.Delaborator.isParentProj : Bool → Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- **Alias** of `Ideal.hasFiniteMulSupport`.

---

For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^(val_v(I))` is not the unit ideal.  -/
Ideal.finite_mulSupport : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 → Function.HasFiniteMulSupport fun v => v.maxPowDividing I
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lieIdeal_oper_eq_span : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N⁆ = LieSubmodule.lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
-- Init.Data.Vector.Lemmas
Vector.allM_congr : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {xs ys : Vector α n},
  xs = ys → ∀ {p q : α → m Bool}, (∀ (a : α), p a = q a) → Vector.allM p xs = Vector.allM q ys
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainCoeff_chainTopIdx_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainBotCoeff i (RootPairing.chainTopIdx i j) =
      RootPairing.chainBotCoeff i j + RootPairing.chainTopCoeff i j ∧
    RootPairing.chainTopCoeff i (RootPairing.chainTopIdx i j) = 0
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sdiff_eq_sUnion' : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C → ∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I
-- Mathlib.Data.Matrix.PEquiv
PEquiv.transpose_toMatrix_toPEquiv_apply : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
  [inst_3 : One α] (f : m ≃ n) (j : n), f.toPEquiv.toMatrix.transpose j = Pi.single (f.symm j) 1
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_option' : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {x : V},
  (LinearIndependent K fun o => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.mk₀_comp_extMk : ∀ {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 : ℕ}
  (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0)
  {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {g : X' ⟶ X} (φ : R'.Hom R g),
  (CategoryTheory.Abelian.Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ =
    R'.extMk (CategoryTheory.CategoryStruct.comp (φ.hom.f n) f) m hm ⋯
-- Mathlib.Algebra.Ring.SumsOfSquares
_private.Mathlib.Algebra.Ring.SumsOfSquares.0.Submonoid.square_subsemiringClosure : ∀ {T : Type u_2} [inst : CommSemiring T], (Submonoid.square T).subsemiringClosure = Subsemiring.closure {x | IsSquare x}
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] {c : ℕ → 𝕜} {n : ℕ}, c n = 0 → FormalMultilinearSeries.ofScalars E c n = 0
-- Mathlib.Order.UpperLower.Closure
coe_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), ↑(upperClosure s) = ⋃ a ∈ s, Set.Ici a
-- Mathlib.Analysis.Convex.Between
Sbtw.ne_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Sbtw R x y z → y ≠ x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.hom_ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'},
  θ.left = θ'.left → θ.right = θ'.right → θ.base = θ'.base → θ = θ'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproduct.bicone_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).snd = CategoryTheory.Limits.biprod.snd
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIci a ↔ a ≤ x`  -/
LocallyFiniteOrderTop.finset_mem_Ici : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrderTop α] (a x : α),
  x ∈ LocallyFiniteOrderTop.finsetIci a ↔ a ≤ x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a more convenient formulation to show that a `KernelFork` of the form
`KernelFork.ofι i _` is a limit cone when we know that `i` is a monomorphism.  -/
CategoryTheory.Limits.KernelFork.IsLimit.ofι' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y K : C} →
        {f : X ⟶ Y} →
          (i : K ⟶ X) →
            (w : CategoryTheory.CategoryStruct.comp i f = 0) →
              ({A : C} →
                  (k : A ⟶ X) →
                    CategoryTheory.CategoryStruct.comp k f = 0 → { l // CategoryTheory.CategoryStruct.comp l i = k }) →
                [hi : CategoryTheory.Mono i] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w)
-- Mathlib.Tactic.Polynomial.Core
Mathlib.Tactic.Polynomial.PolynomialExt.mk.sizeOf_spec : ∀ (infer : Lean.Expr → Lean.MetaM Lean.Expr), sizeOf { infer := infer } = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.reverseEquiv.symm a = CliffordAlgebra.reverse a
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.Functor.inv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_2 : F.IsEquivalence], F.inv = F_1.inv
-- Init.Meta.Defs
Lean.isIdEndEscape : Char → Bool
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
FundamentalGroup.map_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (x : X)
  (a : { as := x } ⟶ { as := x }), (FundamentalGroup.map f x) a = Path.Homotopic.Quotient.map a f
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_top : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  ⊤.spanRank = p.spanRank
-- Mathlib.Order.ModularLattice
infIccOrderIsoIccSup.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α),
  infIccOrderIsoIccSup a b = infIccOrderIsoIccSup a b
-- Mathlib.Algebra.Group.Embedding
addLeftEmbedding_eq_addRightEmbedding : ∀ {G : Type u_1} [inst : AddCommMagma G] [inst_1 : IsCancelAdd G] (g : G), addLeftEmbedding g = addRightEmbedding g
-- Mathlib.Topology.UniformSpace.Basic
uniformity_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  uniformity (α × β) =
    Filter.comap (fun p => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (uniformity β)
-- Mathlib.Order.CountableSupClosed
/-- Every set generates a set closed under countable infimum.  -/
countableInfClosure : {α : Type u_2} → [Preorder α] → ClosureOperator (Set α)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_lift_OptionT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε α : Type u} {x : OptionT m α} {h : ε → OptionT m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} sh)} [inst : Std.Do.WP m sh] [Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)
-- Mathlib.Topology.Separation.Regular
/-- **Alias** of the reverse direction of `t5Space_iff_forall_t4Space`.

---

A space is `T5Space` iff it is hereditarily `T4Space`.
 -/
T5Space.of_forall_t4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), T4Space ↑s) → T5Space X
-- Mathlib.Logic.Equiv.Defs
Equiv.exists_subtype_congr : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : { a // p a } ≃ { b // q b }), (∃ a, p a) ↔ ∃ b, q b
-- Mathlib.Analysis.Normed.Ring.TransferInstance
/-- Transfer a `SeminormedRing` across an `Equiv`  -/
Equiv.seminormedRing : {α : Type u_1} → {β : Type u_2} → [SeminormedRing β] → α ≃ β → SeminormedRing α
-- Mathlib.Algebra.Category.Grp.Limits
/-- A choice of limit cone for a functor into `CommGrpCat`.
(Generally, you'll just want to use `limit F`.)  -/
CommGrpCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubMulAction.ofStabilizer.isPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [MulAction.IsPretransitive G α] {a b : α},
  MulAction.IsPretransitive ↥(MulAction.stabilizer G a) ↥(SubMulAction.ofStabilizer G a) ↔
    MulAction.IsPretransitive ↥(MulAction.stabilizer G b) ↥(SubMulAction.ofStabilizer G b)
-- Mathlib.FieldTheory.AxGrothendieck
/-- A special case of the **Ax-Grothendieck** theorem

Any injective polynomial map `K^n → K^n` is also surjective if `K` is an
algebraically closed field.  -/
ax_grothendieck_univ : ∀ {K : Type u_1} {ι : Type u_2} [inst : Field K] [IsAlgClosed K] [Finite ι] (p : ι → MvPolynomial ι K),
  (Function.Injective fun v i => (MvPolynomial.eval v) (p i)) →
    Function.Surjective fun v i => (MvPolynomial.eval v) (p i)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.isEmpty_bot : ∀ (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], IsEmpty ↥⊥
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.finitePresentation : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmooth R S], Algebra.FinitePresentation R S
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrHyp.mk.inj : ∀ {lhsIdx rhsIdx hypIdx : ℕ} {hypsPos : List (Option ℕ)} {isContra : Bool} {lhsIdx_1 rhsIdx_1 hypIdx_1 : ℕ}
  {hypsPos_1 : List (Option ℕ)} {isContra_1 : Bool},
  { lhsIdx := lhsIdx, rhsIdx := rhsIdx, hypIdx := hypIdx, hypsPos := hypsPos, isContra := isContra } =
      { lhsIdx := lhsIdx_1, rhsIdx := rhsIdx_1, hypIdx := hypIdx_1, hypsPos := hypsPos_1, isContra := isContra_1 } →
    lhsIdx = lhsIdx_1 ∧ rhsIdx = rhsIdx_1 ∧ hypIdx = hypIdx_1 ∧ hypsPos = hypsPos_1 ∧ isContra = isContra_1
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
Std.IterM.Intermediate.zip.eq_1 : ∀ {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α₁ m β₁] (it₁ : Std.IterM m β₁)
  (memo : Option { out // ∃ it, it.IsPlausibleOutput out }) (it₂ : Std.IterM m β₂),
  Std.IterM.Intermediate.zip it₁ memo it₂ = { internalState := { left := it₁, memoizedLeft := memo, right := it₂ } }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.forget_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  (CategoryTheory.Limits.Cone.forget F).map f = f.hom