mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Simproc
/-- Returns `true`, if `@OfNat.ofNat α n inst` is the standard way we represent `Nat` numerals in Lean.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Simproc.0.Lean.Meta.Grind.Arith.isNormNatNum : Lean.Expr → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Topology.Separation.Hausdorff
tendsto_nhds_unique_of_eventuallyEq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X}
  [l.NeBot], Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → f =ᶠ[l] g → a = b
-- Lean.LibrarySuggestions.SymbolFrequency
/-- Return the number of times a `Name` appears
in the signatures of (non-internal) theorems in the current module,
skipping instance arguments and proofs.

Note that this is cached, and so returns the frequency within theorems that had been elaborated
when the function is first called (with any argument).
 -/
Lean.LibrarySuggestions.localSymbolFrequency : Lean.Name → Lean.MetaM ℕ
-- Init.Prelude
/-- Create syntax node with 2 children  -/
Lean.Syntax.node2 : Lean.SourceInfo → Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instOne : {α : Type u_1} → [CommGroup α] → [inst : Preorder α] → One (LowerSet α)
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.BVDecideConfig.mk.injEq : ∀ (timeout : ℕ)
  (trimProofs binaryProofs acNf andFlattening embeddedConstraintSubst structures fixedInt enums graphviz : Bool)
  (maxSteps : ℕ) (shortCircuit : Bool) (solverMode : Lean.Elab.Tactic.BVDecide.SolverMode) (timeout_1 : ℕ)
  (trimProofs_1 binaryProofs_1 acNf_1 andFlattening_1 embeddedConstraintSubst_1 structures_1 fixedInt_1 enums_1
    graphviz_1 : Bool)
  (maxSteps_1 : ℕ) (shortCircuit_1 : Bool) (solverMode_1 : Lean.Elab.Tactic.BVDecide.SolverMode),
  ({ timeout := timeout, trimProofs := trimProofs, binaryProofs := binaryProofs, acNf := acNf,
        andFlattening := andFlattening, embeddedConstraintSubst := embeddedConstraintSubst, structures := structures,
        fixedInt := fixedInt, enums := enums, graphviz := graphviz, maxSteps := maxSteps, shortCircuit := shortCircuit,
        solverMode := solverMode } =
      { timeout := timeout_1, trimProofs := trimProofs_1, binaryProofs := binaryProofs_1, acNf := acNf_1,
        andFlattening := andFlattening_1, embeddedConstraintSubst := embeddedConstraintSubst_1,
        structures := structures_1, fixedInt := fixedInt_1, enums := enums_1, graphviz := graphviz_1,
        maxSteps := maxSteps_1, shortCircuit := shortCircuit_1, solverMode := solverMode_1 }) =
    (timeout = timeout_1 ∧
      trimProofs = trimProofs_1 ∧
        binaryProofs = binaryProofs_1 ∧
          acNf = acNf_1 ∧
            andFlattening = andFlattening_1 ∧
              embeddedConstraintSubst = embeddedConstraintSubst_1 ∧
                structures = structures_1 ∧
                  fixedInt = fixedInt_1 ∧
                    enums = enums_1 ∧
                      graphviz = graphviz_1 ∧
                        maxSteps = maxSteps_1 ∧ shortCircuit = shortCircuit_1 ∧ solverMode = solverMode_1)
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- Constructor for `Adjunction.IsTriangulated`.
 -/
CategoryTheory.Adjunction.IsTriangulated.mk'' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated],
  adj.IsTriangulated
-- Mathlib.Data.ZMod.QuotientRing
/-- The **Chinese remainder theorem**, elementary version for `ZMod`. See also
`Mathlib/Data/ZMod/Basic.lean` for versions involving only two numbers.  -/
ZMod.prodEquivPi : {ι : Type u_3} →
  [inst : Fintype ι] →
    (a : ι → ℕ) → Pairwise (Function.onFun Nat.Coprime a) → ZMod (∏ i, a i) ≃+* ((i : ι) → ZMod (a i))
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_sup_sdiff' : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y
-- Mathlib.Algebra.Module.RingHom
/-- If the module action of `R` on `S` is compatible with multiplication on `S`, then
`fun x ↦ x • 1` is a ring homomorphism from `R` to `S`.

