mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_ofHom : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (f : X →o Y), PartOrd.Hom.hom (PartOrd.ofHom f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.fst_eq_snd_of_mono_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.Limits.pullback.fst f f = CategoryTheory.Limits.pullback.snd f f
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A finite connected graph contains a vertex that leaves the graph preconnected if removed.  -/
SimpleGraph.Connected.exists_preconnected_induce_compl_singleton_of_finite : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V], G.Connected → ∃ v, (SimpleGraph.induce {v}ᶜ G).Preconnected
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.strictConvexOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConvexOn s φ f → (∀ (r : ℝ), r ≠ 0 → 0 < φ r) → StrictConvexOn ℝ s f
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.whiskerRight_apply : ∀ {R : Type u} [inst : CommRing R] {L M : ModuleCat R} (f : L ⟶ M) (N : ModuleCat R) (l : ↑L) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)) (l ⊗ₜ[R] n) =
    (CategoryTheory.ConcreteCategory.hom f) l ⊗ₜ[R] n
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying type.  -/
CommMonCat.carrier : CommMonCat → Type u
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.subtype_injective : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), Function.Injective ⇑s.subtype
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → Set.range ⇑(mfderiv% ↑e x) = Set.univ
-- Mathlib.Analysis.Convex.Basic
Convex.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ∩ t)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_eq_unbotD_withBotDegree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.degree f = WithBot.unbotD 0 (m.withBotDegree f)
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Colex.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LT ι] [Std.Trichotomous fun x1 x2 => x1 < x2] [WellFoundedLT ι]
  [inst_3 : (i : ι) → AddMonoid (α i)] [inst_4 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)]
  [∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Colex (Π₀ (i : ι), α i))
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt32HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.RepresentationTheory.Subrepresentation
/-- An `A[G]`-submodule of `ρ.asModule` can be thought of as a subrepresentation of `ρ`.
 -/
Subrepresentation.ofSubmodule' : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] →
              {ρ : Representation A G W} → Submodule (MonoidAlgebra A G) ρ.asModule → Subrepresentation ρ
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_prod_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Module.Free R S] [Module.Free R T] [Module.Finite R S]
  [Module.Finite R T] (x : S × T), (Algebra.trace R (S × T)) x = (Algebra.trace R S) x.1 + (Algebra.trace R T) x.2
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.mor.injEq : ∀ (thm thm_1 : Mathlib.Meta.FunProp.GeneralTheorem),
  (Mathlib.Meta.FunProp.Theorem.mor thm = Mathlib.Meta.FunProp.Theorem.mor thm_1) = (thm = thm_1)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_6} [inst : NormedAddCommGroup H]
  {f : α → H} {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)
-- Aesop.Script.Step
Aesop.Script.Step.validate : Aesop.Script.Step → Lean.MetaM Unit
-- Mathlib.Topology.Category.TopCat.EpiMono
TopCat.epi_iff_surjective : ∀ {X Y : TopCat} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_apply_univ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {i : Set α}, (v.restrict i) Set.univ = v i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGE_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂),
  Std.DTreeMap.Const.getEntryGE t₁ k h' = Std.DTreeMap.Const.getEntryGE t₂ k ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_back!_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.max! = t.toArray.back!
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.eq_of_bisim : ∀ {F : PFunctor.{uA, uB}} (R : F.M → F.M → Prop) [Nonempty F.M],
  PFunctor.M.IsBisimulation R → ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
-- Mathlib.Data.Fintype.Basic
/-- For functions on finite sets, they are bijections iff they map universes into universes.  -/
Multiset.bijective_iff_map_univ_eq_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Bijective f ↔ Multiset.map f Finset.univ.val = Finset.univ.val
-- Mathlib.Order.Defs.PartialOrder
/-- A preorder is a reflexive, transitive relation `≤`.
In a preorder, `a < b` means `a ≤ b ∧ ¬b ≤ a`, and `<` is defined this way by default.
You can override this definition to set a better def-eq.
 -/
