mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.Modules.toPresheaf X).ReflectsIsomorphisms
-- Mathlib.Algebra.Group.Basic
eq_zero_sub_of_add_eq_zero_right : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a + b = 0 → b = 0 - a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.continuous_coe : Continuous Real.Angle.coe
-- Mathlib.Order.Category.DistLat
/-- Constructs an equivalence between distributive lattices from an order isomorphism between them.
 -/
DistLat.Iso.mk : {α β : DistLat} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.trivial_comon_counit : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_pow_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  [inst_3 : AddMonoid A] [inst_4 : AddMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (n : ℕ) (f : AddMonoidAlgebra R A), (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_mono : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L]
  {q₁ q₂ : Submodule K (Module.Dual K ↥H)}
  (hq₁ : ∀ (i : ↥LieSubalgebra.root), q₁ ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i))
  (hq₂ :
    ∀ (i : ↥LieSubalgebra.root), q₂ ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)),
  q₁ ≤ q₂ → LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q₁ hq₁ ≤ LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q₂ hq₂
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {s : S},
  IsAlgebraic R s → s ∈ nonZeroDivisors S → ∃ q, q.coeff 0 ≠ 0 ∧ (Polynomial.aeval s) q = 0
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Ioi_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α} {n : ℤ},
  ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.not_matchesAt_of_prefixFunction_eq : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    ∀ {k : ℕ} {hki : needlePos.byteIdx - 1 < pat.copy.toByteArray.size},
      String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat.copy.toByteArray (needlePos.byteIdx - 1) hki =
          k →
        ∀ (p : s.Pos),
          stackPos.unoffsetBy needlePos ≤ p.offset →
            p.offset < stackPos.unoffsetBy { byteIdx := k } →
              ∀ {h₁ : stackPos < s.rawEndPos} {h₂ : needlePos < pat.rawEndPos},
                s.getUTF8Byte stackPos h₁ ≠ pat.getUTF8Byte needlePos h₂ → ¬String.Slice.Pattern.Model.MatchesAt pat p
-- Init.GetElem
Array.get!Internal.eq_1 : ∀ {α : Type u} [inst : Inhabited α] (a : Array α) (i : ℕ), a.get!Internal i = a.getD i default
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforward_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (i : E.I₀), (CategoryTheory.PreZeroHypercover.pushforward f E).f i = CategoryTheory.CategoryStruct.comp (E.f i) f
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUSizeHXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_of_not_isSFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (κ : ProbabilityTheory.Kernel α β), ¬ProbabilityTheory.IsSFiniteKernel κ → μ.compProd κ = 0
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_one : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R],
  Matrix.permanent 1 = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lift.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : M → α) (h : ∀ (a b : M), ArchimedeanClass.mk a = ArchimedeanClass.mk b → f a = f b),
  ArchimedeanClass.lift f h = Quotient.lift f ⋯
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- A submodule is a pointed cone.  -/
PointedCone.ofSubmodule : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → Submodule R E → PointedCone R E
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.mk.sizeOf_spec : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι} [inst_2 : SizeOf ι]
  [inst_3 : (a : ι) → SizeOf (F a)] [inst_4 : (a : ι) → SizeOf (X a)] [inst_5 : (a : ι) → SizeOf (s a)]
  (equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i) (nat : InverseSystem.IsNatEquiv f equiv)
  (compat :
    ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
      (equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2),
  sizeOf { equiv := equiv, nat := nat, compat := compat } = 1
-- Mathlib.GroupTheory.Congruence.Basic
Con.mrange_mk' : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M}, MonoidHom.mrange c.mk' = ⊤
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.restrictScalars.congr_simp : ∀ (R : Type u_1) {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : CommSemiring S] [inst_7 : Algebra S A] [inst_8 : Module S M] [inst_9 : LinearMap.CompatibleSMul A M R S]
  (d d_1 : Derivation S A M), d = d_1 → Derivation.restrictScalars R d = Derivation.restrictScalars R d_1
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopModuleCat.endRingEquiv.eq_1 : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (M : TopModuleCat R),
  M.endRingEquiv =
    { toFun := TopModuleCat.Hom.hom, invFun := TopModuleCat.ofHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
      map_add' := ⋯ }
-- Mathlib.Tactic.Translate.Core
/-- Argument `n` needs to be checked. This is specified with `(relevant_arg := n)`.  -/
Mathlib.Tactic.Translate.RelevantArg.arg : ℕ → Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_insert_right : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → insert b (Finset.Ioo a b) = Finset.Ioc a b
-- Mathlib.Analysis.Calculus.ContDiff.CPolynomial
ContinuousMultilinearMap.contDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {n : WithTop ℕ∞},
  ContDiff 𝕜 n ⇑f
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
instDecidableEqDihedralGroup : {n : ℕ} → DecidableEq (DihedralGroup n)
-- Std.Http.Data.Headers.Name
/-- Standard Date header name
 -/
Std.Http.Header.Name.date : Std.Http.Header.Name
-- Init.Data.Vector.Algebra
Vector.instNeg : {α : Type u_1} → {n : ℕ} → [Neg α] → Neg (Vector α n)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.toEquiv : {X : Type u_5} → {Y : Type u_6} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → X ≃ Y
-- Mathlib.GroupTheory.OrderOfElement
finEquivZPowers_symm_apply : ∀ {G : Type u_1} [inst : Group G] {x : G} (hx : IsOfFinOrder x) (n : ℕ),
  (finEquivZPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.span_range_eq_ideal : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = KaehlerDifferential.ideal R S
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.IsEntriesNode : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β → Prop
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_top : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f], Submodule.localized₀ p f ⊤ = ⊤
-- Lean.LibrarySuggestions.SymbolFrequency
/-- The symbol frequency map for imported constants. This is initialized on first use.  -/
Lean.LibrarySuggestions.symbolFrequencyMap : Lean.CoreM (Lean.NameMap ℕ)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x y : M₁),
  f (x + y) = f x + f y
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `add_apply`. -/
ContinuousMultilinearMap.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withoutCheckDeprecated : {m : Type → Type u_1} → {α : Type} → [MonadWithReaderOf Lean.Elab.Term.Context m] → m α → m α
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- A lax functor `F` between bicategories `B` and `C` consists of a function between objects
`F.obj`, a function between 1-morphisms `F.map`, and a function between 2-morphisms `F.map₂`.

Unlike functors between categories, `F.map` does not need to strictly commute with composition,
and does not need to strictly preserve the identity. Instead, there are specified 2-morphisms
`𝟙 (F.obj a) ⟶ F.map (𝟙 a)` and `F.map f ≫ F.map g ⟶ F.map (f ≫ g)`.

`F.map₂` strictly commutes with composition and preserves the identity. It also preserves the
associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains
of 2-morphisms.
 -/
CategoryTheory.LaxFunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Stream'.Seq α}, b ∈ Stream'.Seq.map f s → ∃ a ∈ s, f a = b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : IrreducibleSpace ↥X] (f : X.PartialMap Y),
  f.toRationalMap.fromFunctionField = f.fromFunctionField
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.continuousOn_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {r : ℝ},
  InnerProductSpace.HarmonicContOnCl f (Metric.ball x r) → ContinuousOn f (Metric.closedBall x r)