This is the `RingHom` version of `MonoidHom.smulOneHom`.

When `R` is commutative, usually `algebraMap` should be preferred.  -/
RingHom.smulOneHom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] → [inst_1 : NonAssocSemiring S] → [inst_2 : Module R S] → [IsScalarTower R S S] → R →+* S
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech adjunction.  -/
CategoryTheory.SimplicialObject.equivalenceLeftToRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      (X : CategoryTheory.SimplicialObject.Augmented C) →
        (F : CategoryTheory.Arrow C) →
          (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) → (X ⟶ F.augmentedCechNerve)
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex cosine function, defined via `exp`  -/
Complex.cos : ℂ → ℂ
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_not_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  (Filter.bliminf u f fun x => ¬p x) ⊓ Filter.bliminf u f p = Filter.liminf u f
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_iff_dist_eq' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P}, c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuot_ext' : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u₄}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop} (f g : RingQuot s →ₐ[S] B),
  f.comp (RingQuot.mkAlgHom S s) = g.comp (RingQuot.mkAlgHom S s) → f = g
-- Init.Data.String.Length
String.length_ofList : ∀ {l : List Char}, (String.ofList l).length = l.length
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqTheoremForm : BEq Mathlib.Meta.FunProp.TheoremForm
-- Init.Data.String.Lemmas.Basic
String.empty_ne_singleton : ∀ {c : Char}, "" ≠ String.singleton c
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_dvd_absNorm_of_le : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {I J : Ideal S},
  J ≤ I → Ideal.absNorm I ∣ Ideal.absNorm J
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedConfig.default : Mathlib.Meta.FunProp.Config
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.isArithFrobAt_localize : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) [inst_3 : Q.IsPrime],
  H.localize.IsArithFrobAt (IsLocalRing.maximalIdeal (Localization.AtPrime Q))
-- Lean.Linter.Deprecated
Lean.Linter.isDeprecated : Lean.Environment → Lean.Name → Bool
-- Mathlib.RingTheory.Localization.Ideal
/-- If `R` is a ring, then prime ideals in the localization at `M`
correspond to prime ideals in the original ring `R` that are disjoint from `M`  -/
IsLocalization.orderIsoOfPrime : {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] → { p // p.IsPrime } ≃o { p // p.IsPrime ∧ Disjoint ↑M ↑p }
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instSetLike.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective := ⋯ }
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_lt_opow_left_of_succ : ∀ {a b c : Ordinal.{u_1}}, a < b → a ^ Order.succ c < b ^ Order.succ c
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.ext_iff : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f g : P →ᴬ[R] Q},
  f = g ↔ ∀ (x : P), f x = g x
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.mk : (Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri) →
  (Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic)) →
    (Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)) →
      (Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit) →
        (Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit) →
          Std.Mutex (Lean.Server.ServerTask Unit) →
            Dynamic → IO.Ref Dynamic → Lean.Server.RequestHandlerCompleteness → Lean.Server.StatefulRequestHandler
-- Aesop.Index.RulePattern
/-- Get all substitutions of the rule patterns that match a subexpression of
`e`. Subexpressions containing bound variables are not considered. The returned
array may contain duplicates.  -/
Aesop.RulePatternIndex.getCore : Lean.Expr → Aesop.RulePatternIndex → Aesop.BaseM (Array (Aesop.RuleName × Aesop.Substitution))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {v : β k},
  t.WF → (Array.find? (fun x => compare x.fst k == Ordering.eq) t.toArray = some ⟨k, v⟩ ↔ t.get? k = some v)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.tr.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) (x : Γ) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ),
  Turing.TM1to0.tr M (some q, v) x = some (Turing.TM1to0.trAux M x q v)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The first inclusion of a pushout cocone.  -/
CategoryTheory.Limits.PushoutCocone.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Y} → {g : X ⟶ Z} → (t : CategoryTheory.Limits.PushoutCocone f g) → Y ⟶ t.pt
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.precompose_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {G : CategoryTheory.Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j)
  (naturality :
    ∀ {j j' : J} (f : j ⟶ j'),
      app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
        ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j),
  (c.precompose app naturality).ι = fun j => c.ι j ∘ app j
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.of.eq_1 : ∀ (M : Type u) [inst : Mul M], MagmaCat.of M = { carrier := M, str := inst }
-- Lean.Environment
/-- Context for `realizeConst` established by `enableRealizationsForConst`.  -/
_private.Lean.Environment.0.Lean.RealizationContext : Type
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_id : ∀ {X : BoolAlg}, BoolAlg.Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedLatticeHom.id ↑X
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (AddLocalization.addEquivOfQuotient f) (AddLocalization.mk x y) = f.mk' x y
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.mul_edist_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x y : α), (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.hpath_hext : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} {p₁ : Path x₀ x₁} {p₂ : Path x₂ x₃},
  (∀ (t : ↑unitInterval), p₁ t = p₂ t) → ⟦p₁⟧ ≍ ⟦p₂⟧
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.fst_apply : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (self : A × B), (NonUnitalStarAlgHom.fst R A B) self = self.1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isRevMatch_iff_isRevMatch_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch p pos ↔ String.Slice.Pattern.Model.IsRevMatch (fun x => decide (p x)) pos
-- Init.Data.List.Find
List.getLast_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (h : List.filterMap f l ≠ []),
  (List.filterMap f l).getLast h = (List.findSome? f l.reverse).get ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLT.toPosMulMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [PosMulReflectLT α], PosMulMono α
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.Regular]
  {x : ENNReal}, x ≠ ⊤ → (x • μ).Regular
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mkHom_f_succ_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'')
  (n : ℕ),
  (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.InducedCategory.isGroupoid : ∀ {C : Type u} (D : Type u₂) [inst : CategoryTheory.Category.{v, u₂} D] [CategoryTheory.IsGroupoid D] (F : C → D),
  CategoryTheory.IsGroupoid (CategoryTheory.InducedCategory D F)
-- Mathlib.Algebra.Homology.QuasiIso
CategoryTheory.ShortComplex.QuasiIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ φ_1 : S₁ ⟶ S₂),
  φ = φ_1 → CategoryTheory.ShortComplex.QuasiIso φ = CategoryTheory.ShortComplex.QuasiIso φ_1
-- Std.Time.DateTime.PlainDateTime
/-- Returns the week of the month for the given `PlainDateTime`, where weeks start on `firstDay`.
The first partial week containing day 1 is week 1, so weeks may span fewer than 7 days.
 -/
