mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform isomorphism between dependent functions `Π i : Fin 2, α i` and `α 0 × α 1`.  -/
UniformEquiv.piFinTwo : (α : Fin 2 → Type u) → [inst : (i : Fin 2) → UniformSpace (α i)] → ((i : Fin 2) → α i) ≃ᵤ α 0 × α 1
-- Mathlib.Order.ModularLattice
instIsLowerModularLatticeOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α], IsLowerModularLattice αᵒᵈ
-- Mathlib.Algebra.GCDMonoid.Nat
Int.gcd_eq_natAbs : ∀ {a b : ℤ}, a.gcd b = a.natAbs.gcd b.natAbs
-- Mathlib.Topology.Defs.Sequences
SequentialSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), IsSeqClosed s → IsClosed s) → SequentialSpace X
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_fun_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M], (Function.mulSupport fun x => 1) = ∅
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_sumElim_zero_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] (x : ι → K), Height.mulHeight (Sum.elim x 0) = Height.mulHeight x
-- Lean.Parser.Command
/-- Declares one or more universe variables.

`universe u v`

`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].

Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.

[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)

```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a

/- Implicit type-universe parameter, equivalent to `id₁`.
  Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a

/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```

On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.

```lean
def L₁.{u} := List (Type u)

-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`

universe u
def L₃ := List (Type u)
```

## Examples

```lean
universe u v w

structure Pair (α : Type u) (β : Type v) : Type (max u v) where
  a : α
  b : β

#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
 -/
Lean.Parser.Command.universe : Lean.Parser.Parser
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
denselyOrdered_units_iff : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] [Nontrivial αˣ], DenselyOrdered αˣ ↔ DenselyOrdered α
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isOpenImmersion_of_isEmpty : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↥X], AlgebraicGeometry.IsOpenImmersion f
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsVertexCover.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (c : Set V), G.IsVertexCover c = ∀ ⦃v w : V⦄, G.Adj v w → v ∈ c ∨ w ∈ c
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPushout_op_iff_hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.Limits.HasPushout f.op g.op ↔ CategoryTheory.Limits.HasPullback f g
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_smul : ∀ {𝕜 : 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 : ℕ} (r : 𝕜)
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F), (r • f).curryLeft = r • f.curryLeft
-- Std.Data.Internal.List.Associative
Std.Internal.List.size_filter_not_contains_map_fst_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).length +
        (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).length =
      l₁.length
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- **Alias** of `Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup`.

---

The alternating group is the closure of the set of permutations with cycle type (2, 2).  -/
Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → Subgroup.closure {g | g.cycleType = {2, 2}} = alternatingGroup α
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.empty_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), SeparatedNhds s ∅
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.card_ofPermHom_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)),
  (a.ofPermHom τ).support.card = ∑ c ∈ (↑τ).support, (↑c).support.card
-- Mathlib.Tactic.Widget.Conv
/-- Accesses the `arg`th implicit or explicit argument,
depending on whether `all` is `true` or `false`, respectively.
Corresponds to the `conv` tactic `arg`.
For example, `Path.arg 3 true next` is `arg @3` followed by `next`,
and `Path.arg 0 false next` is `arg 0` followed by `next`.
 -/
Mathlib.Tactic.Conv.Path.arg : ℕ → Bool → Mathlib.Tactic.Conv.Path → Mathlib.Tactic.Conv.Path
-- Init.Data.SInt.Bitwise
ISize.toBitVec_and : ∀ (a b : ISize), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- the identity map as a continuous linear map.  -/
ContinuousLinearMap.id : (R₁ : Type u_1) →
  [inst : Semiring R₁] →
    (M₁ : Type u_4) →
      [inst_1 : TopologicalSpace M₁] → [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → M₁ →L[R₁] M₁
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsPreLocalizingSequence.mk : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreLocalizingSequence._auto_1},
  (∀ (n : ℕ), MeasureTheory.IsStoppingTime 𝓕 (τ n)) →
    (∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun x => τ x ω) Filter.atTop (nhds ⊤)) →
      ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P
-- Mathlib.Data.Int.ModEq
Int.right_modEq_add_iff : ∀ {n a b : ℤ}, b ≡ a + b [ZMOD n] ↔ n ∣ a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_map_pi : ∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → NonUnitalRing (C i)]
  [inst_2 : (i : ι) → TopologicalSpace (C i)] [inst_3 : (i : ι) → StarRing (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Module ℝ (C i)] [inst_7 : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)]
  [inst_8 : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)]
  [inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint]
  [∀ (i : ι), IsSemitopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_14 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i},
  autoParam (∀ (i : ι), 0 ≤ c i) CFC.sqrt_map_pi._auto_1 → CFC.sqrt c = fun i => CFC.sqrt (c i)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.reachable_deleteEdges_iff_exists_walk`. -/
