mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.IsContained.mono_left`. -/
SimpleGraph.IsContained.trans_le' : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α},
  A ≤ A' → A'.IsContained B → A.IsContained B
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow.eq_1 : ∀ (n : ℕ) (r : ℝ), Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow [] n r = default
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
FiberBundle.trivializationAt_continuousAlternatingMap_source : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (x₀ : B),
  (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀).source =
    Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.ker_corootForm_eq_dualAnnihilator : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], LinearMap.ker P.CorootForm = Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator
-- Init.Data.Order.Ord
Std.instTransOrdProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.TransOrd α] [Std.TransOrd β], Std.TransOrd (α × β)
-- Mathlib.Analysis.Calculus.MeanValue
/-- If `f` has zero derivative on a connected open set, then `f` is constant on `s`.  -/
IsOpen.exists_is_const_of_fderiv_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E},
  IsOpen s → IsPreconnected s → DifferentiableOn 𝕜 f s → Set.EqOn (fderiv 𝕜 f) 0 s → ∃ a, ∀ x ∈ s, f x = a
-- Init.Data.Vector.Lemmas
Vector.all_eq : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, xs.all p = decide (∀ (i : ℕ) (x : i < n), p xs[i] = true)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `SemilinearIsometryEquivClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear
isometric equivs `E → E₂`.

See also `LinearIsometryEquivClass F R E E₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`.  -/
SemilinearIsometryEquivClass : (𝓕 : Type u_11) →
  {R : outParam (Type u_12)} →
    {R₂ : outParam (Type u_13)} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          (σ₁₂ : outParam (R →+* R₂)) →
            {σ₂₁ : outParam (R₂ →+* R)} →
              [RingHomInvPair σ₁₂ σ₂₁] →
                [RingHomInvPair σ₂₁ σ₁₂] →
                  (E : outParam (Type u_14)) →
                    (E₂ : outParam (Type u_15)) →
                      [inst_4 : SeminormedAddCommGroup E] →
                        [inst_5 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → [EquivLike 𝓕 E E₂] → Prop
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.associator_inv_toNatTrans : ∀ {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E),
  (CategoryTheory.Bicategory.associator F G H).inv.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).inv
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_apply : ∀ {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : a ≠ 0)
  (x : 𝕜), (affineHomeomorph a b h) x = a * x + b
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_norm_le_of_norm_le : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) (c : NNReal),
  ‖g‖ ≤ ↑c → ‖SemiNormedGrp.explicitCokernelDesc w‖ ≤ ↑c
-- Lean.Data.Options
Lean.getOptionDeclsArray : IO (Array (Lean.Name × Lean.OptionDecl))
-- Mathlib.NumberTheory.NumberField.DirichletDensity
NumberField.Set.HasDirichletDensity.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S S_1 : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))),
  S = S_1 →
    ∀ (δ δ_1 : ℝ), δ = δ_1 → NumberField.Set.HasDirichletDensity S δ = NumberField.Set.HasDirichletDensity S_1 δ_1
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy of `mul_invOf_cancel_right` for rectangular matrices.  -/
Matrix.mul_invOf_cancel_right : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  (A : Matrix m n α) (B : Matrix n n α) [inst_3 : Invertible B], A * B * ⅟B = A
-- Lean.Widget.Types
Lean.Widget.WidgetInstance.mk.inj : ∀ {id : Lean.Name} {javascriptHash : UInt64} {props : StateM Lean.Server.RpcObjectStore Lean.Json} {id_1 : Lean.Name}
  {javascriptHash_1 : UInt64} {props_1 : StateM Lean.Server.RpcObjectStore Lean.Json},
  { id := id, javascriptHash := javascriptHash, props := props } =
      { id := id_1, javascriptHash := javascriptHash_1, props := props_1 } →
    id = id_1 ∧ javascriptHash = javascriptHash_1 ∧ props = props_1
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : Ω → E}
  [inst_3 : InnerProductSpace ℝ E] {Y : Ω → E},
  AEMeasurable X P →
    AEMeasurable Y P →
      ProbabilityTheory.IndepFun X Y P →
        MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => X ω + Y ω) P) =
          MeasureTheory.charFun (MeasureTheory.Measure.map X P) * MeasureTheory.charFun (MeasureTheory.Measure.map Y P)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.coxeterWeight_nonneg : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [inst_10 : Module S M] [IsScalarTower S R M]
  [IsStrictOrderedRing S], 0 ≤ P.coxeterWeightIn S i j
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.subsemiringClass : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜],
  SubsemiringClass (HomogeneousSubsemiring 𝒜) A
