mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- Simple graphs on `card V` vertices having at least `(turanDensity H + o(1)) * (card V) ^ 2`
edges contain `H`, for sufficiently large `card V`.  -/
SimpleGraph.isContained_of_card_edgeFinset : ∀ {W : Type u_1} (H : SimpleGraph W) {ε : ℝ},
  0 < ε →
    ∀ {V : Type u_2} [inst : Fintype V],
      Fintype.card V ≥ H.turanDensityConst ε →
        ∀ (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],
          ↑G.edgeFinset.card ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H.IsContained G
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The sheaf hom on all basic opens, commuting with restrictions.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens : (X : AlgebraicGeometry.LocallyRingedSpace) →
  (CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp
      (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj ⟶
    (CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp
      ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj
-- Lean.Meta.Basic
Lean.Meta.getTheoremInfo : Lean.ConstantInfo → Lean.MetaM (Option Lean.ConstantInfo)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, Option.all (fun x_2 => x_2 == k) (m.getKey? k) = true
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.IsStrictSegal.segal : ∀ {X : SSet} [self : X.IsStrictSegal] (n : ℕ), Function.Bijective (X.spine n)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The bijection between factorizations in `C` and factorizations in `Cᵒᵖ`.  -/
CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {X Y : C} → {f : X ⟶ Y} → W₁.MapFactorizationData W₂ f ≃ W₂.op.MapFactorizationData W₁.op f.op
-- Mathlib.Data.List.Rotate
List.isRotated_iff_mem_map_range : ∀ {α : Type u} {l l' : List α}, l ~r l' ↔ l' ∈ List.map l.rotate (List.range (l.length + 1))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub' : ∀ {x : ℝ}, 0 ≤ x → ∀ {y z : ℝ}, y - z ≠ 0 → x ^ (y - z) = x ^ y / x ^ z
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.mul_kronecker_mul : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17}
  [inst : Fintype m] [inst_1 : Fintype m'] [inst_2 : CommSemiring α] (A : Matrix l m α) (B : Matrix m n α)
  (A' : Matrix l' m' α) (B' : Matrix m' n' α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A * B) (A' * B') =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A A' * Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B B'
-- Mathlib.Tactic.CancelDenoms.Core
/-- The proof that `cancelled` is valid.  -/
Mathlib.Tactic.CancelDenoms.CancelResult.pf : {u : Lean.Level} →
  {α : Q(Type u)} →
    {mα : Q(Mul «$α»)} →
      {e v : Q(«$α»)} → (self : Mathlib.Tactic.CancelDenoms.CancelResult mα e v) → Q(«$v» * «$e» = unknown_1)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_finsum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.LeAtTop], Function.HasFiniteSupport f → ∑'[L] (b : β), f b = ∑ᶠ (b : β), f b
-- Lean.Attributes
Lean.ParametricAttribute.preserveOrder : {α : Type} → Lean.ParametricAttribute α → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `C` has an initial object such that every morphism *to* it is an isomorphism, then `C`
has strict initial objects.  -/
CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
  (∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f) → CategoryTheory.Limits.HasStrictInitialObjects C
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.finrank_eq_two : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] [StrongRankCondition R], Module.finrank R (QuadraticAlgebra R a b) = 2
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteConstObjWhiskeringRight : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (J : Type) →
            CategoryTheory.CatCommSq (CategoryTheory.Functor.const (CategoryTheory.Discrete J)) L
              ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L)
              (CategoryTheory.Functor.const (CategoryTheory.Discrete J))
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instIsCentralScalarPreLp : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : (i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)],
  IsCentralScalar 𝕜 (PreLp E)
