mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.of_rank_eq_nat : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ},
  Module.rank K V = ↑n → FiniteDimensional K V
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then the L-series of `f - g` is zero for large real arguments.  -/
LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq : ∀ {f g : ℕ → ℂ},
  LSeries.abscissaOfAbsConv f < ⊤ →
    LSeries.abscissaOfAbsConv g < ⊤ →
      ((fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x) →
        (fun x => LSeries (f - g) ↑x) =ᶠ[Filter.atTop] 0
-- Lean.Meta.Tactic.TryThis
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.mkFailedToMakeTacticMsg : Lean.MessageData → Lean.MessageData → Lean.MessageData
-- Lean.Elab.ConfigEval.Types
/-- The original option name (without macro scopes), even after shifting.  -/
Lean.Elab.ConfigEval.ConfigItem.origOptionName : Lean.Elab.ConfigEval.ConfigItem → Lean.Name
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.smul_set_stabilizer_subset : ∀ {G : Type u_1} [inst : CommGroup G] {s : Set G} {a : G}, a ∈ s → a • ↑(MulAction.stabilizer G s) ⊆ s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inr_map_Ici_zero : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Unitization.inr '' Set.Ici 0 ⊆ Set.Ici 0
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonFunctor_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (D : Type u₂) [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {X Y : CategoryTheory.LaxBraidedFunctor C D} (α : X ⟶ Y) (A : CategoryTheory.CommMon C),
  ((CategoryTheory.Functor.mapCommMonFunctor C D).map α).app A =
    CategoryTheory.CommMon.homMk (CategoryTheory.Mon.Hom.mk' (α.hom.hom.app A.X) ⋯ ⋯)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_toMatrix₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b₁ b₂) B).SeparatingLeft ↔ B.SeparatingLeft
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n : A) (X : C),
  (CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
-- Mathlib.Algebra.Divisibility.Units
symm_isRelPrime : ∀ {α : Type u_1} [inst : CommMonoid α], Std.Symm IsRelPrime
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.scope : Aesop.RuleFilter → Aesop.ScopeName
-- Mathlib.Order.BoundedOrder.Basic
eq_bot_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a = ⊥ ↔ a ≤ ⊥
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv_apply : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B) (x : K),
  (IsFractionRing.semilinearEquivOfRingEquiv K L f) x = (IsFractionRing.ringEquivOfRingEquiv f) x
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk.eq_1 : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M],
  CommRing.Pic.mk R M =
    (equivShrink (CategoryTheory.Skeleton (SemimoduleCat R))ˣ)
      (Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Module.Finite.reprₛ R M)⟧
        ⟦SemimoduleCat.of R (Module.Dual R (Module.Finite.reprₛ R M))⟧ ⋯)
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.mk.sizeOf_spec : ∀ (candidates : Array Lean.Elab.Structural.RecArgCandidate) (report : Lean.MessageData),
  sizeOf { candidates := candidates, report := report } = 1 + sizeOf candidates + sizeOf report
-- Mathlib.CategoryTheory.ComposableArrows.Two
/-- Variant of `twoδ₂Toδ₁` for preorders.  -/
CategoryTheory.ComposableArrows.twoδ₂Toδ₁' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁) ⟶
            CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)
-- Mathlib.CategoryTheory.Yoneda
/-- `FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda.  -/
CategoryTheory.Functor.FullyFaithful.homNatIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          F.FullyFaithful →
            (X : C) →
              F.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj X))) ≅
                CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op X)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` reflects
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsColimit_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimit K.op F.op],
  CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} {x y : CategoryTheory.Quotient r},
  x.as = y.as → x = y
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Makes an ordered additive group isomorphism from a proof that the map preserves
addition.  -/
OrderAddMonoidIso.mk' : {α : Type u_2} →
  {β : Type u_3} →
    {x : AddCommGroup α} →
      {x_1 : Preorder α} →
        {x_2 : AddCommGroup β} →
          {x_3 : PartialOrder β} →
            (f : α ≃ β) → (∀ {a b : α}, f a ≤ f b ↔ a ≤ b) → (∀ (a b : α), f (a + b) = f a + f b) → α ≃+o β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_toArray_rio_push : ∀ {n : ℕ}, (*...=n).toArray = (*...n).toArray.push n
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.ofNat : ℕ → Lean.Meta.ProjReductionKind
-- Mathlib.Data.Finset.Density
Finset.dens_sdiff : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α} [inst_1 : DecidableEq α], s ⊆ t → (t \ s).dens = t.dens - s.dens
-- Mathlib.AlgebraicGeometry.Spec
/-- The spectrum of a commutative ring, as a topological space.
 -/