Std.Time.PlainDateTime.weekOfMonth : Std.Time.PlainDateTime → optParam Std.Time.Weekday Std.Time.Weekday.monday → Std.Time.Week.Ordinal
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instIsIsoFunctorUnitTopCatAdj : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  CategoryTheory.IsIso ContinuousGeneratedByCat.adj.unit
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- Relating the existing noncomputable `HasPullbacksAlong` typeclass to `ChosenPullbacksAlong`.  -/
CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y X : C} → (f : Y ⟶ X) → [CategoryTheory.Limits.HasPullbacksAlong f] → CategoryTheory.ChosenPullbacksAlong f
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.coe_mk : ∀ {K : Type u_1} [inst : Field K] {x : K} (hx : x ∈ integralClosure ℤ K), ↑⟨x, hx⟩ = x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsDomain R]
  (S : Submonoid R) [Module.IsTorsionFree R M], Module.IsTorsionFree (Localization S) (LocalizedModule S M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ΨSq 2 = W.Ψ₂Sq
-- Mathlib.Order.Filter.Map
Filter.map_eq_comap_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {n : β → α},
  m ∘ n = id → n ∘ m = id → Filter.map m f = Filter.comap n f
-- Mathlib.Data.NNReal.Basic
NNReal.natCast_iInf : ∀ {ι : Sort u_4} (f : ι → ℕ), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Mathlib.RingTheory.Radical.Basic
IsCoprime.divRadical : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a b : E}, IsCoprime a b → IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_minKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km),
  (Std.DTreeMap.Const.modify t k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Init.Data.SInt.Lemmas
Int16.ofIntClamp_int8ToInt : ∀ (x : Int8), Int16.ofIntClamp x.toInt = x.toInt16
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unwantedUnicode.inj : ∀ {c c_1 : Char},
  Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c = Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c_1 →
    c = c_1
-- Mathlib.Data.Matrix.Mul
/-- Left multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices.  -/
Matrix.addMonoidHomMulLeft : {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {α : Type v} → [inst : NonUnitalNonAssocSemiring α] → [Fintype m] → Matrix l m α → Matrix m n α →+ Matrix l n α
-- Init.Data.Array.Range
Array.range'_eq_append_iff : ∀ {s n : ℕ} {xs ys : Array ℕ},
  Array.range' s n = xs ++ ys ↔ ∃ k ≤ n, xs = Array.range' s k ∧ ys = Array.range' (s + k) (n - k)
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsClosedEmbedding g → Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding (g ∘ f)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withNewLocalInstanceImp : {α : Type} → Lean.Name → Lean.Expr → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Data.Multiset.Bind
Multiset.cons_product : ∀ {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β),
  (a ::ₘ s) ×ˢ t = Multiset.map (Prod.mk a) t + s ×ˢ t
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionData.mk.inj : ∀ {name : Lean.Name} {expr : Lean.Expr} {projNrs : List ℕ} {isDefault isPrefix : Bool} {name_1 : Lean.Name}
  {expr_1 : Lean.Expr} {projNrs_1 : List ℕ} {isDefault_1 isPrefix_1 : Bool},
  { name := name, expr := expr, projNrs := projNrs, isDefault := isDefault, isPrefix := isPrefix } =
      { name := name_1, expr := expr_1, projNrs := projNrs_1, isDefault := isDefault_1, isPrefix := isPrefix_1 } →
    name = name_1 ∧ expr = expr_1 ∧ projNrs = projNrs_1 ∧ isDefault = isDefault_1 ∧ isPrefix = isPrefix_1
-- Mathlib.RingTheory.LocalRing.Module
IsLocalRing.map_mkQ_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] {N₁ N₂ : Submodule R M},
  N₁ ≤ N₂ →
    N₂.FG →
      (Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₁ = Submodule.map (IsLocalRing.maximalIdeal R • N₂).mkQ N₂ ↔
        N₁ = N₂)
-- Mathlib.Analysis.Normed.Group.BallSphere
instContinuousNegElemBallOfNat : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ}, ContinuousNeg ↑(Metric.ball 0 r)
-- Std.Time.Zoned.TimeZone
/-- A zeroed `Timezone` representing GMT (no offset).
 -/
Std.Time.TimeZone.GMT : Std.Time.TimeZone
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.Repr.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {a : A} {ι : Type u_1} [inst_4 : SizeOf R] [inst_5 : SizeOf A] [inst_6 : SizeOf ι]
  (index : Finset ι) (left right : ι → A) (eq : ∑ i ∈ index, left i ⊗ₜ[R] right i = CoalgebraStruct.comul a),
  sizeOf { index := index, left := left, right := right, eq := eq } = 1 + sizeOf index + sizeOf eq
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.id_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} {a : M} (f : CategoryTheory.ShiftedHom X Y a),
  f.map (CategoryTheory.Functor.id C) = f
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.le_canonical : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical],
  J ≤ CategoryTheory.Sheaf.canonicalTopology C
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.algebraMap_toRingHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (self : P.Hom P') (x : P.Ring),
  (algebraMap P'.Ring S') (self.toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.unit_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : Monoid M] [inst_2 : Monoid N]
  [inst_3 : MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x), ↑⋯.unit = f ↑h.unit
-- Init.Data.Char.Ordinal
Char.succ?_eq : ∀ {c : Char}, c.succ? = Option.map Char.ofOrdinal (c.ordinal.addNat? 1)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.botEquivPUnit_apply : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : ↥⊥),
  Submodule.botEquivPUnit x = PUnit.unit
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β ≃ γ),
  (e.transEquiv f').target = ⇑f'.symm ⁻¹' e.target
-- Mathlib.Algebra.Order.Hom.Monoid
/-- An `OrderAddMonoidIso` respects `≤`.  -/
OrderAddMonoidIso.map_le_map_iff' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (self : α ≃+o β) {a b : α}, self.toFun a ≤ self.toFun b ↔ a ≤ b