mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent.eq_1 : ∀ {A : Type u_1} (M : Type u_2) [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M] [inst_2 : Module A M],
  Ideal.primaryComponent M I = ⨆ i, Submodule.torsionBySet A M ↑(I ^ i)
-- Init.Prelude
/-- The implementation of `a <<< b : α`. See `HShiftLeft`.  -/
ShiftLeft.shiftLeft : {α : Type u} → [self : ShiftLeft α] → α → α → α
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {b : β}, s +ᵥ {b} = (fun x => x +ᵥ b) '' s
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The underlying set of a term of a `OneMemClass` is nonempty.  -/
OneMemClass.coe_nonempty : ∀ {S : Type u_3} {M : Type u_4} [inst : One M] [inst_1 : SetLike S M] [OneMemClass S M] (s : S), (↑s).Nonempty
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare} {k : α}
  {f : β → β} {fallback : α}, compare ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.RingTheory.Flat.Basic
/-- An `R`-module `M` is flat if for every finitely generated submodule `N` of every
finitely generated `R`-module `P` in the same universe as `R`,
the canonical map `N ⊗ M → P ⊗ M` is injective. This implies the same is true for
arbitrary `R`-modules `N` and `P` and injective linear maps `N →ₗ[R] P`, see
`Flat.rTensor_preserves_injective_linearMap`. To show a module over a ring `R` is flat, it
suffices to consider the case `P = R`, see `Flat.iff_rTensor_injective`.  -/
Module.Flat : (R : Type u) → (M : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dualProdDualEquivDual_symm_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (M' : Type u_4)
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M × M' →ₗ[R] R),
  (Module.dualProdDualEquivDual R M M').symm f = (f ∘ₗ LinearMap.inl R M M', f ∘ₗ LinearMap.inr R M M')
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_symm_nhdsWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    Filter.map (↑(extChartAt I x).symm)
        (nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)) =
      nhdsWithin y s
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsEquivalenceFunctorInv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [inst_2 : Φ.functor.IsEquivalence] [inst_3 : Φ.IsInduced] [inst_4 : W₂.RespectsIso], Φ.inv.functor.IsEquivalence
-- Mathlib.FieldTheory.IsRealClosed.Basic
/-- A field `R` is real closed if all of the following hold:
1. `R` is real (that is, `-1` is not a sum of squares in `R`).
2. for every `x` in `R`, one of `x` or `-x` is a square.
3. every odd-degree polynomial over `R` has a root in `R`.
 -/
IsRealClosed : (R : Type u_1) → [Field R] → Prop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeUnop.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop),
  CategoryTheory.Limits.coconeOfConeUnop c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.removeUnop c.π }
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Iic_val : ∀ {n : ℕ} (i : Fin n), Fin.val ⁻¹' Set.Iic ↑i = Set.Iic i
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- See note [partially-applied ext lemmas].  -/
AddMonoidAlgebra.bialgHom_ext' : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : AddMonoid M]
  ⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B⦄,
  (↑φ₁).comp (AddMonoidAlgebra.of A M) = (↑φ₂).comp (AddMonoidAlgebra.of A M) →
    (↑φ₁).comp AddMonoidAlgebra.singleZeroAlgHom = (↑φ₂).comp AddMonoidAlgebra.singleZeroAlgHom → φ₁ = φ₂
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Ici : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b : M), (fun x => x + a) '' Set.Ici b = Set.Ici (b + a)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.fiberEquivGroup_smul_self : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x}))
  {e' : ↑(f ⁻¹' {x})}, (hf.fiberEquivGroup e) e' • ↑e = ↑e'
