mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Transport a `Functor.PushoutObjObj` structure via a natural isomorphism of functors.  -/
CategoryTheory.Functor.PushoutObjObj.ofNatIso : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₂ Y₂ : C₂} →
                    {f₂ : X₂ ⟶ Y₂} →
                      F.PushoutObjObj f₁ f₂ →
                        {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
                          (F ≅ F') → F'.PushoutObjObj f₁ f₂
-- Mathlib.Data.Finset.Piecewise
/-- `s.piecewise f g` is the function equal to `f` on the finset `s`, and to `g` on its
complement.  -/
Finset.piecewise : {ι : Type u_1} →
  {π : ι → Sort u_2} →
    (s : Finset ι) → ((i : ι) → π i) → ((i : ι) → π i) → [(j : ι) → Decidable (j ∈ s)] → (i : ι) → π i
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convOne_apply : ∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid C] [inst_4 : Module R C] [inst_5 : Coalgebra R C] (c : C),
  (WithConv.ofConv 1) c = (algebraMap R A) (CoalgebraStruct.counit c)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.mk : {ι : Type u_1} →
  (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex ι) →
    (∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex.faces) → AbstractSimplicialComplex ι
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the fourth quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open fourth quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open fourth quadrant
  for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the fourth quadrant.

Then `f` is equal to zero on the closed fourth quadrant.  -/
PhragmenLindelof.eq_zero_on_quadrant_IV : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ (x : ℝ), 0 ≤ x → f ↑x = 0) → (∀ x ≤ 0, f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | 0 ≤ z.re ∧ z.im ≤ 0}
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.toIsSemitopologicalRing : ∀ (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [IsTopologicalRing R],
  IsSemitopologicalRing R
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithTop.monotone_map_iff`. -/
Monotone.withTop_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (WithTop.map f)
-- Mathlib.Algebra.Group.NatPowAssoc
npow_mul_comm : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (m n : ℕ) (x : M),
  x ^ m * x ^ n = x ^ n * x ^ m
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.pushPending : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Unit
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.quot_one : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat),
  Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) MonCat.Colimits.Prequotient.one = 1
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.of_comp_left : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn (g ∘ f) s → IsLocalHomeomorphOn g (f '' s) → (∀ x ∈ s, ContinuousAt f x) → IsLocalHomeomorphOn f s
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_symm_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  (Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = Localization.mk x y
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The second projection from `PrimitiveAddChar`, giving the character.  -/
AddChar.PrimitiveAddChar.char : {R : Type u} →
  [inst : CommRing R] →
    {R' : Type v} →
      [inst_1 : Field R'] → (self : AddChar.PrimitiveAddChar R R') → AddChar R (CyclotomicField (↑self.n) R')
-- Mathlib.Topology.Sheaves.Skyscraper
/-- Taking stalks is the left adjoint of `skyscraperSheafFunctor ⋙ Sheaf.forget`. Useful
only when the fact that `skyscraperPresheafFunctor` factors through `Sheaf C X` is relevant.  -/
skyscraperSheafForgetAdjunction : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              TopCat.Presheaf.stalkFunctor C p₀ ⊣ (skyscraperSheafFunctor p₀).comp (TopCat.Sheaf.forget C X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X X_1 : C) (e_X : X = X_1) (Y Y_1 : C) (e_Y : Y = Y_1) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (X ⊞ Y) = (X_1 ⊞ Y_1)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.coe_subgroupMap_apply : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥H),
  ↑((e.subgroupMap H) g) = e ↑g
-- Std.Time.Format.Basic
Std.Time.FormatType : Type → Std.Time.FormatString → Type
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_eq_zero : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ}, 0 < p → ∀ {f : Polynomial R}, (Polynomial.expand R p) f = 0 ↔ f = 0
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_univ_pos : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ],
  0 < μ.real Set.univ
-- Mathlib.Algebra.Lie.Weights.Cartan
LieModuleHom.codRestrict.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (P : LieSubmodule R L N) (f f_1 : M →ₗ⁅R,L⁆ N) (e_f : f = f_1)
  (h : ∀ (m : M), f m ∈ P), LieModuleHom.codRestrict P f h = LieModuleHom.codRestrict P f_1 ⋯
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_reverse`. -/
List.SortedGT.reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT → l.reverse.SortedLT
-- Mathlib.Algebra.Group.Action.Defs
instIsLeftCancelSMulOfIsLeftCancelMul : ∀ (G : Type u_9) [inst : Mul G] [IsLeftCancelMul G], IsLeftCancelSMul G G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, (Std.ExtDTreeMap.Const.get? t a).isSome = true ↔ a ∈ t
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.smul_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {r : (CategoryTheory.End X)ᵐᵒᵖ} {f : X ⟶ Y},
  r • f = CategoryTheory.CategoryStruct.comp (MulOpposite.unop r) f
-- Mathlib.Algebra.Star.Basic
StarAddMonoid.mk : {R : Type u} →
  [inst : AddMonoid R] →
    [toInvolutiveStar : InvolutiveStar R] → (∀ (r s : R), star (r + s) = star r + star s) → StarAddMonoid R
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
IsIntegrallyClosed.of_iInf_eq_bot : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {ι : Type u_3} (S : ι → Subalgebra R K), (∀ (i : ι), IsIntegrallyClosed ↥(S i)) → ⨅ i, S i = ⊥ → IsIntegrallyClosed R
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CategoryTheory.Functor.instIsTriangulatedPlusMapHomotopyCategoryPlus : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C]
  [inst_7 : CategoryTheory.Limits.HasZeroObject D] [inst_8 : CategoryTheory.Limits.HasBinaryBiproducts D],
  F.mapHomotopyCategoryPlus.IsTriangulated
