mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_bijective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂], Function.Bijective AffineIsometryEquiv.symm
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_sumCoords : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), ⇑b.sumCoords = fun m => (b.repr m).sum fun x => id
-- Init.Core
/-- `return (b : β) s` means that the block exited via a `return b` early-exit command  -/
DoResultPR.return : {α β σ : Type u} → β → σ → DoResultPR α β σ
-- Lean.Elab.Calc
Lean.Elab.Term.instInhabitedCalcStepView.default : Lean.Elab.Term.CalcStepView
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.hasTerminal : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} [G.Faithful] [G.Full] {Y : A},
  CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G (G.obj Y))
-- Mathlib.Data.Set.Basic
Set.Subset.antisymm : ∀ {α : Type u} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
-- Mathlib.Order.SuccPred.Basic
WithTop.succ_coe_of_not_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : (a : α) → Decidable (Order.succ a = a)]
  {a : α}, ¬IsMax a → Order.succ ↑a = ↑(Order.succ a)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The canonical projection `∐ I.right ⟶ multicoequalizer I`.  -/
CategoryTheory.Limits.Multicoequalizer.sigmaπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] →
          [CategoryTheory.Limits.HasCoproduct I.left] →
            [inst_3 : CategoryTheory.Limits.HasCoproduct I.right] → ∐ I.right ⟶ CategoryTheory.Limits.multicoequalizer I
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly : BEq Int.Internal.Linear.Poly
-- Mathlib.Algebra.Group.Prod
Prod.isAddUnit_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] {x : M × N},
  IsAddUnit x ↔ IsAddUnit x.1 ∧ IsAddUnit x.2
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddCon.instCompleteLattice =
    { toSemilatticeSup := (completeLatticeOfInf (AddCon M) ⋯).toSemilatticeSup,
      inf := fun c d => { toSetoid := c.toSetoid ⊓ d.toSetoid, add' := ⋯ }, inf_le_left := ⋯, inf_le_right := ⋯,
      le_inf := ⋯, toSupSet := (completeLatticeOfInf (AddCon M) ⋯).toSupSet, isLUB_sSup := ⋯,
      toInfSet := (completeLatticeOfInf (AddCon M) ⋯).toInfSet, isGLB_sInf := ⋯,
      top :=
        let __src := ⊤;
        { toSetoid := __src, add' := ⋯ },
      le_top := ⋯,
      bot :=
        let __src := ⊥;
        { toSetoid := __src, add' := ⋯ },
      bot_le := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The natural inclusion `B₁(G, A) →ₗ[k] Z₁(G, A)`.  -/
groupHomology.boundariesToCycles₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ↥(groupHomology.boundaries₁ A) →ₗ[k] ↥(groupHomology.cycles₁ A)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates limits, then `F : C ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.push_end_proc : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  0 ≤ᵐ[μ.restrict s] f →
    MeasureTheory.IntegrableOn f s μ → (0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s))
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates finite colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteLimits F.op
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_le_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} [L.NeBot],
  (∀ (i : ι), f i ≤ g i) → Multipliable f L → Multipliable g L → ∏'[L] (i : ι), f i ≤ ∏'[L] (i : ι), g i
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.instInhabitedGuessNameData.default : Mathlib.Tactic.GuessName.GuessNameData
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Subgroup.copy : {G : Type u_1} → [inst : Group G] → (K : Subgroup G) → (s : Set G) → s = ↑K → Subgroup G
-- Batteries.Lean.AttributeExtra
Lean.ParametricAttributeExtra.mk : {α : Type} → Lean.ParametricAttribute α → Std.HashMap Lean.Name α → Lean.ParametricAttributeExtra α
-- Mathlib.Analysis.Asymptotics.TVS
/-- `f =O[𝕜; l] g` (`IsBigOTVS 𝕜 l f g`) is a generalization of `f =O[l] g` (`IsBigO l f g`)
that works in topological `𝕜`-vector spaces.

Given two functions `f` and `g` taking values in topological vector spaces
over a normed field `𝕜`,
we say that $f = O(g)$ if for any neighborhood of zero `U` in the codomain of `f`
there exists a neighborhood of zero `V` in the codomain of `g`
such that $\operatorname{gauge}_{K, U} (f(x)) \le \operatorname{gauge}_{K, V} (g(x))$,
where $\operatorname{gauge}_{K, U}(y) = \inf \{‖c‖ \mid y ∈ c • U\}$.
 -/
Asymptotics.IsBigOTVS : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [ENorm 𝕜] →
          [TopologicalSpace E] →
            [TopologicalSpace F] → [Zero E] → [Zero F] → [SMul 𝕜 E] → [SMul 𝕜 F] → Filter α → (α → E) → (α → F) → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
/-- The natural isomorphism `(K⟦n⟧).homology a ≅ K.homology a'` when `n + a = a'`.  -/
CochainComplex.ShiftSequence.shiftIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CategoryWithHomology C] →
        (n a a' : ℤ) →
          n + a = a' →
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp
                (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a) ≅
              HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a')
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.destruct_join.aux.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2)
  (h_1 : Unit → motive none) (h_2 : (s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))),
  (match none with
    | none => h_1 ()
    | some (s, S) => h_2 s S) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `X` represents a presheaf of additive monoids, then `X` is an additive monoid object.  -/
CategoryTheory.AddGrpObj.ofRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) →
          (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X → CategoryTheory.AddGrpObj X
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distances between two sets and their closures coincide.  -/
Metric.hausdorffDist_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  Metric.hausdorffDist (closure s) (closure t) = Metric.hausdorffDist s t
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- Let `S` be a Dedekind domain that is torsion-free over a domain `R`, and let `p ≠ ⊥` be an
ideal of `R`. Then `p` is unramified in `S` if and only if `S` is unramified at every maximal
ideal `P` of `S` lying over `p`.

See `Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain` if `R` is of characteristic zero.  -/
Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [IsDedekindDomain S] [Module.IsTorsionFree R S] {p : Ideal R},
  p ≠ ⊥ → (Algebra.IsUnramifiedIn S p ↔ ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → Algebra.IsUnramifiedAt R P)
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- If `f` is a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, then for every
`n : ℕ` and `a : α`, we have `f (n • a) ≤ (f a)`.  -/
IsNonarchimedean.nsmul_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddMonoid α]
  [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {n : ℕ} {a : α}, f (n • a) ≤ f a
-- Aesop.Tree.ExtractScript
Aesop.extractSafePrefixScript : Aesop.TreeM (Aesop.Script.UScript × Bool)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, this is the quotient map
`Ker(ρ(g) - Id(A)) ⟶ Ker(ρ(g) - Id(A))/Im(N) ≅ Hᵢ(G, A)` for any odd `i`.  -/
Rep.FiniteCyclicGroup.groupHomologyπOdd : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            [DecidableEq G] →
              (∀ (x : G), x ∈ Subgroup.zpowers g) →
                (i : ℕ) →
                  Odd i →
                    (ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶
                      groupHomology A i)
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.IsRightDerivedFunctor.mk : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  {RF : CategoryTheory.Functor D H} {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {α : F ⟶ L.comp RF} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W],
  RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W
-- Mathlib.Topology.Algebra.Group.Basic
/-- The topological closure of a normal subgroup is normal.  -/
Subgroup.is_normal_topologicalClosure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (N : Subgroup G)
  [N.Normal], N.topologicalClosure.Normal
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.map_stabilizer_le : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (f : G →* H) (s : Set G),
  Subgroup.map f (MulAction.stabilizer G s) ≤ MulAction.stabilizer H (⇑f '' s)
-- Mathlib.Algebra.GroupWithZero.Basic
inv_mul_cancel_left₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b : G₀), a⁻¹ * (a * b) = b
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_le : ∀ {r : ENNReal} {n : ℕ∞}, ⌈r⌉ₑ ≤ n ↔ r ≤ ↑n
-- Init.Data.List.Basic
/-- All elements of the empty list are vacuously pairwise related.  -/
List.Pairwise.nil : ∀ {α : Type u} {R : α → α → Prop}, List.Pairwise R []
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr'_symm_apply_right : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (x : N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂),
  ((SemidirectProduct.congr' fn fg).symm x).right = fg.symm x.right
-- Init.GetElem
Fin.instGetElemFinVal : {cont : Type u_1} →
  {elem : Type u_2} →
    {dom : cont → ℕ → Prop} → {n : ℕ} → [GetElem cont ℕ elem dom] → GetElem cont (Fin n) elem fun xs i => dom xs ↑i
-- Lean.Message
/-- Creates message data wrapping `fmt` that gives information about `expr` when hovered over.

Options:
- `location?` overrides what "go to definition" does
- `docString?` allows overriding the docstring for the expression
- `mkDocString?` allows generating a dynamic docstring; if this is provided, `docString?` is ignored
- `explicit` makes the hover pretty print the head application in explicit mode;
  the default value is `false` (note: delaboration expression hovers normally set this to `true`,
  since their purpose is to get more information about a given expression)
 -/
Lean.MessageData.withExprHover : Std.Format →
  Lean.Expr →
    Lean.LocalContext →
      optParam (Option Lean.DeclarationLocation) none →
        optParam (Option String) none →
          optParam (Option (Lean.PPContext → IO String)) none → optParam Bool false → Lean.MessageData
-- Mathlib.Order.Filter.Germ.Basic
Filter.Product.instInhabited : {α : Type u_1} → {l : Filter α} → {ε : α → Type u_5} → [(a : α) → Inhabited (ε a)] → Inhabited (l.Product ε)
-- Aesop.Builder.Forward
_private.Aesop.Builder.Forward.0.Aesop.RuleBuilder.getImmediatePremises.isPatternInstantiated : Option Aesop.RulePattern → ℕ → Bool
-- Std.Data.ExtDHashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtDHashMap.modify : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → (β a → β a) → Std.ExtDHashMap α β
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul : ∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) →
    ∀ {p : ℝ}, 0 < p → MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ
-- Init.Prelude
/-- If this is an `ident`, return the parsed value, else `.anonymous`.  -/
Lean.Syntax.getId : Lean.Syntax → Lean.Name
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Subgroups of the subgroup `H` are considered as subgroups that are less than or equal to
`H`.  -/
Subgroup.MapSubtype.orderIso : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Subgroup ↥H ≃o { H' // H' ≤ H }
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter'.match_1.eq_1 : ∀ {α : Type u_1} (motive : α → List α → Sort u_2) (a : α) (h_1 : (a : α) → motive a [])
  (h_2 : (a h : α) → (l : List α) → motive a (h :: l)),
  (match a, [] with
    | a, [] => h_1 a
    | a, h :: l => h_2 a h l) =
    h_1 a
-- Init.Prelude
Sub.mk : {α : Type u} → (α → α → α) → Sub α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.instAlgebraSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : Field A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : Field C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → Algebra ↥A[b] ↥A⟮(algebraMap B C) b⟯
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.analyticAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {z : E} {s : Set E},
  s ∈ nhds z → AnalyticOn 𝕜 f s → AnalyticAt 𝕜 f z
-- Mathlib.Algebra.Order.Floor.Div
/-- Ceiling division. If `a > 0`, then `b ⌈/⌉ a` is the least `c` such that `b ≤ a • c`.  -/
CeilDiv.ceilDiv : {α : Type u_2} →
  {β : Type u_3} →
    {inst : AddCommMonoid α} →
      {inst_1 : PartialOrder α} →
        {inst_2 : AddCommMonoid β} →
          {inst_3 : PartialOrder β} → {inst_4 : SMulZeroClass α β} → [self : CeilDiv α β] → β → α → β
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.adjoint_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] [inst_9 : FiniteDimensional 𝕜 E]
  [inst_10 : FiniteDimensional 𝕜 F] [inst_11 : FiniteDimensional 𝕜 G] [inst_12 : FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F)
  (g : G →ₗ[𝕜] H),
  LinearMap.adjoint (TensorProduct.map f g) = TensorProduct.map (LinearMap.adjoint f) (LinearMap.adjoint g)
-- Mathlib.Data.Int.Init
Int.gcd_negSucc_negSucc : ∀ (m n : ℕ), (Int.negSucc m).gcd (Int.negSucc n) = (m + 1).gcd (n + 1)
-- Lean.LocalContext
Lean.LocalDecl.setUserName : Lean.LocalDecl → Lean.Name → Lean.LocalDecl
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The center of an algebra is the set of elements which commute with every element. They form a
subalgebra.  -/
Subalgebra.center : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A
-- Mathlib.Topology.Constructions.SumProd
/-- **Alias** of `IsClosed.setOfPred_mapsTo`.

---

If `f x y` is continuous in `x` for all `y ∈ s`,
then the set of `x` such that `f x` maps `s` to `t` is closed.  -/
IsClosed.setOf_mapsTo : ∀ {X : Type u} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {α : Type u_5} {f : X → α → Z}
  {s : Set α} {t : Set Z}, IsClosed t → (∀ a ∈ s, Continuous fun x => f x a) → IsClosed {x | Set.MapsTo (f x) s t}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A minimal Weierstrass equation has multiplicative reduction if and only if
the valuation of its discriminant is less than 1 and the valuation of `a₄` equals 1.  -/
WeierstrassCurve.HasMultiplicativeReduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Mathlib.Topology.NhdsWithin
nhdsWithin_subtype : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (a : { x // x ∈ s }) (t : Set { x // x ∈ s }),
  nhdsWithin a t = Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' t))
-- Init.Data.Vector.Lemmas
Vector.foldr_toList : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β → β) {init : β} {xs : Vector α n},
  List.foldr f init xs.toList = Vector.foldr f init xs
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊆ Set.Ici b ↔ b ≤ a
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_univ : ∀ {α : Type u} [inst : Semiring α], Ideal.span Set.univ = ⊤
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] (X : A),
  (CategoryTheory.Abelian.LeftResolution.karoubi.π Λ).app ((CategoryTheory.Idempotents.toKaroubi A).obj X) =
    (CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ).app X
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_sdiff_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
-- Lean.Compiler.ExternAttr
Lean.isExtern : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` equalizes the two maps  -/
CategoryTheory.RegularMono.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.RegularMono f),
  CategoryTheory.CategoryStruct.comp f self.left = CategoryTheory.CategoryStruct.comp f self.right
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.of_mul_left : ∀ {R : Type u_1} [inst : Monoid R] {m n : R}, Squarefree (m * n) → Squarefree m
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_toBilin : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁) (M : Matrix n n R₁),
  (LinearMap.BilinForm.toMatrix b) ((Matrix.toBilin b) M) = M
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_const_left : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => C * f x) l Filter.atTop
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.discr_odd_prime' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p),
  p ≠ 2 → Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj : ∀ {R : CommRingCat} {U : (AlgebraicGeometry.Spec R).Opens},
  algebraMap ↑R ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op U)) =
    CommRingCat.Hom.hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
        ((AlgebraicGeometry.Spec R).presheaf.map (CategoryTheory.homOfLE ⋯).op))
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodComm_apply : ∀ (R₁ : Type u_1) [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  (M₂ : Type u_5) [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] (a : M₁ × M₂), (ContinuousLinearEquiv.prodComm R₁ M₁ M₂) a = a.swap
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_union_mul_inter : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (f : α → M) (s t : Set α),
  (s ∪ t).mulIndicator f * (s ∩ t).mulIndicator f = s.mulIndicator f * t.mulIndicator f
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.DTreeMap.getKeyLT! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α → α
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.scopedEntries : {α β σ : Type} → Lean.ScopedEnvExtension.StateStack α β σ → Lean.ScopedEnvExtension.ScopedEntries β
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- **Alias** of `Filter.tendsto_atTop_finset_of_monotone`.

---

If `f` is a monotone sequence of `Finset`s and each `x` belongs to one of `f n`, then
`Tendsto f atTop atTop`.  -/
Monotone.tendsto_atTop_finset : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : β → Finset α},
  Monotone f → (∀ (x : α), ∃ n, x ∈ f n) → Filter.Tendsto f Filter.atTop Filter.atTop