Preorder : Type u_2 → Type u_2
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.hasDerivWithinAt_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → (HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x)
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.zero_compl : ∀ {R : Type u_1} [inst : NonAssocRing R], 0ᶜ = 1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.recOnSubsingleton₂.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {r : AddLocalization S → AddLocalization S → Sort u}
  [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (AddLocalization.mk a b) (AddLocalization.mk c d))]
  (x y : AddLocalization S) (f : (a c : M) → (b d : ↥S) → r (AddLocalization.mk a b) (AddLocalization.mk c d)),
  x.recOnSubsingleton₂ y f =
    Quotient.recOnSubsingleton₂' x y fun t =>
      Prod.rec (motive := fun x => (a₂ : M × ↥S) → r (Quotient.mk'' x) (Quotient.mk'' a₂))
        (fun x x_1 t => Prod.rec (fun x_2 x_3 => f x x_2 x_1 x_3) t) t
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symm.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D),
  e.symm =
    { functor := e.inverse, inverse := e.functor, unitIso := e.counitIso.symm, counitIso := e.unitIso.symm,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.MvPolynomial.Rename
/-- `exists_finset_rename` for two polynomials at once: for any two polynomials `p₁`, `p₂` in a
polynomial semiring `R[σ]` of possibly infinitely many variables, `exists_finset_rename₂` yields
a finite subset `s` of `σ` such that both `p₁` and `p₂` are contained in the polynomial semiring
`R[s]` of finitely many variables.  -/
MvPolynomial.exists_finset_rename₂ : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p₁ p₂ : MvPolynomial σ R),
  ∃ s q₁ q₂, p₁ = (MvPolynomial.rename Subtype.val) q₁ ∧ p₂ = (MvPolynomial.rename Subtype.val) q₂
-- Mathlib.Combinatorics.Additive.CovBySMul
covBySMul_zero : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {A B : Set X}, CovBySMul M 0 A B ↔ A = ∅
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addETransformRight e x = (x.1 ∪ (AddOpposite.op e +ᵥ x.1), x.2 ∩ (-e +ᵥ x.2))
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G),
  (CategoryTheory.NatIso.unop α).hom = CategoryTheory.NatTrans.unop α.hom
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instInhabitedFunIndInfo.default : Lean.Meta.FunIndInfo
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).getKey? k = none
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- A version of the Freiman homomorphism condition expressed using `Finset`s,
for practicality.  -/
IsAddFreimanHom.sum_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ},
  IsAddFreimanHom n A B f →
    ∀ {s t : Finset α} {hsA : ↑s ⊆ A} {htA : ↑t ⊆ A},
      s.card = n → t.card = n → ∑ i ∈ s, i = ∑ i ∈ t, i → ∑ i ∈ s, f i = ∑ i ∈ t, f i