SimpleGraph.reachable_delete_edges_iff_exists_walk : ∀ {V : Type u} {G : SimpleGraph V} {v w v' w' : V}, (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ p, s(v, w) ∉ p.edges
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.Equivalent.trans : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂}
  {B₃ : LinearMap.BilinForm R M₃}, B₁.Equivalent B₂ → B₂.Equivalent B₃ → B₁.Equivalent B₃
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.of_injective : ∀ {α : Type u_1}, Function.Injective FreeAddMonoid.of
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_one : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ), x ^ (y + 1) = x ^ y * x
-- Std.Time.Time.PlainTime
/-- `Second` component of the `PlainTime`
 -/
Std.Time.PlainTime.second : Std.Time.PlainTime → Std.Time.Second.Ordinal true
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_image' : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), openSegment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Set.Ioo 0 1
-- Mathlib.CategoryTheory.Abelian.Transfer
/-- If `C` is an additive category equivalent to an abelian category `D`
via a functor that preserves zero morphisms,
then `C` is also abelian.
 -/
CategoryTheory.abelianOfEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [CategoryTheory.Abelian D] → (F : CategoryTheory.Functor C D) → [F.IsEquivalence] → CategoryTheory.Abelian C
-- Mathlib.Logic.Function.Basic
Function.Injective.extend_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (g : α → γ) (e' : β → γ) (a : α), Function.extend f g e' (f a) = g a
-- Lean.Meta.Tactic.Grind.Types
/-- Sequence of cases steps that generated this goal. We only use this information for diagnostics.
Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
applications that generated only 1 subgoal.
 -/
Lean.Meta.Grind.Split.State.trace : Lean.Meta.Grind.Split.State → List Lean.Meta.Grind.CaseTrace
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.le_cof_iff_blsub : ∀ {b : Ordinal.{u}} {a : Cardinal.{u}},
  a ≤ b.cof ↔ ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
-- Mathlib.Topology.Separation.Hausdorff
IsCompact.inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s t : Set X}, IsCompact s → IsCompact t → IsCompact (s ∩ t)
-- Mathlib.Algebra.Group.Action.Hom
AddMonoidHom.vaddZeroHom_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddZeroClass N] [inst_2 : AddAction M N]
  [inst_3 : VAddAssocClass M N N] (x : M), AddMonoidHom.vaddZeroHom x = x +ᵥ 0
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instPow.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Monoid N],
  OneHom.instPow = { pow := fun f n => { toFun := ⇑f ^ n, map_one' := ⋯ } }
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.thmNames : Lean.Compiler.CSimp.State → Lean.SSet Lean.Name
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α} (h' : a ∈ m),
  m.get? a = some (m.get a h')
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.mk.inj : ∀ {toMatcherInfo : Lean.Meta.MatcherInfo} {matcherName : Lean.Name} {matcherLevels : Array Lean.Level}
  {params : Array Lean.Expr} {motive : Lean.Expr} {discrs alts remaining : Array Lean.Expr}
  {toMatcherInfo_1 : Lean.Meta.MatcherInfo} {matcherName_1 : Lean.Name} {matcherLevels_1 : Array Lean.Level}
  {params_1 : Array Lean.Expr} {motive_1 : Lean.Expr} {discrs_1 alts_1 remaining_1 : Array Lean.Expr},
  { toMatcherInfo := toMatcherInfo, matcherName := matcherName, matcherLevels := matcherLevels, params := params,
        motive := motive, discrs := discrs, alts := alts, remaining := remaining } =
      { toMatcherInfo := toMatcherInfo_1, matcherName := matcherName_1, matcherLevels := matcherLevels_1,
        params := params_1, motive := motive_1, discrs := discrs_1, alts := alts_1, remaining := remaining_1 } →
    toMatcherInfo = toMatcherInfo_1 ∧
      matcherName = matcherName_1 ∧
        matcherLevels = matcherLevels_1 ∧
          params = params_1 ∧ motive = motive_1 ∧ discrs = discrs_1 ∧ alts = alts_1 ∧ remaining = remaining_1
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_neg : ∀ {x : ℝ}, Irrational (-x) → Irrational x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α}
  {h' : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.DistinctKeys l →
    ∀ (h : l.Perm l'), Std.Internal.List.getValue a l h' = Std.Internal.List.getValue a l' ⋯
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (hc : CategoryTheory.Limits.IsColimit c) {j₀ : J} {y : X ⟶ Y.obj j₀},
  CategoryTheory.CategoryStruct.comp y (c.ι.app j₀) = 0 →
    ∀ [CategoryTheory.IsFiltered J],
      CategoryTheory.Epi (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f y)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.toFun.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g), rTensor.toFun Q hfg = (LinearMap.rTensor Q f).range.liftQ (LinearMap.rTensor Q g) ⋯
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The subgroup `G` of the group `G`.  -/
Subgroup.instTop : {G : Type u_1} → [inst : Group G] → Top (Subgroup G)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsGood.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P P_1 : HomotopicalAlgebra.Cylinder A),
  P = P_1 →
    ∀ [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C],
      P.IsGood = P_1.IsGood
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_union : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α]
  [inst_3 : DecidableEq α],
  a ∈ lowerClosure ↑s → a ∈ lowerClosure ↑t → (s ∪ t).truncatedSup a = s.truncatedSup a ⊔ t.truncatedSup a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {combined lw rw : ℕ} →
          aig.RefVec lw →
            aig.RefVec rw → combined = rw + lw → Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is a slightly more convenient method to verify that a trident is a limit cone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.Trident.IsLimit.mk : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Trident f) →
              (lift : (s : CategoryTheory.Limits.Trident f) → s.pt ⟶ t.pt) →
                (∀ (s : CategoryTheory.Limits.Trident f), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) →
                  (∀ (s : CategoryTheory.Limits.Trident f) (m : s.pt ⟶ t.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
                          CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) →
                        m = lift s) →
                    CategoryTheory.Limits.IsLimit t