-- Mathlib.Algebra.Order.Sum
Sum.elim_le_one_iff : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [inst : LE β] [inst_1 : One β] {v₁ : α₁ → β} {v₂ : α₂ → β},
  Sum.elim v₁ v₂ ≤ 1 ↔ v₁ ≤ 1 ∧ v₂ ≤ 1
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R], IsJacobsonRing (Polynomial R) ↔ IsJacobsonRing R
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ)
  (ll : List ((a : α) × β a)) (m : Std.DTreeMap.Internal.Impl α β)
  (hm : Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true)
  (rr : List ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll m hm rr =
    match m, hm with
    | Std.DTreeMap.Internal.Impl.leaf, hm => f ll Std.DTreeMap.Internal.Cell.empty ⋯ rr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r, hm =>
      match h : k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll l_1 ⋯ (⟨k', v'⟩ :: r.toListModel ++ rr)
      | Ordering.eq => f (ll ++ l_1.toListModel) (Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯) ⋯ (r.toListModel ++ rr)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.applyPartition.go k l f (ll ++ l_1.toListModel ++ [⟨k', v'⟩]) r ⋯ rr
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.le_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α), m ≤ m.trim
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeatTR.loop.eq_2 : ∀ {α : Type u} (f : α → α) (x : α) (n : ℕ), Nat.repeatTR.loop✝ f n.succ x = Nat.repeatTR.loop✝ f n (f x)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_trans_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : Z), (f.trans g).symm z = f.symm (g.symm z)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {X Y : B × C}
  (a : X ⟶ Y), (CategoryTheory.Bicategory.Prod.snd B C).map a = a.2
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.HasProd.flip : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [μ.HasProd ν B],
  ν.HasProd μ B.flip
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_two_mul' : ∀ (x : ℂ), Complex.cos (2 * x) = Complex.cos x ^ 2 - Complex.sin x ^ 2
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4OfSize_shrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.AB4OfSize.{max w w', v, u} C], CategoryTheory.AB4OfSize.{w, v, u} C
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_pow_iff_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ}
  [ZeroLEOneClass M₀], 0 ≤ a → n ≠ 0 → (1 < a ^ n ↔ 1 < a)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_mul_cancel : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {x y z : R}, ¬z ≤ᵥ 0 → x * z ≤ᵥ y * z → x ≤ᵥ y
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_eq_card_nsmul : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (m : β), (∀ x ∈ s, f x = m) → s.noncommSum f comm = s.card • m
-- Mathlib.RingTheory.LocalProperties.Basic
/-- Let `S` be an `R`-algebra and `Sᵣ` and `Rᵣ` be the respective localizations at a submonoid
`M` of `R`. If `P` is stable under base change and `P` holds for `algebraMap R S`, then
`P` holds for `algebraMap Rᵣ Sᵣ`.  -/
RingHom.IsStableUnderBaseChange.of_isLocalization : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.IsStableUnderBaseChange P →
    ∀ {R S Rᵣ Sᵣ : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Rᵣ] [inst_3 : CommRing Sᵣ]
      [inst_4 : Algebra R Rᵣ] [inst_5 : Algebra S Sᵣ] [inst_6 : Algebra R S] [inst_7 : Algebra R Sᵣ]
      [inst_8 : Algebra Rᵣ Sᵣ] [IsScalarTower R S Sᵣ] [IsScalarTower R Rᵣ Sᵣ] (M : Submonoid R) [IsLocalization M Rᵣ]
      [IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ], P (algebraMap R S) → P (algebraMap Rᵣ Sᵣ)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularMono.containsIdentities : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MorphismProperty.regularMono C).ContainsIdentities
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_some_of_findSome?_eq_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin n → Option α}, Fin.findSome? f = some x → ∃ i, f i = some x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instHasZeroObjectLocalization' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C]
  (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [inst_3 : W.HasLocalization]
  [CategoryTheory.Limits.HasZeroObject C], CategoryTheory.Limits.HasZeroObject W.Localization'
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.toFinset ⊆ t.toFinset ↔ s ⊆ t
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.mk.inj : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : NontriviallyNormedField 𝕜} {inst_1 : AddCommGroup E} {inst_2 : Module 𝕜 E}
  {inst_3 : TopologicalSpace E} {X₀ X₁ : Submodule 𝕜 E} {isTopCompl : Submodule.IsTopCompl X₁ X₀}
  {finite_X₀ : FiniteDimensional 𝕜 ↥X₀} {X₀_1 X₁_1 : Submodule 𝕜 E} {isTopCompl_1 : Submodule.IsTopCompl X₁_1 X₀_1}
  {finite_X₀_1 : FiniteDimensional 𝕜 ↥X₀_1},
  { X₀ := X₀, X₁ := X₁, isTopCompl := isTopCompl, finite_X₀ := finite_X₀ } =
      { X₀ := X₀_1, X₁ := X₁_1, isTopCompl := isTopCompl_1, finite_X₀ := finite_X₀_1 } →
    X₀ = X₀_1 ∧ X₁ = X₁_1