-- Mathlib.Data.Finset.Erase
Finset.erase_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {x y : α} (s : Finset α), x ∈ s → (s.erase x = s.erase y ↔ x = y)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_univ_ne_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ν Set.univ ≠ 0
-- Mathlib.Analysis.Normed.Field.Basic
DenselyNormedField.toNormedField : {α : Type u_5} → [self : DenselyNormedField α] → NormedField α
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_single_eq_coeff_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Add M]
  (m₂ : M),
  (∀ m' ∈ x.coeff.support, m' + m = m₁ ↔ m' = m₂) → (x * AddMonoidAlgebra.single m r).coeff m₁ = x.coeff m₂ * r
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_isTop : ∀ (α : Type u_1) [inst : PartialOrder α], {x | IsTop x}.Subsingleton
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- Hyperbolic distance between two points is greater than or equal to the distance between the
logarithms of their imaginary parts.  -/
UpperHalfPlane.dist_log_im_le : ∀ (z w : UpperHalfPlane), dist (Real.log z.im) (Real.log w.im) ≤ dist z w
-- Mathlib.RingTheory.Trace.Basic
/-- The dual basis of a basis under the trace form in a finite separable extension.
 -/
Module.Basis.traceDual : {K : Type u_4} →
  {L : Type u_5} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {ι : Type w} →
            [FiniteDimensional K L] →
              [Algebra.IsSeparable K L] → [Finite ι] → [DecidableEq ι] → Module.Basis ι K L → Module.Basis ι K L
-- Mathlib.Tactic.Eqns
eqns : Lean.ParserDescr
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.zsmul_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → ∀ (m n : ℤ), AddCommute (m • a) (n • b)
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.under_map_of_isPrimary_disjoint`. -/
IsLocalization.comap_map_of_isPrimary_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R},
  I.IsPrimary → Disjoint ↑M ↑I → Ideal.under R (Ideal.map (algebraMap R S) I) = I
-- Mathlib.Data.Matrix.Mul
Matrix.one_mul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (M : Matrix m n α), 1 * M = M
-- Mathlib.Order.LiminfLimsup
Filter.limsup_le_limsup_of_le : ∀ {α : Type u_6} {β : Type u_7} [inst : ConditionallyCompleteLattice β] {f g : Filter α},
  f ≤ g →
    ∀ {u : α → β},
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_limsup_of_le._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) g u) Filter.limsup_le_limsup_of_le._auto_3 →
          Filter.limsup u f ≤ Filter.limsup u g
-- Mathlib.Tactic.FunProp.FunctionData
/-- Is function body of `f` a morphism application? What kind?  -/
Mathlib.Meta.FunProp.FunctionData.isMorApplication : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM Mathlib.Meta.FunProp.MorApplication
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.spectrum_le : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A)
  ⦃x : NNReal⦄,
  x ∈ spectrum NNReal a → autoParam (0 ≤ a) IsometricContinuousFunctionalCalculus.spectrum_le._auto_1 → x ≤ ‖a‖₊
-- Mathlib.NumberTheory.SumFourSquares
Int.sq_add_sq_of_two_mul_sq_add_sq : ∀ {m x y : ℤ}, 2 * m = x ^ 2 + y ^ 2 → m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.to_rightInverse : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ {g : β → α}, Function.RightInverse g f → LipschitzWith K g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg c = Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg c_1) = (c = c_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.mk.inj : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {pt : C} {π : (j : J) → pt ⟶ F j}
  {ι : (j : J) → F j ⟶ pt}
  {ι_π :
    autoParam
      (∀ (j j' : J),
        CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
      CategoryTheory.Limits.Bicone.ι_π._autoParam}
  {pt_1 : C} {π_1 : (j : J) → pt_1 ⟶ F j} {ι_1 : (j : J) → F j ⟶ pt_1}
  {ι_π_1 :
    autoParam
      (∀ (j j' : J),
        CategoryTheory.CategoryStruct.comp (ι_1 j) (π_1 j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
      CategoryTheory.Limits.Bicone.ι_π._autoParam},
  { pt := pt, π := π, ι := ι, ι_π := ι_π } = { pt := pt_1, π := π_1, ι := ι_1, ι_π := ι_π_1 } →
    pt = pt_1 ∧ π ≍ π_1 ∧ ι ≍ ι_1
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.mkSimpTheoremFromExpr : Lean.Meta.Origin →
  Array Lean.Name →
    Lean.Expr →
      optParam Bool false →
        optParam Bool true →
          optParam ℕ 1000 →
            optParam Lean.Meta.ConfigWithKey Lean.Meta.simpGlobalConfig → Lean.MetaM (Array Lean.Meta.SimpTheorem)
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- A field is a valuation ring.  -/
ValuationRing.of_field : ∀ (K : Type u) [inst : Field K], ValuationRing K
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.equiv_unit : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SimplyConnectedSpace X],
  Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {outWidth : ℕ} →
        {aig : Std.Sat.AIG α} →
          {w : ℕ} →
            (idx : ℕ) →
              aig.RefVec w → aig.RefVec (w * idx) → idx ≤ w → outWidth = w * w → Std.Sat.AIG.RefVecEntry α outWidth
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instOne : {α : Type u_1} → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [One β] → One C(α, β)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H)
  (K : FiniteIndexNormalAddSubgroup H),
  FiniteIndexNormalAddSubgroup.comap f K =
    { toAddSubgroup := AddSubgroup.comap f K.toAddSubgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ }
-- Mathlib.Combinatorics.Colex
/-- **Alias** of `Finset.toFinset_bitIndices_sum_two_pow`. -/
Finset.toFinset_bitIndices_twoPowSum : ∀ (s : Finset ℕ), (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s
-- Init.Data.Option.Basic
/-- If `a ~ b`, then `some a ~ some b`  -/
Option.Rel.some : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β}, r a b → Option.Rel r (some a) (some b)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_le_left : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided], I * J ≤ I
-- Mathlib.Order.Bounds.Defs
IsGLB.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsGLB s = IsGreatest (lowerBounds s)
-- Mathlib.MeasureTheory.PiSystem
/-- Rectangles formed by π-systems form a π-system.  -/
IsPiSystem.prod : ∀ {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {D : Set (Set β)},
  IsPiSystem C → IsPiSystem D → IsPiSystem (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D)
-- Mathlib.Data.Set.Lattice
Set.iInter_of_empty : ∀ {α : Type u_1} {ι : Sort u_5} [IsEmpty ι] (s : ι → Set α), ⋂ i, s i = Set.univ
-- Init.Data.UInt.Bitwise
UInt32.neg_one_xor : ∀ {a : UInt32}, -1 ^^^ a = ~~~a
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (d d' : ℕ) → d = d' + 1 → motive (Int.ofNat d'.succ))
  (h_3 : (d : ℕ) → motive (Int.negSucc d)),
  (match 0 with
    | 0 => h_1 ()
    | Int.ofNat d@hd:d'.succ => h_2 d d' hd
    | Int.negSucc d => h_3 d) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
where `G` is locally-full and cover-dense, and `ℱ', ℱ` are sheaves,
we may obtain a natural isomorphism between presheaves.
 -/
CategoryTheory.Functor.IsCoverDense.sheafIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ ℱ' : CategoryTheory.Sheaf K A} → (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) → (ℱ ≅ ℱ')
-- Mathlib.Topology.Constructions
Continuous.rangeFactorization : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Continuous (Set.rangeFactorization f)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_monotone : Monotone Cardinal.lift.{u_2, u_1}
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variable to occurrences.
For example, an entry `x ↦ {y, z}` means that `x` may occur in `lowers`, or `uppers`, or `diseqs` of
variables `y` and `z`.
If `x` occurs in `diseqs[y]`, `lowers[y]`, or `uppers[y]`, then `y` is in `occurs[x]`,
but the reverse is not true.
If `x` is in `elimStack`, then `occurs[x]` is the empty set.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.occurs : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray Lean.Meta.Grind.Arith.Linear.VarSet
-- Lean.Parser.Extra
Lean.Parser.group.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- The setoid structure on `A` defined by the equivalence relation of `IsConjRoot R · ·`.
 -/