-- Lean.Meta.LazyDiscrTree
/-- Given an expression we are looking for patterns that match, return the key and sub-expressions.
 -/
Lean.Meta.LazyDiscrTree.MatchClone.getMatchKeyArgs : Lean.Expr → Bool → Lean.MetaM (Lean.Meta.LazyDiscrTree.Key × Array Lean.Expr)
-- Batteries.Tactic.GeneralizeProofs
/-- Generalize `prop`, where `proof` is its proof.
 -/
Batteries.Tactic.GeneralizeProofs.MAbs.insertProof : Lean.Expr → Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs Unit
-- Mathlib.Order.Nucleus
NucleusClass.toInfHomClass : ∀ {F : Type u_2} {X : Type u_3} {inst : SemilatticeInf X} {inst_1 : FunLike F X X} [self : NucleusClass F X],
  InfHomClass F X X
-- Std.Http.Data.URI.Basic
Std.Http.instBEqURI : BEq Std.Http.URI
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Subcomplex.liftPath_arrow_coe : ∀ {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n)
  (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op { len := 0 }))
  (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op { len := 1 })) (j : Fin n),
  ↑((A.liftPath p hp₀ hp₁).arrow j) = p.arrow j
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.fibration_pullbackObjObjπ : ∀ {X₁ Y₁ E B : SSet} {i : X₁ ⟶ Y₁} {p : E ⟶ B} [CategoryTheory.Mono i] [HomotopicalAlgebra.Fibration p]
  (sq₁₃ : CategoryTheory.MonoidalClosed.internalHom.PullbackObjObj i p), HomotopicalAlgebra.Fibration sq₁₃.π
-- Init.GrindInstances.ToInt
Lean.Grind.instAddInt32SintOfNatNat : Lean.Grind.ToInt.Add Int32 (Lean.Grind.IntInterval.sint 32)
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier : ∀ {R : Type u} [inst : CommRing R] (A : AlgCat R), ↑(ModuleCat.MonModuleEquivalenceAlgebra.inverse.obj A).X = ↑A
-- Lean.Meta.Tactic.Ext
/-- Returns `true` if `d` contains theorem with name `declName`.  -/
Lean.Meta.Ext.ExtTheorems.contains : Lean.Meta.Ext.ExtTheorems → Lean.Name → Bool
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
toDegLex_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] (a b : α), toDegLex (a + b) = toDegLex a + toDegLex b
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.map Fin.castSuccEmb (Finset.Ioc i j) = Finset.Ioc i.castSucc j.castSucc
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.eq_1 : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (s : Set ι), LinearIndepOn R v s = LinearIndependent R fun (x : ↑s) => v ↑x
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasSum.sub : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f g : β → α} {a₁ a₂ : α},
  HasSum f a₁ L → HasSum g a₂ L → HasSum (fun b => f b - g b) (a₁ - a₂) L
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type u_1} {I : J → Type u_2}
  {inst_1 : CategoryTheory.Category.{v_1, u_1} J} {inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)}
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} {x y : k.Hom l}, x = y ↔ x.base = y.base ∧ x.hom = y.hom
-- Mathlib.Topology.Connected.PathConnected
/-- If `f` is continuous on `F` and `F` is path-connected, so is `f(F)`.  -/
IsPathConnected.image' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X},
  IsPathConnected F → ∀ {f : X → Y}, ContinuousOn f F → IsPathConnected (f '' F)