-- Mathlib.Analysis.Calculus.MeanValue
constant_of_has_deriv_right_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) → (∀ x ∈ Set.Ico a b, HasDerivWithinAt f 0 (Set.Ici x) x) → ∀ x ∈ Set.Icc a b, f x = f a
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.State.mk.sizeOf_spec : ∀ (found : Lean.NameSet) (vars : Array Lean.Elab.Term.PatternVar),
  sizeOf { found := found, vars := vars } = 1 + sizeOf found + sizeOf vars
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instNontrivial : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [Nontrivial R] [Nonempty M], Nontrivial (AddMonoidAlgebra R M)
-- Lean.Data.Lsp.Internal
/-- Name of the parent declaration of this location.  -/
Lean.Lsp.RefInfo.Location.parentDecl? : Lean.Lsp.RefInfo.Location → Option String
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- If `F ≤ E` are two intermediate fields of `L / K`, then `E` is also an intermediate field of
`L / F`. It can be viewed as an inverse to `IntermediateField.restrictScalars`.  -/
IntermediateField.extendScalars : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → {F E : IntermediateField K L} → F ≤ E → IntermediateField (↥F) L
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_20 : Lean.RealizationContext✝ → Lean.Environment
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulUpwardEnumerableNat : Std.PRange.LawfulUpwardEnumerable ℕ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.star.sizeOf_spec : sizeOf Lean.Meta.LazyDiscrTree.Key.star = 1
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (l : List α) (acc : Array α)
  (h_1 : (l : List α) → (acc : Array α) → motive 0 l acc) (h_2 : (x : ℕ) → (acc : Array α) → motive x [] acc)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (acc : Array α) → motive n.succ (a :: l) acc),
  (match 0, l, acc with
    | 0, l, acc => h_1 l acc
    | x, [], acc => h_2 x acc
    | n.succ, a :: l, acc => h_3 n a l acc) =
    h_1 l acc
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_mul_const : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.variance (fun ω => X ω * c) μ = ProbabilityTheory.variance X μ * c ^ 2
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fG_iff : ∀ (M : Type u_3) [inst : AddMonoid M], AddMonoid.FG M ↔ ⊤.FG
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.coeAddMonoidHom.eq_1 : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] (A : ι → S),
  DirectSum.coeAddMonoidHom A = DirectSum.toAddMonoid fun i => AddSubmonoidClass.subtype (A i)
-- Init.Coe
instCoeHTCOfCoeOTC : {α : Sort u_1} → {β : Sort u_2} → [CoeOTC α β] → CoeHTC α β
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_add : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f g : M →ₛₗ[σ₁₂] M₂)
  (h : M₂ →ₛₗ[σ₂₃] M₃), h ∘ₛₗ (f + g) = h ∘ₛₗ f + h ∘ₛₗ g