IsConjRoot.setoid : (R : Type u_1) → (A : Type u_5) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Setoid A
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_biUnion_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I},
  π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J
-- Lean.Data.PersistentArray
Lean.PersistentArray.stats : {α : Type u} → Lean.PersistentArray α → Lean.PersistentArray.Stats
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).minKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.sub : Nat.Primrec' fun v => v.head - v.tail.head
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of the forward direction of `isMin_iff_eq_bot`. -/
IsMin.eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsMin a → a = ⊥
-- Init.Data.Array.Lemmas
List.foldrM_push_eq_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α} {f : α → m β}
  {xs : Array β},
  List.foldrM (fun x xs => xs.push <$> f x) xs l = do
    let __do_lift ← List.mapM f l.reverse
    pure (xs ++ __do_lift.toArray)
-- Mathlib.Order.Monotone.Defs
/-- **Alias** of the forward direction of `monotone_iff_apply₂`. -/
Monotone.apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, Monotone f → ∀ (i : ι), Monotone fun x => f x i
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.union_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → μ t = 0 → MeasureTheory.NullMeasurableSet (s ∪ t) μ
-- Mathlib.Topology.Sober
Topology.IsOpenEmbedding.quasiSober : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsOpenEmbedding f → ∀ [QuasiSober β], QuasiSober α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapAddGrp_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapAddGrp.unitIso =
    CategoryTheory.Functor.mapAddGrpIdIso.symm ≪≫
      CategoryTheory.Functor.mapAddGrpNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapAddGrpCompIso