mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.AsSubring
/-- The canonical map from a localization of `A` at `S` to the fraction ring
of `A`, given that `S ≤ A⁰`.  -/
Localization.mapToFractionRing : {A : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing A] →
      (S : Submonoid A) →
        [inst_1 : CommRing K] →
          [inst_2 : Algebra A K] →
            [IsFractionRing A K] →
              (B : Type u_3) →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra A B] → [IsLocalization S B] → S ≤ nonZeroDivisors A → B →ₐ[A] K
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.hashEMatchTheoremPtr.unsafe_1 : Lean.Meta.Grind.EMatchTheorem → UInt64
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.totalDegree 1 = 0
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommGroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCommGroup (f i)] → AddCommGroup ((i : I) → f i)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balanceₘ k v l r =
    if l.size + r.size ≤ 1 then Std.DTreeMap.Internal.Impl.bin k v l r
    else
      if h : r.size > Std.DTreeMap.Internal.delta * l.size then
        match r, h with
        | Std.DTreeMap.Internal.Impl.leaf, h => ⋯.elim
        | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr
      else
        if h_1 : l.size > Std.DTreeMap.Internal.delta * r.size then
          match l, h, h_1 with
          | Std.DTreeMap.Internal.Impl.leaf, h, h_2 => ⋯.elim
          | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_2 =>
            Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r
        else Std.DTreeMap.Internal.Impl.bin k v l r
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.congrOrderIso_symm : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N]
  (e : ArchimedeanClass M ≃o ArchimedeanClass N),
  (FiniteArchimedeanClass.congrOrderIso e).symm = FiniteArchimedeanClass.congrOrderIso e.symm
-- Mathlib.Order.Birkhoff
OrderEmbedding.supIrredLowerSet_surjective : ∀ {α : Type u_1} [inst : PartialOrder α] [Finite α], Function.Surjective ⇑OrderEmbedding.supIrredLowerSet
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {s : Set (((i : ι) → Em i) × G)},
  AnalyticOnNhd 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symmEquiv_symm_apply_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Add P] [inst_1 : Add Q] (h : Q ≃+ P) (a : P),
  ((AddEquiv.symmEquiv P Q).symm h) a = h.symm a
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ematch.sizeOf_spec : ∀ (k : Lean.Meta.Grind.EMatchTheoremKind), sizeOf (Lean.Meta.Grind.AttrKind.ematch k) = 1 + sizeOf k
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  f =o[𝕜; l] g → f =o[𝕜; l] (-g)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom (X.opcyclesIsoH f n₀ n₁ hn₁).inv =
    X.ιE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_toLatticeHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β),
  ⇑f.toLatticeHom = ⇑f
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.restrictScalars_symm_apply : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M₂),
  (LinearEquiv.restrictScalars R f).symm a = f.symm a
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.Hom.ext_iff : ∀ {R S : CommRingCat} {x y : R.Hom S}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Order.Bounds.Basic
/-- Adding a point to a set preserves its boundedness above.  -/
bddAbove_insert : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] {s : Set α} {a : α}, BddAbove (insert a s) ↔ BddAbove s
-- Mathlib.Probability.Kernel.Category.Stoch
/-- `Stoch` is the wide subcategory of `SFinKer` with Markov-kernel morphisms.  -/
Stoch : Type (u_1 + 1)
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.instIteratorLoop : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          {o : Type x → Type x'} →
            [inst : Monad n] →
              [Monad o] →
                [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.ULiftIterator α m n β lift) n o
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
AlternatingMap.ofSubsingleton.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} [inst_5 : Subsingleton ι] (i i_1 : ι),
  i = i_1 → AlternatingMap.ofSubsingleton R M N i = AlternatingMap.ofSubsingleton R M N i_1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
MulHom.eq_of_eqOn_dense : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {s : Set M},
  Subsemigroup.closure s = ⊤ → ∀ {f g : M →ₙ* N}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addScopedEntry : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → Lean.Name → β → Lean.Environment
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.Finite : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → ∀ [M.RankFinite], I.Finite
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_monomial_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R] (p₁ p₂ : MvPolynomial σ R)
  (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
  m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) =
    (MvPolynomial.monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      m.sPolynomial p₁ p₂
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instDecidableRelEquivOfDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableRel Ordnode.Equiv
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.differential.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ],
  P.differential = (P.basis.constr P.Ring) fun j i => (MvPolynomial.pderiv (P.map i)) (P.relation j)
-- Mathlib.Order.Category.PartOrd
PartOrd.ofHom_comp : ∀ {X Y Z : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] [inst_2 : PartialOrder Z] (f : X →o Y)
  (g : Y →o Z), PartOrd.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (PartOrd.ofHom f) (PartOrd.ofHom g)
-- Mathlib.Analysis.Convex.Function
/-- Right translation preserves concavity.  -/
ConcaveOn.translate_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f : E → β}, ConcaveOn 𝕜 s f → ∀ (c : E), ConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂.app T = T.mor₁
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.sup_span_singleton_eq_top_iff : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [Module.Finite K V]
  {W : Submodule K V} {v : V}, v ∉ W → (W ⊔ K ∙ v = ⊤ ↔ Module.finrank K (V ⧸ W) = 1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousMultilinear_norm_le' : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
  [inst_6 : Fintype ι] [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)]
  (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
  (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
  ‖f.mkContinuousMultilinear C H‖ ≤ max C 0
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.isVanKampen_isPullback_isPullback_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  {H : CategoryTheory.IsPushout f g h i},
  H.IsVanKampen →
    ∀ {X' Y' Z' : C} {h' : X' ⟶ Z'} {i' : Y' ⟶ Z'} {αX : X' ⟶ X} [CategoryTheory.Limits.HasPullback αX f] {αY : Y' ⟶ Y}
      {αZ : Z' ⟶ Z} {W : C} {f₁ f₂ : Z' ⟶ W},
      CategoryTheory.IsPullback h' αX αZ h →
        CategoryTheory.IsPullback i' αY αZ i →
          CategoryTheory.CategoryStruct.comp h' f₁ = CategoryTheory.CategoryStruct.comp h' f₂ →
            CategoryTheory.CategoryStruct.comp i' f₁ = CategoryTheory.CategoryStruct.comp i' f₂ → f₁ = f₂
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Given a function `U : ι → α` for `[CompleteLattice α]`,
`iInf U` provides a limit cone over `diagram U`.
 -/
CategoryTheory.Pairwise.coconeIsColimit : {ι : Type v} →
  {α : Type u} →
    (U : ι → α) → [inst : CompleteLattice α] → CategoryTheory.Limits.IsColimit (CategoryTheory.Pairwise.cocone U)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
/-- The `setToSimpleFunc` is equal to a sum over any set that includes `f.range` (except `0`).  -/
MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subset : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α}
  [inst_4 : DecidablePred fun x => x ≠ 0] (T : Set α → F →L[ℝ] F'),
  T ∅ = 0 →
    ∀ {f : MeasureTheory.SimpleFunc α F} {s : Finset F},
      {x ∈ f.range | x ≠ 0} ⊆ s → MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ s, (T (⇑f ⁻¹' {x})) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} {k fallback : α},
  t.WF → (Std.TreeSet.Raw.filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} {x y : P.Elements} (f : x ⟶ y)
  {Z : CategoryTheory.Functor Cᵒᵖ (Type (max (max v₂ w) v₁))} (h : F.op.comp (G.obj P) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ x)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ y) h
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using `sUnion`.  -/
MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S T : Set (Set α)},
  m0 = MeasurableSpace.generateFrom S →
    IsPiSystem S → T ⊆ S → T.Countable → ⋃₀ T = Set.univ → (∀ s ∈ T, μ s ≠ ⊤) → (∀ s ∈ S, μ s = ν s) → μ = ν
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher.default : {ρ : Type} → {pat : ρ} → {s : String.Slice} → String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s
-- Mathlib.NumberTheory.FLT.Three
/-- If `p : 𝓞 K` is a prime that divides both `S.a + η * S.b` and `S.a + η ^ 2 * S.b`, then `p`
is associated with `λ`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K},
  Prime p →
    p ∣
        FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
          ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
      p ∣
          FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
            ↑⋯.unit ^ 2 *
              FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) →
        Associated p (hζ.toInteger - 1)
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot : ∀ {α : Type u} [inst : SemilatticeSup α] [OrderBot α], CategoryTheory.Limits.HasFiniteColimits α
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Variant of `map_uliftYonedaEquiv` with general `g`. This is technically strictly more general
than `map_uliftYonedaEquiv`, but `map_uliftYonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error.  -/
CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} {F : CategoryTheory.Sheaf J (Type (max v v'))}
  (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- The property of objects that are the point of a colimit cocone for a
functor `F : J ⥤ C` where all objects `F.obj j` satisfy `P`.  -/
CategoryTheory.ObjectProperty.colimitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Action.Basic
/-- The morphism between the underlying objects of this action  -/
Action.Hom.hom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → {M N : Action V G} → M.Hom N → (M.V ⟶ N.V)
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddSubgroup.orderIsoAddCon_apply : ∀ {G : Type u_1} [inst : AddGroup G] (N : { N // N.Normal }), AddSubgroup.orderIsoAddCon N = QuotientAddGroup.con ↑N
-- Init.Data.Vector.Zip
Vector.take_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {n : ℕ} {as : Vector α n} {bs : Vector α_1 n}
  {i : ℕ}, (Vector.zipWith f as bs).take i = Vector.zipWith f (as.take i) (bs.take i)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_opow_aux₁ : ∀ {e a : ONote} [Ne : e.NF] [Na : a.NF] {a' : Ordinal.{0}},
  e.repr ≠ 0 →
    a' < Ordinal.omega0 ^ e.repr →
      a.repr = a' →
        ∀ (n : ℕ+), (Ordinal.omega0 ^ e.repr * ↑↑n + a') ^ Ordinal.omega0 = (Ordinal.omega0 ^ e.repr) ^ Ordinal.omega0
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeLTNat : (n : ℕ) → Fintype ↑{i | i < n}
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `f : M → N` is a homomorphism between two additive magmas,
then `AddMonoidAlgebra.mapDomain f` is a non-unital algebra homomorphism
between their additive magma algebras.  -/
AddMonoidAlgebra.mapDomainNonUnitalAlgHom : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Add M] → [inst_4 : Add N] → (M →ₙ+ N) → AddMonoidAlgebra A M →ₙₐ[R] AddMonoidAlgebra A N
-- Init.Data.String.Bootstrap
String.Internal.append : String → String → String
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.abs_discr_ge_of_isTotallyComplex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NumberField.IsTotallyComplex K],
  ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) /
      ((4 / Real.pi) ^ Module.finrank ℚ K * ↑(Module.finrank ℚ K).factorial ^ 2) ≤
    ↑|NumberField.discr K|
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.not_hasEigenvalue_zero_tfae : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M),
  [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) ≠ 0,
      LinearMap.det φ ≠ 0, LinearMap.ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.le_of_le_of_eq : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] {a b : α}, a ≤ 0 → b = 0 → a + b ≤ 0
-- Mathlib.Condensed.Discrete.Colimit
/-- The functor which takes a finite set to the set of maps into `F(*)` for a presheaf `F` on
`LightProfinite`.
 -/
LightCondensed.finYoneda : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u) → CategoryTheory.Functor FintypeCatᵒᵖ (Type u)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_add_add_eq_append : ∀ {m : ℤ} {n k : ℕ}, (m...m + ↑n + ↑k).toArray = (m...m + ↑n).toArray ++ ((m + ↑n)...m + ↑n + ↑k).toArray
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.addAction.eq_1 : ∀ {α : Type u_4} {M : Type u_5} [inst : AddMonoid α] [inst_1 : AddZeroClass M] [inst_2 : AddAction α M]
  [inst_3 : VAddAssocClass α M M] (c : AddCon M), c.addAction = { toVAdd := c.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_union_eq_right : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (∀ a ∈ s₁, a ∉ s₂ → f a = 0) → ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₂, f a
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instNontrivialRight : ∀ {𝕜 : Type u_3} {A : Type u_4} [Nonempty 𝕜] [Nontrivial A], Nontrivial (Unitization 𝕜 A)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_id : ∀ (R : Type u_1) {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜],
  ⇑(GradedAlgHom.id R 𝒜) = id
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_sub_iff_add_modEq' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b c : G}, a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The map from `P.P` to the product of two copies of `A`, when `P` is
a pre-path object for `A`. `P` shall be a *good* path object
when this morphism is a fibration.  -/
HomotopicalAlgebra.PrepathObject.p : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P : HomotopicalAlgebra.PrepathObject A) → [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] → P.P ⟶ A ⨯ A
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : CategoryTheory.Functor C Dᵒᵖ} (η : X ⟶ Y),
  (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.card_fixingSubgroup_eq_finrank : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  [FiniteDimensional F E] [IsGalois F E], Nat.card ↥K.fixingSubgroup = Module.finrank (↥K) E
-- Mathlib.Algebra.Ring.BooleanRing
RingHom.asBoolAlg_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : BooleanRing α] [inst_1 : BooleanRing β] (f : α →+* β) (a : AsBoolAlg α),
  f.asBoolAlg a = (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) a