-- Lean.Data.Json.Parser
Lean.Json.Parser.lookahead : (p : Char → Prop) → String → [DecidablePred p] → Std.Internal.Parsec.String.Parser Unit
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  CategoryTheory.Limits.Cocone.functorialityEquivalence F e =
    CategoryTheory.Equivalence.mk'' (CategoryTheory.Limits.Cocone.functoriality F e.functor)
      ((CategoryTheory.Limits.Cocone.functoriality (F.comp e.functor) e.inverse).comp
        (CategoryTheory.Limits.Cocone.precomposeEquivalence
            (F.associator e.functor e.inverse ≪≫ F.isoWhiskerLeft e.unitIso.symm ≪≫ F.rightUnitor)).functor)
      (CategoryTheory.NatIso.ofComponents'
        (fun c =>
          CategoryTheory.Limits.Cocone.extInv
            (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).pt) ⋯)
        ⋯)
      (CategoryTheory.NatIso.ofComponents' (fun c => CategoryTheory.Limits.Cocone.extInv (e.counitIso.app c.pt) ⋯) ⋯) ⋯
-- Mathlib.Algebra.Group.Graph
/-- **Goursat's lemma** for monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃* I`.  -/
Submonoid.exists_mulEquiv_eq_mgraph : ∀ {H : Type u_2} {I : Type u_3} [inst : Monoid H] [inst_1 : Monoid I] {G : Submonoid (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) →
    Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = e.toMonoidHom.mgraph
-- Mathlib.Data.EReal.Operations
EReal.top_mul_of_pos : ∀ {x : EReal}, 0 < x → ⊤ * x = ⊤
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddSemigrpIso_inv : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (e : X ≃+ Y),
  e.toAddSemigrpIso.inv = AddSemigrp.ofHom e.symm.toAddHom
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedMul_algebraMap : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i))
  (r : R), ((TensorProduct.gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x
-- Mathlib.Algebra.Order.Ring.Defs
one_add_le_one_sub_mul_one_add : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b c : R},
  a + b + b * c ≤ c → 1 + a ≤ (1 - b) * (1 + c)
-- Mathlib.Probability.Independence.InfinitePi
ProbabilityTheory.iIndepFun.hasLaw_infinitePi : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    ProbabilityTheory.iIndepFun X P →
      AEMeasurable (fun ω i => X i ω) P →
        ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.infinitePi μ) P
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.eq_2 : ∀ {L : FirstOrder.Language} {M : Type u_5} {α : Type u_3}
  (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x))
  (v : α → M) (xs : Fin x → M)
  (h_1 : (x : ℕ) → (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs)
  (h_2 :
    (x : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
        (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs)
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin x)) →
          (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs)
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs)
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs),
  (match x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => h_1 x _v _xs
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs => h_2 x t₁ t₂ v xs
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs => h_3 x l R ts v xs
    | x, f₁.imp f₂, v, xs => h_4 x f₁ f₂ v xs
    | x, f.all, v, xs => h_5 x f v xs) =
    h_2 x t₁ t₂ v xs