-- Mathlib.Algebra.Module.ZMod
/-- The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n`.
See note [reducible non-instances].  -/
AddCommGroup.zmodModule : {n : ℕ} → {G : Type u_3} → [inst : AddCommGroup G] → (∀ (x : G), n • x = 0) → Module (ZMod n) G
-- Mathlib.NumberTheory.LucasLehmer
/-- **Lucas-Lehmer Test**: a Mersenne number `2^p-1` is prime if and only if
the Lucas-Lehmer residue `s p (p-2) % (2^p - 1)` is zero.
 -/
LucasLehmer.LucasLehmerTest : ℕ → Prop
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given a splitting of a short complex `S`, this shows that `S.g` is a split epimorphism.  -/
CategoryTheory.ShortComplex.Splitting.splitEpi_g : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} → S.Splitting → CategoryTheory.SplitEpi S.g
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Init.Data.Vector.Attach
Vector.attach_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n},
  xs.reverse.attach =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodPUnit_symm_apply : ∀ (M : Type u_1) [inst : Monoid M], ⇑(MulEquiv.coprodPUnit M).symm = ⇑Monoid.Coprod.inl
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.card_le_vcDim : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, 𝒜.Shatters s → s.card ≤ 𝒜.vcDim
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitBy.loop.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → List α → List (List α) → Sort u_2) (a : α) (as : List α) (b : α) (r : List α)
  (acc : List (List α))
  (h_1 : (a : α) → (as : List α) → (b : α) → (r : List α) → (acc : List (List α)) → motive (a :: as) b r acc)
  (h_2 : (ag : α) → (r : List α) → (acc : List (List α)) → motive [] ag r acc),
  (match a :: as, b, r, acc with
    | a :: as, b, r, acc => h_1 a as b r acc
    | [], ag, r, acc => h_2 ag r acc) =
    h_1 a as b r acc
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation less-equal operator arising from `ValuativeRel`.  -/
ValuativeRel.vle : {R : Type u_1} → {inst : Semiring R} → [self : ValuativeRel R] → R → R → Prop
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instInhabited : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → Inhabited (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.toPerm_apply : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X), DilationEquiv.toPerm e = e.toEquiv
-- Init.Data.Nat.Lemmas
Nat.sub_min_sub_right : ∀ (a b c : ℕ), min (a - c) (b - c) = min a b - c
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk''.inj : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst : Monoid G} {inst_1 : Ring R}
  {inst_2 : AddCommGroup V} {inst_3 : TopologicalSpace V} {inst_4 : IsTopologicalAddGroup V} {inst_5 : Module R V}
  {inst_6 : AddCommGroup W} {inst_7 : TopologicalSpace W} {inst_8 : IsTopologicalAddGroup W} {inst_9 : Module R W}
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {toContinuousLinearEquiv : V ≃L[R] W}
  {cont : autoParam (Continuous (↑↑toContinuousLinearEquiv).toFun) ContinuousLinearMap.cont._autoParam}
  {isIntertwining' :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont }}
  {toContinuousLinearEquiv_1 : V ≃L[R] W}
  {cont_1 : autoParam (Continuous (↑↑toContinuousLinearEquiv_1).toFun) ContinuousLinearMap.cont._autoParam}
  {isIntertwining'_1 :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv_1, cont := cont_1 } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv_1, cont := cont_1 }},
  { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' } =
      { toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 } →
    toContinuousLinearEquiv = toContinuousLinearEquiv_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.mapEdgeSet_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (e : ↑G.edgeSet),
  f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom f) e
-- Mathlib.CategoryTheory.Shift.CommShift
/-- A functor `F` commutes with the shift by a monoid `A` if it is equipped with
commutation isomorphisms with the shifts by all `a : A`, and these isomorphisms
satisfy coherence properties with respect to `0 : A` and the addition in `A`.  -/
CategoryTheory.Functor.CommShift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D →
          (A : Type u_6) →
            [inst_2 : AddMonoid A] →
              [CategoryTheory.HasShift C A] → [CategoryTheory.HasShift D A] → Type (max (max u_1 u_6) v_2)
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a b : α i), Function.update f i '' Set.Icc a b = Set.Icc (Function.update f i a) (Function.update f i b)
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type E₇. See [bourbaki1968] plate VI, page 281.  -/
CartanMatrix.E₇ : Matrix (Fin 7) (Fin 7) ℤ
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.sub_mem_iff_left : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, y ∈ p → (x - y ∈ p ↔ x ∈ p)
-- Mathlib.CategoryTheory.Groupoid.Basic
CategoryTheory.Groupoid.isThin_iff : ∀ (C : Type u_1) [inst : CategoryTheory.Groupoid C], Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)
-- Init.Data.Array.Perm
Array.Perm.size_eq : ∀ {α : Type u_1} {xs ys : Array α}, xs.Perm ys → xs.size = ys.size
-- Mathlib.Algebra.Ring.Regular
/-- Right `Mul` by a `k : α` over `[Ring α]` is injective, if `k` is not a zero divisor.
The typeclass that restricts all terms of `α` to have this property is `NoZeroDivisors`.  -/
isRightRegular_of_non_zero_divisor : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] (k : α), (∀ (x : α), x * k = 0 → x = 0) → IsRightRegular k
-- Mathlib.Topology.Compactness.Lindelof
/-- `Filter.coclosedLindelof` is the filter generated by complements to closed Lindelof sets.  -/
Filter.coclosedLindelof : (X : Type u_2) → [TopologicalSpace X] → Filter X
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i : M₁ →ₗ[R] M₁) (j : M₂ →ₗ[R] M₂) (n : ℕ),
  hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItemTag.hash : Lean.Lsp.CompletionItemTag → UInt64
-- Mathlib.Algebra.Group.Submonoid.Defs
ZeroMemClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : Zero M] [inst_1 : SetLike S M], (∀ (s : S), 0 ∈ s) → ZeroMemClass S M
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_le_unionProd : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), S.prod T ≤ S.unionProd T
-- Mathlib.Tactic.Linter.TextBased
/-- Verify that all modules are named in `UpperCamelCase`  -/
Mathlib.Linter.TextBased.linter.modulesUpperCamelCase : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.range_gluedTo : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), Set.range ⇑I.gluedTo = ↑I.support
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ},
  CategoryTheory.Limits.coconeLeftOpOfConeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c),
            map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCoeSortType : CoeSort AddCommMonCat (Type u)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- The category of which this is a full subcategory  -/
CategoryTheory.ObjectProperty.FullSubcategory.obj : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {P : CategoryTheory.ObjectProperty C} → P.FullSubcategory → C
-- Mathlib.Analysis.Normed.Group.Basic
/-- A group homomorphism from a `CommGroup` to a `SeminormedGroup` induces a
`SeminormedCommGroup` structure on the domain.  -/
SeminormedCommGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : CommGroup E] → [inst_2 : SeminormedGroup F] → [MonoidHomClass 𝓕 E F] → 𝓕 → SeminormedCommGroup E
-- Mathlib.Algebra.Group.Defs
/-- Any `AddCommMagma G` that satisfies
`IsRightCancelAdd G` also satisfies `IsCancelAdd G`.  -/
AddCommMagma.IsRightCancelAdd.toIsCancelAdd : ∀ (G : Type u) [inst : AddCommMagma G] [IsRightCancelAdd G], IsCancelAdd G
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaMon.Full
-- Init.Data.List.Sublist
List.tail_suffix : ∀ {α : Type u_1} (l : List α), l.tail <:+ l
-- Init.Data.ByteArray.Basic
/-- Retrieves the size of the array as a platform-specific fixed-width integer.

Because `USize` is big enough to address all memory on every platform that Lean supports,
there are in practice no `ByteArray`s that have more elements that `USize` can count.
 -/
ByteArray.usize : ByteArray → USize
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.mk.injEq : ∀ (toPreElabHeaderResult : Lean.Elab.Command.PreElabHeaderResult) (indFVar : Lean.Expr)
  (toPreElabHeaderResult_1 : Lean.Elab.Command.PreElabHeaderResult) (indFVar_1 : Lean.Expr),
  ({ toPreElabHeaderResult := toPreElabHeaderResult, indFVar := indFVar } =
      { toPreElabHeaderResult := toPreElabHeaderResult_1, indFVar := indFVar_1 }) =
    (toPreElabHeaderResult = toPreElabHeaderResult_1 ∧ indFVar = indFVar_1)
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- An abbreviation for `PreValuationRing.cond` which should save some writing.  -/
ValuationRing.cond : ∀ {A : Type u} [inst : Mul A] [PreValuationRing A] (a b : A), ∃ c, a * c = b ∨ b * c = a
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- `Polynomial.map` as an `AlgHom` for noncommutative algebras.

This is the algebra version of `Polynomial.mapRingHom`.  -/
Polynomial.mapAlgHom : {R : Type u} →
  {A : Type z} →
    {B : Type u_2} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Polynomial A →ₐ[R] Polynomial B
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ), CochainComplex.HomComplex.δ n m 0 = 0
-- Mathlib.Data.Set.Opposite
Set.mem_unop : ∀ {α : Type u_1} {s : Set αᵒᵖ} {a : α}, a ∈ s.unop ↔ Opposite.op a ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [toIsMinimal : WeierstrassCurve.IsMinimal R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1 →
    (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ = 1 →
      WeierstrassCurve.HasMultiplicativeReduction R W