-- Init.Data.BitVec.Basic
BitVec.instComplement : {w : ℕ} → Complement (BitVec w)
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  {m : M} {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ →
    ∀ (n : ℕ), ⁅h, ((LieModule.toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((LieModule.toEnd R L M) f ^ n) m
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.CommMonoid.mul_prod_eraseIdx : ∀ {M : Type u_4} [inst : CommMonoid M] {l : List M} {i : ℕ} (h : i < l.length), l[i] * (l.eraseIdx i).prod = l.prod
-- Mathlib.Algebra.GradedMulAction
/-- Internally graded version of `Mul.toSMul`.  -/
SetLike.GradedMul.toGradedSMul : ∀ {ιA : Type u_1} {R : Type u_4} [inst : AddMonoid ιA] [inst_1 : Monoid R] {S : Type u_5} [inst_2 : SetLike S R]
  (A : ιA → S) [SetLike.GradedMonoid A], SetLike.GradedSMul A A
-- Init.Data.SInt.Lemmas
Int16.toNat_toBitVec_of_le : ∀ {x : Int16}, 0 ≤ x → x.toBitVec.toNat = x.toNatClampNeg
-- Mathlib.Data.List.Lex
List.lex_nil_or_eq_nil : ∀ {α : Type u} {r : α → α → Prop} (l : List α), List.Lex r [] l ∨ l = []
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_div : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [inst : RCLike L] (r : L)
  (f : α → L), ∫ (a : α), f a / r ∂μ = (∫ (a : α), f a ∂μ) / r
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Associativity of the enriched structure  -/
CategoryTheory.MonoidalClosed.assoc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (w x y z : C)
  [inst_2 : CategoryTheory.Closed w] [inst_3 : CategoryTheory.Closed x] [inst_4 : CategoryTheory.Closed y] {Z : C}
  (h : w ⟹ z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (w ⟹ x) (x ⟹ y) (y ⟹ z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.comp w x y) (y ⟹ z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp w y z) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (w ⟹ x) (CategoryTheory.MonoidalClosed.comp x y z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp w x z) h)
-- Lean.Elab.Match
/-- Topological sort. We need it because inaccessible patterns may contain pattern variables that are declared later.
That is, processing patterns from left to right to do not guarantee that the pattern variables are collected in the
"right" order. "Right" here means pattern `x` must occur before pattern `y` if `y`s type depends on `x`.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.topSort : Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Algebra.Order.Ring.Idempotent
mul_eq_zero_add_eq_one_ext_left : ∀ {R : Type u_1} [inst : CommSemiring R] {a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }}, (↑a).1 = (↑b).1 → a = b
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquiv_eq_dualTensorHomEquivOfBasis : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι],
  have this := ⋯;
  have this_1 := ⋯;
  dualTensorHomEquiv R M N = dualTensorHomEquivOfBasis b
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_mk : ∀ {R : Type u_1} [inst : Semiring R] {f : ℕ → R}, PowerSeries.constantCoeff (PowerSeries.mk f) = f 0
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_copy : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = ↑S),
  ↑(S.copy s hs) = s