-- Mathlib.RingTheory.Filtration
/-- An `I` filtration is stable if `I • F.N n = F.N (n+1)` for large enough `n`.  -/
Ideal.Filtration.Stable : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → I.Filtration M → Prop
-- Init.Prelude
Nat.not_succ_le_zero : ∀ (n : ℕ), n.succ ≤ 0 → False
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inr_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.fst X Y) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- Let `Q` be a property of ring maps that is stable under localization.
Then if the associated property of scheme morphisms holds for `f`, `Q` holds on all stalks.  -/
AlgebraicGeometry.HasRingHomProperty.stalkMap : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
      Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
    P f → ∀ (x : ↥X), Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- `Spec (𝒪ₓ(U)/I(U)) ⟶ Spec (𝒪ₓ(U)) = U`, the closed immersion into `U`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → (U : ↑X.affineOpens) → I.glueDataObj U ⟶ ↑↑U
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.hasDerivAt_Gamma_one_half : HasDerivAt Complex.Gamma (-↑√Real.pi * (↑Real.eulerMascheroniConstant + 2 * Complex.log 2)) (1 / 2)
-- Mathlib.Control.Monad.Writer
/-- Emit an output `w`.  -/
MonadWriter.tell : {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → ω → M PUnit.{u + 1}
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSeminormedCommRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : SeminormedCommRing R] → SeminormedCommRing (BoundedContinuousFunction α R)
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.liftEquiv_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : Topology.IsQuotientMap ⇑f)
  (g : { g // Function.FactorsThrough ⇑g ⇑f }), hf.liftEquiv g = hf.lift ↑g ⋯
-- Std.Data.HashMap.RawLemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `getElem_insertIfNew`.  -/
Std.HashMap.Raw.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Init.Data.UInt.Lemmas
USize.toUInt16_add : ∀ (a b : USize), (a + b).toUInt16 = a.toUInt16 + b.toUInt16
-- Mathlib.Order.RelIso.Basic
RelEmbedding.eq_preimage : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), r = ⇑f ⁻¹'o s
-- Mathlib.Topology.Algebra.ConstMulAction
vadd_closure_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α] (c : M)
  (s : Set α), c +ᵥ closure s ⊆ closure (c +ᵥ s)
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Multiplying `a⁻¹` by `a` twice results in `a` (whether or not `a`
is zero).  -/
inv_mul_mul_self : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a⁻¹ * a * a = a
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.mkAppRevRangeAux.eq_def : ∀ (revArgs : Array Lean.Expr) (start : ℕ) (b : Lean.Expr) (i : ℕ),
  Lean.Expr.mkAppRevRangeAux✝ revArgs start b i =
    if i ≤ start then b
    else
      have i := i - 1;
      Lean.Expr.mkAppRevRangeAux✝ revArgs start (Lean.mkApp b revArgs[i]!) i
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInv : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [Inv G] → Inv (l.Germ G)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_toLinearMap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), ⇑φ.toLinearMap = ⇑φ
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replaceTR.go.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (b c : α) (a : Array α) (a_1 : α) (as : List α),
  List.replaceTR.go✝ l b c (a_1 :: as) a =
    bif b == a_1 then a.toListAppend (c :: as) else List.replaceTR.go✝ l b c as (a.push a_1)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.coeff_domCongrBialgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (a : AddMonoidAlgebra A N),
  ((AddMonoidAlgebra.domCongrBialgEquiv R A e).symm a).coeff = Finsupp.mapDomain (⇑e.symm) a.coeff
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.size_eq_match_roc : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => if next ≤ r.upper then (next<...=r.upper).size + 1 else 0
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_uIcc : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.uIcc a b) = Set.uIcc a b
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBound?_lt : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y z : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  t.lowerBound? x = some y → z ∈ t → (cmp y z = Ordering.lt ↔ cmp x z = Ordering.lt)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_eq_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.MemLp f p μ → p ≠ 0 → (MeasureTheory.lpNorm f p μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- An element is contained in the relative perfect closure if and only if its minimal polynomial
has separable degree one.  -/
mem_perfectClosure_iff_natSepDegree_eq_one : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- The topology on `Over S` induced from the topology on `Scheme` defined by `P`.
This agrees with the topology induced by `S.overPretopology P`, see
`AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology`.  -/
AlgebraicGeometry.Scheme.overGrothendieckTopology : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  (S : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology (CategoryTheory.Over S)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α}, m.WF → (Array.find? (fun x => x.1 == k) m.toArray = none ↔ m.contains k = false)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toList_roc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...=n).toList[i]?.isNone = true) = ((n - m).toNat ≤ i)
-- Mathlib.RepresentationTheory.Basic
/-- A `k`-linear representation of `G` on `V` can be thought of as
an algebra map from `k[G]` into the `k`-linear endomorphisms of `V`.
 -/
Representation.asAlgebraHom : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] → Representation k G V → MonoidAlgebra k G →ₐ[k] Module.End k V
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- A topological ring is `J`-adic if and only if it admits the powers of `J` as a basis of
open neighborhoods of zero.  -/
isAdic_iff : ∀ {R : Type u_1} [inst : CommRing R] [top : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R},
  IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ nhds 0, ∃ n, ↑(J ^ n) ⊆ s
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
AlgebraicGeometry.Polynomial.isOpen_imageOfDf : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, IsOpen (AlgebraicGeometry.Polynomial.imageOfDf f)
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.affineAnd.eq_1 : ∀ (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (X x : AlgebraicGeometry.Scheme)
  (f : X ⟶ x) [inst : AlgebraicGeometry.IsAffine x],
  AlgebraicGeometry.affineAnd Q f =
    (AlgebraicGeometry.IsAffine X ∧ Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)))
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F → F.Nonempty
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X' : C} (f : X' ⟶ X) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasKernel g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).inv
      (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)).arrow =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow (CategoryTheory.inv f)
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Iic_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a : α), Set.SurjOn f (Set.Iic a) (Set.Iic (f a))
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_int16ToBitVec : ∀ (x : Int16), Int8.ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8