-- Mathlib.Algebra.Group.Conj
/-- The canonical quotient map from an additive monoid `α` into the
`AddConjClasses` of `α`  -/
AddConjClasses.mk : {α : Type u_1} → [inst : AddMonoid α] → α → AddConjClasses α
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.sizeof_of_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
-- Mathlib.Order.Filter.Prod
Filter.tendsto_prod_swap : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.swap (f ×ˢ g) (g ×ˢ f)
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- If `X ⟶ Y` is an open immersion of PresheafedSpaces, and `Y` is a Scheme, we can
upgrade it into a morphism of Schemes.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom : {X : AlgebraicGeometry.PresheafedSpace CommRingCat} →
  (Y : AlgebraicGeometry.Scheme) →
    (f : X ⟶ Y.toPresheafedSpace) →
      [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
        AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f ⟶ Y
-- Mathlib.Algebra.Group.Subgroup.Map
/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`.  -/
AddSubgroup.addSubgroupOfEquivOfLe : {G : Type u_7} → [inst : AddGroup G] → {H K : AddSubgroup G} → H ≤ K → ↥(H.addSubgroupOf K) ≃+ ↥H
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x'),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x')
      (X.presheaf.stalkSpecializes h)
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `isClosed_setOfPred_inseparable`. -/
isClosed_setOf_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], IsClosed {p | Inseparable p.1 p.2}
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The isomorphism `M.exteriorPower 0 ≅ ModuleCat.of R R`.  -/
ModuleCat.exteriorPower.iso₀ : {R : Type u} → [inst : CommRing R] → (M : ModuleCat R) → M.exteriorPower 0 ≅ ModuleCat.of R R
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_zsmul_right : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute a ↑u → ∀ (m : ℤ), AddCommute a ↑(m • u)
-- Lean.Message
Lean.SerialMessage.toMessage : Lean.SerialMessage → Lean.Message
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_H0Iso_hom_f : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso B).hom (groupCohomology.shortComplexH0 B).f) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f (Rep.Hom.toModuleCatHom φ))
-- Init.Data.Slice.List.Lemmas
List.mkSlice_roc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- pseudometric space instance on the product of finitely many pseudometric spaces, using the
`L^p` distance, and having as uniformity the product uniformity.  -/
PiLp.instPseudoMetricSpace : (p : ENNReal) →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → PseudoMetricSpace (β i)] → PseudoMetricSpace (PiLp p β)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_hasFDerivAt_iff' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F},
  HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f (↑iso.symm ∘SL f') x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.mem_fixingSubgroup_union_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M},
  g ∈ fixingSubgroup M (s ∪ t) ↔ g ∈ fixingSubgroup M s ∧ g ∈ fixingSubgroup M t
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Turn a morphism in `Semigrp` back into a `MulHom`.  -/
Semigrp.Hom.hom : {X Y : Semigrp} → X.Hom Y → ↑X →ₙ* ↑Y
-- Std.Sat.AIG.Basic
Std.Sat.AIG.denote.go.eq_def : ∀ {α : Type} (x : ℕ) (decls : Array (Std.Sat.AIG.Decl α)) (assign : α → Bool) (h1 : x < decls.size)
  (h2 : Std.Sat.AIG.IsDAG α decls),
  Std.Sat.AIG.denote.go x decls assign h1 h2 =
    match elem : decls[x] with
    | Std.Sat.AIG.Decl.false => false
    | Std.Sat.AIG.Decl.atom v => assign v
    | Std.Sat.AIG.Decl.gate lhs rhs =>
      have this := ⋯;
      have lval := Std.Sat.AIG.denote.go lhs.gate decls assign ⋯ h2;
      have rval := Std.Sat.AIG.denote.go rhs.gate decls assign ⋯ h2;
      (lval ^^ lhs.invert) && (rval ^^ rhs.invert)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : h₂.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
      (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom h)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.idToMonad : {m : Type u → Type v} → [Monad m] → ⦃α : Type u⦄ → Id α → m α
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C],
  CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, max u₂ v, max (max (max u u₂) v) v₂} (CategoryTheory.Functor K C)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  x = Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
        h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) ≍
      h_1 ()
-- Mathlib.RingTheory.FormalGroup.Basic
_private.Mathlib.RingTheory.FormalGroup.Basic.0.termX₀ : Lean.ParserDescr
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
coe_galRestrict_apply : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (σ : Gal(L/K)), ↑((galRestrict A K L B) σ) = (galRestrictHom A K L B) ↑σ
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a functor `F : J ⥤ K ⥤ C`, with all needed colimits,
we can construct a diagram consisting of the colimit cocone over each functor `F.obj j`,
and the universal cocone morphisms between these.
 -/
CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [CategoryTheory.Limits.HasColimitsOfShape K C] → CategoryTheory.Limits.DiagramOfCocones F
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_range_of_tendsto : ∀ {α : Type u} [inst : PseudoMetricSpace α] (u : ℕ → α) {x : α},
  Filter.Tendsto u Filter.atTop (nhds x) → Bornology.IsBounded (Set.range u)
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
/-- For `a ≤ b`, `a` left divides `b`  -/
ExistsMulOfLE.exists_mul_of_le : ∀ {α : Type u} {inst : Mul α} {inst_1 : LE α} [self : ExistsMulOfLE α] {a b : α}, a ≤ b → ∃ c, b = a * c
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
MonoidAlgebra.instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] [inst_3 : Mul A]
  [UniqueProds A], IsRightCancelMulZero (MonoidAlgebra R A)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [h : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.hComp'.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : 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_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  {T₁₂ : CategoryTheory.Functor C₁ C₃} {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp T₂ ≅ T₁₂)
  (eB : B₁.comp B₂ ≅ B₁₂), w.hComp' w' eT eB = (w.hComp w').whiskerHorizontal eT.inv eB.hom
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.coeff_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
  (Polynomial.map f p).coeff n = f (p.coeff n)
-- Mathlib.ModelTheory.Syntax
/-- A theory indicating that each of a set of constants is distinct.  -/
FirstOrder.Language.distinctConstantsTheory : (L : FirstOrder.Language) → {α : Type u'} → Set α → (L.withConstants α).Theory
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.id_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A),
  (CategoryTheory.CategoryStruct.id F).hom a = CategoryTheory.CategoryStruct.id (F.functor a)