AlgebraicGeometry.Spec.topObj : CommRingCat → TopCat
-- Mathlib.SetTheory.Ordinal.Rank
/-- The rank of an element `a` under a well-founded relation `r` is defined recursively as the
smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that
`r b a`).  -/
IsWellFounded.rank : {α : Type u} → (r : α → α → Prop) → [hwf : IsWellFounded α r] → α → Ordinal.{u}
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(a • f, g) = a ^ {deg g} * Res(f, g)`.  -/
Polynomial.resultant_C_mul_left : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ) (r : R),
  (Polynomial.C r * f).resultant g m n = r ^ n * f.resultant g m n
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If we repeat a column of a matrix, we get a matrix of determinant zero.  -/
Matrix.det_updateCol_eq_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
  {i j : n}, i ≠ j → (M.updateCol j fun k => M k i).det = 0
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => min (f x) (g x)) a
-- Mathlib.Data.FunLike.Embedding
EmbeddingLike.mk : ∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [inst : FunLike F α β],
  (∀ (f : F), Function.Injective ⇑f) → EmbeddingLike F α β
-- Mathlib.Algebra.Homology.ExactSequence
/-- The isomorphism `S₁.sc' _ i j k ≅ S₂.sc' _ i j k` induced by an isomorphism `S₁ ≅ S₂`
in `ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.sc'MapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S₁ S₂ : CategoryTheory.ComposableArrows C n} →
          (S₁ ≅ S₂) →
            (h₁ : S₁.IsComplex) →
              (h₂ : S₂.IsComplex) →
                (i j k : ℕ) →
                  (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'MapIso._auto_1) →
                    (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'MapIso._auto_3) →
                      (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'MapIso._auto_5) →
                        S₁.sc' h₁ i j k hij hjk hk ≅ S₂.sc' h₂ i j k hij hjk hk
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.equivRing_x : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S), P.equivRing P.x = P.X
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.le_trim_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α},
  m₁ ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s
-- Mathlib.Algebra.BigOperators.Finprod
/-- `∏ᶠ x, f x` is notation for `finprod f`. It is the product of `f x`, where `x` ranges over the
multiplicative support of `f`, if it's finite, one otherwise. Taking the product over multiple
arguments or conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x`  -/
«term∏ᶠ_,_» : Lean.ParserDescr
-- Mathlib.Data.Multiset.MapFold
Multiset.map_le_map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α}, s ≤ t → Multiset.map f s ≤ Multiset.map f t
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.OptionT.bind.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given an `R`-algebra `A`, `mkPiAlgebra` is the multilinear map on `A^ι` associating
to `m` the product of all the `m i`.

See also `MultilinearMap.mkPiAlgebraFin` for a version that works with a non-commutative
algebra `A` but requires `ι = Fin n`.  -/
MultilinearMap.mkPiAlgebra : (R : Type uR) →
  (ι : Type uι) →
    [inst : CommSemiring R] →
      (A : Type u_1) →
        [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → [Fintype ι] → MultilinearMap R (fun x => A) A
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasSum_subtype_comap_iff_of_support_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α} {s : Set β},
  Function.support f ⊆ s →
    (HasSum (f ∘ Subtype.val) a (L.comap (Function.Embedding.subtype fun x => x ∈ s)) ↔ HasSum f a L)
-- Mathlib.Algebra.Module.Lattice
Submodule.span_range_eq_top_of_injective_of_rank_le : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {M N : Type u}
  [IsDomain R] [IsFractionRing R K] [inst_5 : AddCommGroup M] [inst_6 : Module R M] [inst_7 : AddCommGroup N]
  [inst_8 : Module R N] [inst_9 : Module K N] [IsScalarTower R K N] [Module.Finite K N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → Module.rank K N ≤ Module.rank R M → Submodule.span K ↑f.range = ⊤
-- Lean.Environment
_private.Lean.Environment.0.Lean.saveModuleData.unsafe_impl_2 : System.FilePath → Lean.Name → Lean.ModuleData → IO Lean.Compactor
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.widthInfty_mem_periods : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 𝒢.widthInfty ∈ 𝒢.periods
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instToStringAction : {β : Type u_1} → {α : Type u_2} → [ToString β] → [ToString α] → ToString (Std.Tactic.BVDecide.LRAT.Action β α)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The fundamental groupoid functor preserves products  -/
FundamentalGroupoidFunctor.preservesProduct : ∀ {I : Type u} (X : I → TopCat),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor X)
    FundamentalGroupoid.fundamentalGroupoidFunctor
-- Mathlib.Analysis.Asymptotics.Lemmas
Summable.mul_tendsto_const : ∀ {F : Type u_1} {ι : Type u_2} [inst : NormedRing F] [NormMulClass F] [NormOneClass F] [CompleteSpace F] {f g : ι → F},
  (Summable fun n => ‖f n‖) → ∀ {c : F}, Filter.Tendsto g Filter.cofinite (nhds c) → Summable fun n => f n * g n
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.zero_mul : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring A]
  (M : CStarMatrix m n A), 0 * M = 0
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.aemeasurable_fst : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨} {κ : ProbabilityTheory.Kernel 𝓧 𝓨},
  ProbabilityTheory.HasCondDistrib Y X κ P → AEMeasurable X P
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits : ∀ {A : Type u_1} {C : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A]
  [CategoryTheory.Limits.HasFiniteColimits A], CategoryTheory.HasExactLimitsOfShape J (CategoryTheory.Functor C A)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive left cancel semigroup, if it admits an
injective map that preserves `+` to an additive left cancel semigroup.  -/
Function.Injective.addLeftCancelSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : AddLeftCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddLeftCancelSemigroup M₁
-- Init.Data.Fin.Lemmas
Fin.mk_lt_mk : ∀ {n x y : ℕ} {hx : x < n} {hy : y < n}, ⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter!_eq_self_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ t →
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true →
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size = t.size
-- Mathlib.Topology.Algebra.Support
/-- If a family of functions `f` has locally-finite multiplicative support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
`f` are not equal to 1.  -/
LocallyFinite.exists_finset_nhds_mulSupport_subset : ∀ {X : Type u_1} {R : Type u_8} {ι : Type u_9} [inst : TopologicalSpace X] {U : ι → Set X} [inst_1 : One R]
  {f : ι → X → R},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    (∀ (i : ι), mulTSupport (f i) ⊆ U i) →
      (∀ (i : ι), IsOpen (U i)) →
        ∀ (x : X), ∃ is, ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.mulSupport fun i => f i z) ⊆ ↑is
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.DTreeMap.Const.ofList l cmp).size ≤ l.length
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, t.get? k = some v ↔ ∃ (h : k ∈ t), t.get k h = v
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the forward direction of `spectrum.zero_notMem_iff`. -/
spectrum.isUnit_of_zero_notMem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  0 ∉ spectrum R a → IsUnit a
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorization.map_ne_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A} {f : Polynomial A}
  {h : PowerSeries A}, g.IsWeierstrassFactorization f h → (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Icc : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.Icc x y) = ENNReal.ofReal (↑y - ↑x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (p : (a : α) × β a)
  (h_1 : Unit → motive none) (h_2 : (p : (a : α) × β a) → motive (some p)),
  (match some p with
    | none => h_1 ()
    | some p => h_2 p) =
    h_2 p
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instAddCommMonoid : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → AddCommMonoid (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The isomorphism `(K.extend e).cycles j' ≅ K.cycles j` when `e.f j = j'`.  -/
HomologicalComplex.extendCyclesIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {j : ι} →
                      {j' : ι'} →
                        e.f j = j' →
                          [inst_3 : K.HasHomology j] →
                            [inst_4 : (K.extend e).HasHomology j'] → (K.extend e).cycles j' ≅ K.cycles j
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y), (I.map f).comap f ≤ I
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [LocallyCompactSpace M], LocallyCompactSpace Mᵈᵃᵃ
-- Mathlib.Computability.TuringMachine.Computable
/-- The step function corresponding to this TM.  -/
Turing.FinTM2.step : (tm : Turing.FinTM2) → tm.Cfg → Option tm.Cfg
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_push : ∀ {m n : ℤ}, m ≤ n → (m...=n).toArray = (m...n).toArray.push n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).inr =
    CategoryTheory.Limits.BinaryFan.IsLimit.lift ht 0 (CategoryTheory.CategoryStruct.id Y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instZSMul : {M : Type uM} → {N : Type uN} → [inst : AddZeroClass M] → [inst_1 : AddCommGroup N] → SMul ℤ (M →+ N)
-- Init.Data.List.Basic
List.reverseAux_eq_append : ∀ {α : Type u} {as bs : List α}, as.reverseAux bs = as.reverseAux [] ++ bs
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_filterWithPostcondition : ∀ {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad n Pred EPred] [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.Iter β} {P : Pred}
  {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← (f b).run
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.filterWithPostcondition f it) ⦃ Q; eQ ⦄
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExpr.formatter : Lean.PrettyPrinter.Formatter
-- Std.Http.Data.URI.Basic
/-- Origin-form request target (most common for HTTP requests). Consists of a path and an optional query string.
Example: `/path/to/resource?key=value`
 -/
Std.Http.RequestTarget.originForm : Std.Http.URI.Path → Option Std.Http.URI.Query → Std.Http.RequestTarget
-- Mathlib.CategoryTheory.Limits.Cones
/-- The category of cones on `F` is equivalent to the opposite category of
the category of cocones on the opposite of `F`.
 -/
CategoryTheory.Limits.coneEquivalenceOpCoconeOp : {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.Cone F ≌ (CategoryTheory.Limits.Cocone F.op)ᵒᵖ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
vector angle form.  -/
Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ y → ‖x‖ = ‖y‖ → o.oangle y x = ↑Real.pi - 2 • o.oangle (y - x) y
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.tower_top : ∀ (K : Type u_1) (L : Type u_2) (M : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [IsScalarTower K L M] [IsAbelianGalois K M],
  IsAbelianGalois L M
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_le_iff_le : ∀ {a b : ℕ} (ha : a < UInt64.size) (hb : b < UInt64.size), UInt64.ofNatLT a ha ≤ UInt64.ofNatLT b hb ↔ a ≤ b
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The generators of the upper Borel subalgebra.  -/
LieAlgebra.Basis.e : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] → [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → ι → L
-- Init.Data.Option.Basic
/-- `none ~ none`  -/
Option.Rel.none : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Option.Rel r none none
-- Mathlib.Data.List.Sigma
List.mem_keys_of_mem : ∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, s ∈ l → s.fst ∈ l.keys