-- Mathlib.Algebra.Category.MonCat.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
CommMonCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Fin.Fin2
Fin2.fs.inj : ∀ {n : ℕ} {a a_1 : Fin2 n}, a.fs = a_1.fs → a = a_1
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atBot_eq_generate_Iic : ∀ {α : Type u_3} [inst : Preorder α], Filter.atBot = Filter.generate (Set.range Set.Iic)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.notMem_of_notMem_closure : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {P : R}, P ∉ Subring.closure s → P ∉ s
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle the action of `C` on `D` as a functor `C ⥤ D ⥤ D`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction : (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] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.Functor C (CategoryTheory.Functor D D)
-- Mathlib.Algebra.Algebra.Unitization
/-- **Alias** of the forward direction of `Unitization.isStarProjection_inr_iff`. -/
IsStarProjection.of_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] {p : A}, IsStarProjection ↑p → IsStarProjection p
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.map_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R),
  (MvPolynomial.map f) ((MvPolynomial.rename g) p) = (MvPolynomial.rename g) ((MvPolynomial.map f) p)
-- Init.Data.Int.Lemmas
Int.sub_left_inj : ∀ {i j : ℤ} (k : ℤ), i - k = j - k ↔ i = j
-- Mathlib.Order.Sublocale
Sublocale.mk.injEq : ∀ {X : Type u_2} [inst : Order.Frame X] (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier)
  (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier) (carrier_1 : Set X)
  (sInf_mem'_1 : ∀ s ⊆ carrier_1, sInf s ∈ carrier_1) (himp_mem'_1 : ∀ (a b : X), b ∈ carrier_1 → a ⇨ b ∈ carrier_1),
  ({ carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } =
      { carrier := carrier_1, sInf_mem' := sInf_mem'_1, himp_mem' := himp_mem'_1 }) =
    (carrier = carrier_1)
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.RepresentablyCoflat (CategoryTheory.Functor.id C)
-- Mathlib.Topology.Separation.Regular
/-- If `closure s` is disjoint with `t`, and `s` is disjoint with `closure t`, then `s` and `t`
admit disjoint neighbourhoods.  -/
CompletelyNormalSpace.completely_normal : ∀ {X : Type u} {inst : TopologicalSpace X} [self : CompletelyNormalSpace X] ⦃s t : Set X⦄,
  Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Init.Data.SInt.Bitwise
