mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
/-- The functor `X ↦ FreeNonUnitalNonAssocAlgebra R X` from the category of types to the
category of non-unital, non-associative algebras over `R` is adjoint to the forgetful functor in the
other direction.  -/
FreeNonUnitalNonAssocAlgebra.lift : (R : Type u_1) →
  {X : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [IsScalarTower R A A] → [SMulCommClass R A A] → (X → A) ≃ (FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A)
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.match_1.eq_2 : ∀ (motive : List Char → Sort u_1) (c : Char) (cs : List Char) (h_1 : Unit → motive [])
  (h_2 : (c : Char) → (cs : List Char) → motive (c :: cs)),
  (match c :: cs with
    | [] => h_1 ()
    | c :: cs => h_2 c cs) =
    h_2 c cs
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.length_pos : ∀ {n : ℕ} (c : OrderedFinpartition n), 0 < n → 0 < c.length
-- Mathlib.NumberTheory.PrimeCounting
/-- The cardinality of the finset `primesBelow n` equals the counting function
`primeCounting'` at `n`.  -/
Nat.primesBelow_card_eq_primeCounting' : ∀ (n : ℕ), n.primesBelow.card = n.primeCounting'
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_const_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal),
  ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ ≤ c * μ s
-- Mathlib.Algebra.BigOperators.Finprod
finsum_comp_equiv : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (e : α ≃ β) {f : β → M},
  ∑ᶠ (i : α), f (e i) = ∑ᶠ (i' : β), f i'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_toList : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {p : α → β → Bool},
  ((Std.DHashMap.Raw.Const.toList ↑m).all fun x => p x.1 x.2) = (↑m).all p
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α}, a ∉ ∅
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams : Type
-- Mathlib.Algebra.Regular.SMul
/-- An `M`-regular element is an element `c` such that multiplication on the left by `c` is an
injective map `M → M`.  -/
IsSMulRegular : {R : Type u_1} → (M : Type u_3) → [SMul R M] → R → Prop
-- Mathlib.Data.ENat.Basic
/-- Homomorphism from `ℕ∞` to `ℕ` sending `∞` to `0`.  -/
ENat.toNatHom : ℕ∞ →*₀ ℕ
-- Mathlib.FieldTheory.Normal.Closure
/-- `L/F` is a normal closure of `K/F` if the minimal polynomial of every element of `K` over `F`
splits in `L`, and `L` is generated by roots of such minimal polynomials over `F`.
(Since the minimal polynomial of a transcendental element is 0,
the normal closure of `K/F` is the same as the normal closure over `F`
of the algebraic closure of `F` in `K`.)  -/
IsNormalClosure : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) → [inst : Field F] → [inst_1 : Field K] → [inst_2 : Field L] → [Algebra F K] → [Algebra F L] → Prop
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.extendComp`.

---

Extending a cocone by a composition is the same as extending the cone twice.  -/
CategoryTheory.Limits.Cocones.extendComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) →
            {X Y : C} →
              (g : s.pt ⟶ Y) → (f : Y ⟶ X) → s.extend (CategoryTheory.CategoryStruct.comp g f) ≅ (s.extend g).extend f
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.of_retract : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderRetracts] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g), P g → P f
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toOver_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.toOver.pt = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id c.pt)
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Irreducible.maximalIdeal_pow_eq_closedBall_pow : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K]
  [IsDiscreteValuationRing ↥(Valued.integer K)] {ϖ : ↥(Valued.integer K)},
  Irreducible ϖ → ∀ (n : ℕ), ↑(Valued.maximalIdeal K ^ n) = Metric.closedBall 0 (‖ϖ‖ ^ n)
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.of_comp_left : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) {W : Type u_3} [inst_2 : Quiver W]
  (ψ : V ⥤q W), φ.IsCovering → (φ ⋙q ψ).IsCovering → Function.Surjective φ.obj → ψ.IsCovering
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (t : List (α × Bool)),
  FreeAddGroup.reduce t =
    List.rec []
      (fun hd1 _tl1 ih =>
        List.casesOn ih [hd1] fun hd2 tl2 => if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)
      t
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The morphism on `Localization W` that is induced by a left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        {X Y : C} →
          W.LeftFraction X Y →
            ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ⟶
              (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_commute_cfcₙ : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  Commute (cfcₙ f a) (cfcₙ g a)
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_lt_iff_slt : ∀ (a b : BitVec 8), Int8.ofBitVec a < Int8.ofBitVec b ↔ a.slt b = true
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.Quotient.commGroup.eq_1 : ∀ {G : Type u_5} [inst : CommGroup G] (N : Subgroup G),
  QuotientGroup.Quotient.commGroup N = { toGroup := QuotientGroup.Quotient.group N, mul_comm := ⋯ }
-- Mathlib.Data.Quot
Trunc.eq : ∀ {α : Sort u_1} (a b : Trunc α), a = b
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.inf_mul : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I J K : Ideal A), (I ⊓ J) * K = I * K ⊓ J * K
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- [Stacks Tag 0DVA](https://stacks.math.columbia.edu/tag/0DVA) -/
AlgebraicGeometry.isSeparated_of_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Function.Injective ⇑f → AlgebraicGeometry.IsSeparated f
-- Mathlib.Data.EReal.Operations
EReal.neg_sub : ∀ {x y : EReal}, x ≠ ⊥ ∨ y ≠ ⊥ → x ≠ ⊤ ∨ y ≠ ⊤ → -(x - y) = -x + y
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_Prop : Cardinal.mk Prop = 2
-- Lean.Meta.Basic
/-- Local instances in `lctx`.  -/
Lean.Meta.Context.localInstances : Lean.Meta.Context → Lean.LocalInstances
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α} {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.compatiblePreservingOfDownwardsClosed : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (K : CategoryTheory.GrothendieckTopology D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful]
  (hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)), CategoryTheory.CompatiblePreserving K F
-- Init.Data.String.Lemmas.Iterate
String.toList_chars : ∀ {s : String}, s.chars.toList = s.toList
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.mk : Std.Mutex Std.BarrierState✝ → Std.Condvar → ℕ → Std.Barrier
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instInhabited : {E : Type u_3} → [inst : Group E] → [DecidableEq E] → Inhabited (GroupNorm E)
-- Mathlib.Analysis.Convex.Function
ConvexOn.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E]
  [inst_6 : Module 𝕜 β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β} {c : 𝕜},
  0 ≤ c → ConvexOn 𝕜 s f → ConvexOn 𝕜 s fun x => c • f x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_pow_of_log_le : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_finMulAntidiag_pi : ∀ (d n : ℕ), Squarefree n → (n.primeFactors.pi fun x => Finset.univ).card = (d.finMulAntidiag n).card
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.verticesSet_nil : ∀ {V : Type u_1} [inst : Quiver V] {a : V}, {v | v ∈ Quiver.Path.nil.vertices} = {a}
-- Init.Data.List.Lemmas
List.foldr_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → List β} {g : β → γ → γ} {l : List α} {init : γ},
  List.foldr g init (List.flatMap f l) = List.foldr (fun x acc => List.foldr g acc (f x)) init l
-- Mathlib.Computability.DFA
DFA.comap_accept : ∀ {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ), (DFA.comap f M).accept = M.accept
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.map.eq_1 : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V},
  SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
-- Mathlib.Data.Finset.Card
Finset.three_lt_card_iff : ∀ {α : Type u_1} {s : Finset α},
  3 < s.card ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_rng_of_bot : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {X : Type u_3}
  [inst_1 : TopologicalSpace X] {f : X → RestrictedProduct (fun i => R i) (fun i => A i) ⊥},
  Continuous f ↔ Continuous (DFunLike.coe ∘ f)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_eq_zero : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, Metric.coveringNumber ε A = 0 ↔ A = ∅
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ofRingEquiv_dpow_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) {n : ℕ} {a : A},
  (DividedPowers.ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂},
  x = y ↔ x.τ₁ = y.τ₁ ∧ x.τ₂ = y.τ₂ ∧ x.τ₃ = y.τ₃ ∧ x.τ₄ = y.τ₄
-- Init.Data.Vector.Lemmas
Vector.getElem_set! : ∀ {α : Type u_1} {n j i : ℕ} {xs : Vector α n} {x : α} (hj : j < n), (xs.set! i x)[j] = if i = j then x else xs[j]
-- Mathlib.Algebra.Field.Subfield.Basic
/-- A field is finitely generated if it is the closure of a finite subset.  -/
Field.FG : (L : Type v) → [DivisionRing L] → Prop
-- Init.Data.Int.Order
Int.not_lt : ∀ {a b : ℤ}, ¬a < b ↔ b ≤ a
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Presheaf.IsSheaf.section_ext : ∀ {X : TopCat} {A : Type u_1} [inst : CategoryTheory.Category.{u, u_1} A] {FC : A → A → Type u_2} {CC : A → Type u}
  [inst_1 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory A FC]
  [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [(CategoryTheory.forget A).ReflectsIsomorphisms] {F : TopCat.Presheaf A X},
  F.IsSheaf →
    ∀ {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {s t : CategoryTheory.ToType (F.obj U)},
      (∀ x ∈ Opposite.unop U,
          ∃ V,
            ∃ (hV : V ≤ Opposite.unop U),
              x ∈ V ∧
                (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) s =
                  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) t) →
        s = t
-- Init.Prelude
/-- This function will cast a value of type `α` to type `β`, and is a no-op in the
compiler. This function is **extremely dangerous** because there is no guarantee
that types `α` and `β` have the same data representation, and this can lead to
memory unsafety. It is also logically unsound, since you could just cast
`True` to `False`. For all those reasons this function is marked as `unsafe`.

It is implemented by lifting both `α` and `β` into a common universe, and then
using `cast (lcProof : ULift (PLift α) = ULift (PLift β))` to actually perform
the cast. All these operations are no-ops in the compiler.

Using this function correctly requires some knowledge of the data representation
of the source and target types. Some general classes of casts which are safe in
the current runtime:

* `Array α` to `Array β` where `α` and `β` have compatible representations,
  or more generally for other inductive types.
* `Quot α r` and `α`.
* `@Subtype α p` and `α`, or generally any structure containing only one
  non-`Prop` field of type `α`.
* Casting `α` to/from `NonScalar` when `α` is a boxed generic type
  (i.e. a function that accepts an arbitrary type `α` and is not specialized to
  a scalar type like `UInt8`).
 -/
unsafeCast : {α : Sort u} → {β : Sort v} → α → β
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.extend = ContinuousMap.IccExtend ContinuousMap.Homotopy.extend._proof_1 F.curry
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) (s : ↑(Y.presheaf.obj (Opposite.op V))),
  X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f V U e)) s) =
    U ⊓ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen s)
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (x x_1 : R) (e_x : x = x_1) (B : Type u_2) [inst_1 : CommSemiring B]
  [inst_2 : Algebra R B] [inst_3 : IsLocalization.Away x B] (m m_1 : ℤ), m = m_1 → selfZPow x B m = selfZPow x_1 B m_1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.uniformity_eq_aux : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A],
  uniformity (CStarMatrix m n A) = uniformity (CStarMatrix m n A)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.natGeneratingSequence.congr_simp : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (a a_1 : ℕ),
  a = a_1 →
    ∀ (a_2 a_3 : α),
      a_2 = a_3 → MeasurableSpace.natGeneratingSequence α a a_2 = MeasurableSpace.natGeneratingSequence α a_1 a_3
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.lowerSemicontinuousAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → y ≤ 0 → LowerSemicontinuousAt (s.indicator fun _x => y) x
-- Mathlib.Data.Set.BoolIndicator
Set.notMem_iff_boolIndicator : ∀ {α : Type u_1} (s : Set α) (x : α), x ∉ s ↔ s.boolIndicator x = false
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s t : Set E}
  {x v : E}, LineDifferentiableWithinAt 𝕜 f t x v → s ⊆ t → LineDifferentiableWithinAt 𝕜 f s x v
-- Std.Http.Internal.Char
/-- RWS = 1*( SP / HTAB ) (character class is identical to `ows`)
 -/
Std.Http.Internal.Char.rws : Char → Bool
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerCongr_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (e : G ≃+ H)
  (r : ↥(AddSubsemigroup.center G)), ↑((AddSubgroup.centerCongr e) r) = e ↑r
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A]
  [CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.Sheaf.locallySurjective J A).HasFunctorialFactorization (CategoryTheory.Sheaf.locallyInjective J A)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
integralClosure_le_completeIntegralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsFractionRing R S],
  integralClosure R S ≤ completeIntegralClosure R S
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.mk.inj : ∀ {toState : Lean.Doc.State}
  {scopedExts : Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState)}
  {toState_1 : Lean.Doc.State}
  {scopedExts_1 : Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState)},
  { toState := toState, scopedExts := scopedExts } = { toState := toState_1, scopedExts := scopedExts_1 } →
    toState = toState_1 ∧ scopedExts = scopedExts_1
-- Mathlib.Topology.Category.Locale
Locale.instInhabited : Inhabited Locale
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {b : R}, p.leadingCoeff * b = 1 → (p * Polynomial.C b).Monic
-- Mathlib.Data.Matrix.Mul
Matrix.instNonAssocRing : {n : Type u_3} → {α : Type v} → [Fintype n] → [DecidableEq n] → [NonAssocRing α] → NonAssocRing (Matrix n n α)
-- Mathlib.Analysis.Normed.Ring.Basic
PUnit.normedCommRing : NormedCommRing PUnit.{u_5 + 1}
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basis : {ι : Type u_3} →
  {s : Set (ι → ℕ)} →
    (hs : IsProperLinearSet s) → [inst : Finite ι] → Module.Basis ↑(IsProperLinearSet.basisSet✝ hs) ℚ (ι → ℚ)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_inf : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring R) (f : F),
  Function.Injective ⇑f →
    NonUnitalSubsemiring.map f (s ⊓ t) = NonUnitalSubsemiring.map f s ⊓ NonUnitalSubsemiring.map f t
-- Std.Data.DHashMap.RawLemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `get_insertIfNew`.  -/
Std.DHashMap.Raw.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.forall_coord_eq_zero_iff : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {x : M}, (∀ (i : ι), (b.coord i) x = 0) ↔ x = 0
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4) →
      (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        ((n : ℕ) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inr (Sum.inr n.succ.succ) :: l)) →
          ((n₁ : ℕ) →
              (t₁ : L.Term (α ⊕ Fin n₁)) →
                (n₂ : ℕ) →
                  (t₂ : L.Term (α ⊕ Fin n₂)) →
                    (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
                      motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l)) →
            ((n : ℕ) →
                (R : L.Relations n) →
                  (k : ℕ) →
                    (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
                      motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l)) →
              ((l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
                  motive (Sum.inr (Sum.inr 0) :: l)) →
                ((l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
                    motive (Sum.inr (Sum.inr 1) :: l)) →
                  ((x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
                      (∀ (n : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
                          x = Sum.inr (Sum.inr n.succ.succ) :: l → False) →
                        (∀ (n₁ : ℕ) (t₁ : L.Term (α ⊕ Fin n₁)) (n₂ : ℕ) (t₂ : L.Term (α ⊕ Fin n₂))
                            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
                            x = Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l → False) →
                          (∀ (n : ℕ) (R : L.Relations n) (k : ℕ)
                              (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
                              x = Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l → False) →
                            (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
                                x = Sum.inr (Sum.inr 0) :: l → False) →
                              (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
                                  x = Sum.inr (Sum.inr 1) :: l → False) →
                                motive x) →
                    motive x
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset : ∀ {α : Type u} [t : TopologicalSpace α] {B B' : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    (∀ u ∈ B', IsOpen u) → (∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u) → TopologicalSpace.IsTopologicalBasis B'
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instEtaleCarrierObjFiniteEtale : ∀ (R : Type u) [inst : CommRing R] (S : CommAlgCat.FiniteEtale R), Algebra.Etale R ↑S.obj