-- Mathlib.Algebra.Star.Conjneg
conjneg_ne_zero : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f : G → R},
  conjneg f ≠ 0 ↔ f ≠ 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Multiset.disjoint_finsetSum_left`. -/
Multiset.disjoint_finset_sum_left : ∀ {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α},
  Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_range_mapDomain_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β),
  Function.Injective f → ∀ (x : β →₀ M), x ∈ Set.range (Finsupp.mapDomain f) ↔ ∀ b ∉ Set.range f, x b = 0
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.isNonRecursive : Lean.Elab.PreDefinition → Bool
-- Mathlib.Data.Num.Basic
Num.pos.injEq : ∀ (a a_1 : PosNum), (Num.pos a = Num.pos a_1) = (a = a_1)
-- Mathlib.Logic.Function.FromTypes
/-- The type of `n`-ary functions `p 0 → p 1 → ... → p (n - 1) → τ`.  -/
Function.FromTypes : {n : ℕ} → (Fin n → Type u) → Type u → Type u
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instDecidableEqCode : DecidableEq Turing.ToPartrec.Code
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.output.injEq : ∀ (indent ticks indent_1 ticks_1 : ℕ),
  (Lean.Server.FileWorker.Hover.RWState.output✝ indent ticks =
      Lean.Server.FileWorker.Hover.RWState.output✝ indent_1 ticks_1) =
    (indent = indent_1 ∧ ticks = ticks_1)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabStateRefT : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instFloorRing : FloorRing ℝ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.foldrM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  t₁.Equiv t₂ → Std.DTreeMap.foldrM f init t₁ = Std.DTreeMap.foldrM f init t₂
-- Mathlib.Analysis.Calculus.Deriv.Pow
/-- Eta-expanded form of `deriv_pow` -/
deriv_fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), deriv (fun i => f i ^ n) x = ↑n * f x ^ (n - 1) * deriv f x
-- Init.Data.Int.Cooper
Int.Cooper.mul_resolve_left_inv_le : ∀ {b q : ℤ} (a p k : ℤ), 0 < a → b * k + b * p ≤ a * q → a ∣ k + p → b * Int.Cooper.resolve_left_inv a p k ≤ q
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- If `P : ProjectiveResolution Z` and `F : C ⥤ D` is an additive functor, this is
an isomorphism between `F.leftDerivedToHomotopyCategory.obj X` and the complex
obtained by applying `F` to `P.complex`.  -/
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {X : C} →
                (P : CategoryTheory.ProjectiveResolution X) →
                  (F : CategoryTheory.Functor C D) →
                    [inst_5 : F.Additive] →
                      F.leftDerivedToHomotopyCategory.obj X ≅
                        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                              (HomotopyCategory.quotient D (ComplexShape.down ℕ))).obj
                          P.complex
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_pos : ∀ (x : ℝ), 0 < x.sigmoid
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.comp_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : CategoryTheory.Arrow.LeftHomotopy f₁ g₁)
  (h₂ : CategoryTheory.Arrow.LeftHomotopy f₂ g₂),
  (h₁.comp h₂).hom =
    CategoryTheory.CategoryStruct.comp h₁.hom (CategoryTheory.Arrow.Hom.left f₂) +
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g₁) h₂.hom
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- If `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)`, and the
pushforward functor `Sheaf K A ⥤ Sheaf J A` is an equivalence, then this
is the equivalence `Sheaf K A ≌ Sheaf J A`.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              (A : Type u_4) →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [(G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, ⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.to_eq : ∀ {α : Type u_1} [inst : DivisionSemiring α] {n d : ℕ} {a n' d' : α},
  Mathlib.Meta.NormNum.IsNNRat a n d → ↑n = n' → ↑d = d' → a = n' / d'
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint : Inhabited Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (ci : Lean.Elab.ContextInfo) (mctxBefore mctxAfter : Lean.MetavarContext)
  (goalsTargetedBy goalsCreatedBy : List Lean.MVarId),
  sizeOf
      { stx := stx, ci := ci, mctxBefore := mctxBefore, mctxAfter := mctxAfter, goalsTargetedBy := goalsTargetedBy,
        goalsCreatedBy := goalsCreatedBy } =
    1 + sizeOf stx + sizeOf ci + sizeOf mctxBefore + sizeOf mctxAfter + sizeOf goalsTargetedBy + sizeOf goalsCreatedBy
-- Mathlib.Algebra.Order.Module.Defs
/-- Binary **rearrangement inequality**.  -/
smul_add_smul_le_smul_add_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
  [PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₁ ≤ a₂ → b₁ ≤ b₂ → a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂
-- Mathlib.Analysis.Quaternion
Quaternion.coe_real_complex_mul : ∀ (r : ℝ) (z : ℂ), r • ↑z = ↑r * ↑z
-- Mathlib.RingTheory.Localization.Pi
/-- If `S i` is a localization of `R i` at the submonoid `M i` for each `i`,
then `Π i, S i` is a localization of `Π i, R i` at the product submonoid.  -/
IsLocalization.instForallPiUniv : ∀ {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [inst : (i : ι) → CommSemiring (R i)]
  [inst_1 : (i : ι) → CommSemiring (S i)] [inst_2 : (i : ι) → Algebra (R i) (S i)] (M : (i : ι) → Submonoid (R i))
  [∀ (i : ι), IsLocalization (M i) (S i)], IsLocalization (Submonoid.pi Set.univ M) ((i : ι) → S i)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap'_f_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₀ : ι},
  (∀ (l : ι), ¬c.Rel k₀ l) →
    (∀ (l : ι), ¬c.Rel l k₀) → ∀ (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)), (Homotopy.nullHomotopicMap' h).f k₀ = 0
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : { p // p.IsPrime ∧ p ≤ I }),
  ↑↑((RelIso.symm (IsLocalization.AtPrime.orderIsoOfPrime S I)) a) =
    ⋂ s,
      ⋂ (_ :
        ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm a) ⊆
          ⇑(algebraMap R S) ⁻¹' ↑s),
        ↑s
-- Mathlib.Data.List.Dedup
List.subset_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l ⊆ l.dedup
-- Init.Data.UInt.Lemmas
USize.ofFin_mk : ∀ {n : ℕ} (hn : n < USize.size), USize.ofFin ⟨n, hn⟩ = USize.ofNatLT n hn
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.binaturality' : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β'),
  (fun {α} => η.app α) ∘ bitraverse f f' = bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f')
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M), Localization S = OreLocalization S M
-- Mathlib.Data.Finsupp.Basic
Finsupp.fst_sumFinsuppAddEquivProdFinsupp : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) (x : α),
  (Finsupp.sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)
-- Init.Data.List.Scan.Lemmas
List.scanrM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α₁ → α₂} {g : α₂ → β → m β} {as : List α₁},
  List.scanrM g init (List.map f as) = List.scanrM (fun a b => g (f a) b) init as
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instCoeWFWFInner : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → {t : Std.TreeMap.Raw α β cmp} → Coe t.WF t.inner.WF
-- Mathlib.Data.NNReal.Basic
NNReal.iSup_div : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), (⨆ i, f i) / a = ⨆ i, f i / a
-- Mathlib.Analysis.Normed.Group.Uniform
SeminormedAddCommGroup.toIsTopologicalAddGroup : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E], IsTopologicalAddGroup E
-- Mathlib.Data.List.TakeWhile
List.dropWhile_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p l[0] = true
-- Mathlib.FieldTheory.SeparableClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`separableClosure F K` if and only if `x` is contained in `separableClosure F E`.  -/
map_mem_separableClosure_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K) {x : E}, i x ∈ separableClosure F K ↔ x ∈ separableClosure F E
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_toUInt8 : ∀ (n : UInt32), n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasLimitsInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimits (CategoryTheory.Ind C)
-- Init.Data.List.Zip
List.map_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {l : List α} {l' : List β},
  List.map f (l.zip l') = List.zipWith (Function.curry f) l l'
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerTMulAlgEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : CommSemiring S] [inst_8 : Algebra R S] [inst_9 : Algebra S A]
  [inst_10 : IsScalarTower R S A] [inst_11 : Fintype m] [inst_12 : DecidableEq m]
  (x : Matrix (m × n) (m × n) (TensorProduct R A B)),
  (Matrix.kroneckerTMulAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x
-- Mathlib.Analysis.SpecificLimits.Fibonacci
/-- The limit of `fib (n + 1) / fib n` as `n → ∞` is the golden ratio.  -/
tendsto_fib_succ_div_fib_atTop : Filter.Tendsto (fun n => ↑(Nat.fib (n + 1)) / ↑(Nat.fib n)) Filter.atTop (nhds Real.goldenRatio)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.subgroupOrderIsoSubgroupMonoidHom.eq_1 : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)],
  CommGroup.subgroupOrderIsoSubgroupMonoidHom G M =
    { toFun := fun H => OrderDual.toDual (MonoidHom.domRestrictHom H Mˣ).ker,
      invFun := fun Φ =>
        (CommGroup.monoidHomMonoidHomEquiv G M).mapSubgroup (MonoidHom.domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Init.Data.Nat.Lcm
Nat.lcm_eq_mul_iff : ∀ {m n : ℕ}, m.lcm n = m * n ↔ m = 0 ∨ n = 0 ∨ m.gcd n = 1
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_lt_pow : ∀ {n k : ℕ}, n ≠ 0 → 2 ≤ k → n.choose k < n ^ k