Int64.toInt32_not : ∀ (a : Int64), (~~~a).toInt32 = ~~~a.toInt32
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (x : CategoryTheory.Bicategory.InducedBicategory C F),
  (CategoryTheory.Bicategory.InducedBicategory.forget.mapId x).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id (F x))
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w : ℕ} {vec : aig.RefVec w}
  {distance : ℕ} {vec_1 : aig.RefVec w} {distance_1 : ℕ},
  { vec := vec, distance := distance } = { vec := vec_1, distance := distance_1 } → vec = vec_1 ∧ distance = distance_1
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- The n-ary version of `Set.mem_mul`.  -/
Set.mem_finsetProd : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
  a ∈ ∏ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : DecidableRel G.Adj] (u v : V),
  G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_ext_iff : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {G F : CategoryTheory.Functor (CategoryTheory.Discrete I) C}, G = F ↔ ∀ (i : I), G.obj { as := i } = F.obj { as := i }
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_b_eq_one' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], { a := 0, b := 1, c := c, d := d }.toPoly.Monic
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.mk : {ι : Type u_1} → (faces : Set (Finset ι)) → IsRelLowerSet faces Finset.Nonempty → PreAbstractSimplicialComplex ι
-- Mathlib.Order.Monotone.Basic
/-- If `f` is a monotone function from `ℤ` to a preorder and `x` lies between `f n` and
`f (n + 1)`, then `x` doesn't lie in the range of `f`.  -/
Monotone.ne_of_lt_of_lt_int : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α},
  Monotone f → ∀ (n : ℤ) {x : α}, f n < x → x < f (n + 1) → ∀ (a : ℤ), f a ≠ x
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The bijection `X.op.S ≃ X.S`.  -/
SSet.S.opEquiv : {X : SSet} → X.op.S ≃ X.S
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.IsFinite.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {p : M.Presentation},
  autoParam p.generators.IsFiniteType SheafOfModules.Presentation.IsFinite.isFiniteType_generators._autoParam →
    autoParam p.relations.IsFiniteType SheafOfModules.Presentation.IsFinite.isFiniteType_relations._autoParam →
      p.IsFinite
-- Mathlib.Order.Filter.Germ.Basic
/-- Coercion from functions to germs as a monoid homomorphism.  -/
Filter.Germ.coeMulHom : {α : Type u_1} → {M : Type u_5} → [inst : Monoid M] → (l : Filter α) → (α → M) →* l.Germ M
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commGroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → CommGroup (f i)] → CommGroup ((i : I) → f i)