-- Mathlib.FieldTheory.KrullTopology
/-- Let `L/E/K` be a tower of fields with `E/K` finite. Then `Gal(L/E)` is an open subgroup of
`Gal(L/K)`.  -/
IntermediateField.fixingSubgroup_isOpen : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [FiniteDimensional K ↥E], IsOpen ↑E.fixingSubgroup
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `M ⊗ -` is an exact functor. See
`Module.Flat.iff_lTensor_exact` to specialize the universe of `N, N', N''` to `Type (max u v)`.  -/
Module.Flat.iff_lTensor_exact' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (X : C)
  [CategoryTheory.Injective X], CategoryTheory.IsIso (F.toRightDerivedZero.app X)
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupMap_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H : AddSubgroup G),
  Function.Surjective ⇑(f.addSubgroupMap H)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_preOmega : ∀ (o : Ordinal.{u_1}), (Ordinal.preOmega o).IsInitial
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)]
  [inst_1 : (i : ι) → VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)], VAddCommClass M N ((i : ι) → α i)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_mul_const_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {u : 𝕜 → 𝕜'} (v : 𝕜'), deriv (fun y => u y * v) x = deriv u x * v
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `fallback` if no such element exists.
 -/
Std.ExtTreeSet.getGTD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α → α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.mk : Lean.Meta.Grind.EMatchTheorem →
  Lean.Expr →
    Lean.Expr →
      ℕ →
        List Lean.Meta.Grind.TheoremGuard → List Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.DelayedTheoremInstance
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : Set α}, MeasurableSet s → (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.NormalMono.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : X ⟶ Y} →
          (Z : C) →
            (g : Y ⟶ Z) →
              (w : CategoryTheory.CategoryStruct.comp f g = 0) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f w) → CategoryTheory.NormalMono f
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a
bigger matrix indexed by [m × (n₁ ⊕ n₂)]  -/
Matrix.fromCols : {R : Type u_1} →
  {m : Type u_2} → {n₁ : Type u_6} → {n₂ : Type u_7} → Matrix m n₁ R → Matrix m n₂ R → Matrix m (n₁ ⊕ n₂) R
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_add : ∀ {c d x y z w : ℕ}, Zsqrtd.SqLe x c y d → Zsqrtd.SqLe z c w d → Zsqrtd.SqLe (x + z) c (y + w) d
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A chosen `S.HomologyData` for a short complex `S` that has homology  -/
CategoryTheory.ShortComplex.homologyData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → S.HomologyData
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorBoth.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Stream.Init
Stream'.tail_even : ∀ {α : Type u} (s : Stream' α), s.even.tail = s.tail.tail.even
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_le_size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.size ≤ (t.erase k).size + 1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_monomial_succ : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], ((Polynomial.monomial (n + 1)) a).coeff 0 = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrict_mker`. -/
AddMonoidHom.restrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N),
  AddMonoidHom.mker (f.domRestrict S) = AddSubmonoid.comap S.subtype (AddMonoidHom.mker f)
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.clsName : Lean.MethodSpecsInfo✝ → Lean.Name
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- If `s` and `t` are null measurable sets of equal measure
and their intersection has finite measure,
then `s \ t` and `t \ s` have equal measures too.  -/
MeasureTheory.measure_sdiff_symm : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t μ → μ s = μ t → μ (s ∩ t) ≠ ⊤ → μ (s \ t) = μ (t \ s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.map f t) k = (Option.map (f k') (Std.ExtDTreeMap.Const.get? t k)).get!
-- Init.Data.Rat.Lemmas
Rat.normalize_self : ∀ (r : ℚ), Rat.normalize r.num r.den ⋯ = r
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
Std.Tactic.BVDecide.BVPred.mkUlt : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.Entrypoint α
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff`. -/
Set.diff_diff : ∀ {α : Type u_1} {s t u : Set α}, (s \ t) \ u = s \ (t ∪ u)
-- Mathlib.Condensed.Limits
instHasLimitsOfSizeCondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (CondensedMod R)