mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.coe_gramSchmidtBasis : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  (b : Module.Basis ι 𝕜 E), ⇑(InnerProductSpace.gramSchmidtBasis b) = InnerProductSpace.gramSchmidt 𝕜 ⇑b
-- Lean.Elab.InfoTree.Main
Lean.Elab.pushInfoLeaf : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.Elab.Info → m Unit
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.coeff_toOrderTopSubOnePos_pow : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] [inst_4 : BinomialRing R] {g : Γ} (hg : 0 < g) (r s : R) (k : ℕ),
  (↑↑(HahnSeries.toOrderTopSubOnePos ⋯ ^ s)).coeff (k • g) = Ring.choose s k • r ^ k
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- When `C` has enough projectives,
`Projective.d f : Projective.syzygies f ⟶ X` is the composition
`π (kernel f) ≫ kernel.ι f`.

(When `C` is abelian, we have `exact (projective.d f) f`.)
 -/
CategoryTheory.Projective.d : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnoughProjectives C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} →
          (f : X ⟶ Y) → [inst_3 : CategoryTheory.Limits.HasKernel f] → CategoryTheory.Projective.syzygies f ⟶ X
-- Lean.Elab.PreDefinition.Structural.IndPred
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.withFunTypes.go : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.GroupTheory.PushoutI
/-- The map from the coproduct into the pushout  -/
Monoid.PushoutI.ofCoprodI : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] →
        [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → Monoid.CoprodI G →* Monoid.PushoutI φ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂ : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M],
  ∀ f ∈ groupCohomology.coboundaries₂ (Rep.ofMulDistribMulAction G M),
    groupCohomology.IsMulCoboundary₂ (⇑Additive.toMul ∘ f)
-- Lean.MonadEnv
Lean.isCtor? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.ConstructorVal)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, `AddMonCat.{u}` has limits of shape `J`.  -/
AddMonCat.HasLimits.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J AddMonCat
-- Mathlib.Analysis.InnerProductSpace.PiL2
Pi.orthonormalBasis_apply : ∀ {η : Type u_7} [inst : Fintype η] [inst_1 : DecidableEq η] {ι : η → Type u_8} [inst_2 : (i : η) → Fintype (ι i)]
  {𝕜 : Type u_9} [inst_3 : RCLike 𝕜] {E : η → Type u_10} [inst_4 : (i : η) → NormedAddCommGroup (E i)]
  [inst_5 : (i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (j : (i : η) × ι i),
  (Pi.orthonormalBasis B) j = PiLp.single 2 j.fst ((B j.fst) j.snd)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ΨSq 0 = 0
-- Init.Data.Int.Bitwise.Lemmas
Int.natCast_shiftRight : ∀ (n s : ℕ), ↑(n >>> s) = ↑n >>> s
-- Mathlib.Computability.Reduce
/-- The many-one degree of a set on a primcodable type.  -/
ManyOneDegree.of : {α : Type u} → [Primcodable α] → [Inhabited α] → (α → Prop) → ManyOneDegree
-- Mathlib.Algebra.Free
FreeAddMagma.map_add' : ∀ {α β : Type u} (f : α → β) (x y : FreeAddMagma α), f <$> (x + y) = f <$> x + f <$> y
-- Init.WF
/-- A lexicographical order based on the orders `ra` and `rb` for the elements of pairs.
 -/
Prod.Lex : {α : Type u} → {β : Type v} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_iff_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ}
  [MulPosMono M₀], 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Lean.CoreM
/-- Allows `realizeConst` calls for the given declaration in all derived environment branches.
Realizations will run using the given environment and options to ensure deterministic results. Note
that while we check that the function isn't called before the declaration is actually added to the
environment, we cannot automatically check that it isn't otherwise called too early in the sense
that helper declarations and environment extension state that may be relevant to realizations may
not have been added yet. We do check that we are not calling it from a different branch than `c` was
added on, which would be definitely too late. Thus, this function should generally be called in
elaborators calling `addDecl` (when that declaration is a plausible target for realization) at the
latest possible point, i.e. at the very end of the elaborator or just before a first realization may
be triggered if any.
 -/
Lean.enableRealizationsForConst : Lean.Name → Lean.CoreM Unit
-- Mathlib.Analysis.Normed.Group.Submodule
/-- If `x` is an element of a submodule `s` of a normed group `E`, its norm in `E` is equal to its
norm in `s`.

This is a reversed version of the `simp` lemma `Submodule.coe_norm` for use by `norm_cast`.  -/
Submodule.norm_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Submodule 𝕜 E} (x : ↥s), ‖↑x‖ = ‖x‖
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.PlausibleStep.depleted : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β},
  it.internalState.countdown = 1 → Std.Iterators.Types.Take.PlausibleStep it Std.IterStep.done
-- Mathlib.Logic.Function.Conjugate
/-- If `fab : α → β` semiconjugates `ga` to `gb` and `fbc : β → γ` semiconjugates `gb` to `gc`,
then `fbc ∘ fab` semiconjugates `ga` to `gc`.

See also `Function.Semiconj.comp_left` for a version with reversed arguments.  -/
Function.Semiconj.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ},
  Function.Semiconj fab ga gb → Function.Semiconj fbc gb gc → Function.Semiconj (fbc ∘ fab) ga gc
-- Mathlib.Computability.Primrec.Basic
/-- `Primrec₂ f` means `f` is a binary primitive recursive function.
This is technically unnecessary since we can always curry all
the arguments together, but there are enough natural two-arg
functions that it is convenient to express this directly.  -/
Primrec₂ : {α : Type u_1} →
  {β : Type u_2} → {σ : Type u_3} → [Primcodable α] → [Primcodable β] → [Primcodable σ] → (α → β → σ) → Prop
-- Lean.Parser.Tactic.Doc
/-- The known tactic tags that allow tactics to be grouped by purpose.
 -/
Lean.Parser.Tactic.Doc.knownTacticTagExt : Lean.PersistentEnvExtension (Lean.Name × String × Option String) (Lean.Name × String × Option String)
  (Lean.NameMap (String × Option String))
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.of_eq_map_equiv : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} {C : Type u_4} [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [P.LiesOver p] {E : Type u_6}
  [inst_6 : EquivLike E B C] [AlgEquivClass E A B C] (σ : E), Q = Ideal.map σ P → Q.LiesOver p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → t.isEmpty = false
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, k ∉ m₂ → Std.ExtDHashMap.Const.get! (m₁ ∩ m₂) k = default
-- Mathlib.Logic.Basic
ite_ne_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, (if P then a else b) ≠ a ↔ ¬P ∧ a ≠ b
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.subtype_mk : ∀ {α : Type ua} {β : Type ub} {p : α → Prop} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : β → α},
  UniformContinuous f → ∀ (h : ∀ (x : β), p (f x)), UniformContinuous fun x => ⟨f x, ⋯⟩
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : Lattice β] [inst_1 : BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x // P x }),
  (BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf) x = ↑x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsCardinalForSmallObjectArgumentInnerHornInclusionsAleph0 : SSet.innerHornInclusions.IsCardinalForSmallObjectArgument Cardinal.aleph0
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.support_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R),
  (x.divMonomial s).support = x.support.preimage (fun x => s + x) ⋯
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.instIsRightAdjointOppositeObjFunctorTypeYoneda : ∀ (R : CommRingCat), (CategoryTheory.yoneda.obj R).IsRightAdjoint
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.natMul : ℕ → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr
-- Mathlib.Data.Finset.Max
/-- Induction principle for `Finset`s in a linearly ordered type: a predicate is true on all
`s : Finset α` provided that:

* it is true on the empty `Finset`,
* for every `s : Finset α` and an element `a` strictly greater than all elements of `s`, `p s`
  implies `p (insert a s)`.  -/
Finset.induction_on_max : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : DecidableEq α] {motive : Finset α → Prop} (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (insert a s)) → motive s
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C] (n : ℕ),
  ⊤.extensionProductIter n = ⊤
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  (K : HomologicalComplex C c) (i : ι),
  (HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).inv.app ((HomotopyCategory.quotient C c).obj K) =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C c i).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i).inv.app K)
        ((HomologicalComplexUpToQuasiIso.homologyFunctor C c i).map
          ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).inv.app K)))
-- Mathlib.RingTheory.RamificationInertia.Inertia
IsFractionRing.algEquivOfAlgEquiv.congr_simp : ∀ {R : Type u_8} {A : Type u_9} {K : Type u_10} {B : Type u_11} {L : Type u_12} [inst : CommSemiring R]
  [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : CommRing K] [inst_4 : CommRing L] [inst_5 : Algebra R A]
  [inst_6 : Algebra R K] [inst_7 : Algebra A K] [inst_8 : IsFractionRing A K] [inst_9 : IsScalarTower R A K]
  [inst_10 : Algebra R B] [inst_11 : Algebra R L] [inst_12 : Algebra B L] [inst_13 : IsFractionRing B L]
  [inst_14 : IsScalarTower R B L] (h h_1 : A ≃ₐ[R] B),
  h = h_1 → IsFractionRing.algEquivOfAlgEquiv h = IsFractionRing.algEquivOfAlgEquiv h_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.support = [u]
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_cancel_right`. -/
Set.union_diff_cancel_right : ∀ {α : Type u_1} {s t : Set α}, s ∩ t ⊆ ∅ → (s ∪ t) \ t = s
-- Lean.MetavarContext
/-- Set the `BinderInfo` of an fvar. If the given metavariable is not declared or
the given fvar doesn't exist in its context, nothing happens.
 -/
Lean.MVarId.setFVarBinderInfo : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Lean.FVarId → Lean.BinderInfo → m Unit
-- Mathlib.Data.Multiset.MapFold
Multiset.nodup_attach : ∀ {α : Type u_1} {s : Multiset α}, s.attach.Nodup ↔ s.Nodup
-- Mathlib.Data.Set.Basic
Set.empty_ne_univ : ∀ {α : Type u} [Nonempty α], ∅ ≠ Set.univ
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.u : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution'✝ hζ → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The cone over the tower
```
⋯ → ∏_{n < m} M n × ∏_{n ≥ m} N n → ⋯ → ∏ N
```
with cone point `∏ M` is indeed a limit cone.
 -/
CategoryTheory.Limits.SequentialProduct.isLimit : {C : Type u_1} →
  {M N : ℕ → C} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      (f : (n : ℕ) → M n ⟶ N n) →
        [inst_1 : CategoryTheory.Limits.HasCountableProducts C] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.SequentialProduct.cone f)
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The short exact sequence
`0 ⟶ opZ^(f₁, f₂ ≫ f₃) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ H^n(f₁, f₂, f₃) ⟶ 0`.  -/
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁ : {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] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ : ι} →
              (f₁ : i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₁₂ : i₀ ⟶ i₂) →
                      (f₂₃ : i₁ ⟶ i₃) →
                        CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
                          CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                            (n₀ n₁ n₂ : ℤ) →
                              autoParam (n₀ + 1 = n₁)
                                  CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1 →
                                autoParam (n₁ + 1 = n₂)
                                    CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3 →
                                  CategoryTheory.ShortComplex C
-- Mathlib.Data.Multiset.AddSub
Multiset.add_zero : ∀ {α : Type u_1} (s : Multiset α), s + 0 = s
-- Mathlib.Logic.Function.CompTypeclasses
/-- `φ`, `ψ` and `ψ ∘ φ` for a `CompTriple`.  -/
CompTriple.comp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P}, CompTriple φ ψ (ψ ∘ φ)
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.mem_Icc_iff_abs_le : ∀ {R : Type u_2} [inst : AddCommGroup R] [inst_1 : LinearOrder R] [IsOrderedAddMonoid R] {x y z : R},
  |x - y| ≤ z ↔ y ∈ Set.Icc (x - z) (x + z)
-- Init.Data.UInt.Basic
/-- Converts 16-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.toUSize : UInt16 → USize
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_empty_of_eq_empty : ∀ {α : Type u_1} {ι : Sort u_5} {i : ι} {f : ι → Set α}, f i = ∅ → ⋂ j, f j = ∅
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opAddEquiv_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : M), AddOpposite.opAddEquiv a = AddOpposite.op a
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The topology of pointwise convergence on `E →Lₚₜ[𝕜] 𝕜` coincides with the weak-\* topology.  -/
PointwiseConvergenceCLM.equivWeakDual : (𝕜 : Type u_3) →
  [inst : NormedField 𝕜] →
    (E : Type u_7) →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] → [inst_3 : Module 𝕜 E] → (E →Lₚₜ[𝕜] 𝕜) ≃L[𝕜] WeakDual 𝕜 E
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.diagram_map : ∀ (P : ProfiniteAddGrp.{u}) {X Y : OpenNormalAddSubgroup ↑P.toProfinite.toTop} (f : X ⟶ Y),
  P.diagram.map f = (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u}).map (P.toFiniteQuotientFunctor.map f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- The pushforward of `SheafOfModules.QuasicoherentData` along a continuous
and cocontinuous functor.  -/
SheafOfModules.QuasicoherentData.pushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {D : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
                {K : CategoryTheory.GrothendieckTopology D} →
                  {S : CategoryTheory.Sheaf K RingCat} →
                    [inst_4 : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] →
                      [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
                        [inst_6 : ∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] →
                          (G : CategoryTheory.Functor D C) →
                            [inst_7 : G.IsContinuous K J] →
                              [G.IsCocontinuous K J] →
                                (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) →
                                  ((SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) →
                                    [inst_9 :
                                        ∀ (X : D),
                                          (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] →
                                      (∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
                                          CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁,
                                              max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
                                            (SheafOfModules.pushforward
                                              (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat
                                                    (K.over X) K).map
                                                φ))) →
                                        {M : SheafOfModules R} →
                                          M.QuasicoherentData → ((SheafOfModules.pushforward φ).obj M).QuasicoherentData
-- Mathlib.Order.Basic
/-- **Alias** of `lt_trans`. -/
LT.lt.trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
-- Std.Tactic.BVDecide.Syntax
/-- The maximum number of subexpressions to visit when performing simplification.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.maxSteps : Lean.Elab.Tactic.BVDecide.BVDecideConfig → ℕ
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobenius_eq_map_frobenius : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CharP R p],
  WittVector.frobenius = WittVector.map (frobenius R p)
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.mk.sizeOf_spec : ∀ (map : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (set : Lean.PHashSet Lean.Meta.Sym.AlphaKey),
  sizeOf { map := map, set := set } = 1 + sizeOf map + sizeOf set
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  s.singularPart μ =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
-- Mathlib.Dynamics.Flow
Flow.restrict.congr_simp : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ ϕ_1 : Flow τ α) (e_ϕ : ϕ = ϕ_1) {s : Set α} (h : IsInvariant ϕ.toFun s), ϕ.restrict h = ϕ_1.restrict ⋯
-- Mathlib.Algebra.Algebra.Hom
/-- Defining the homomorphism in the category R-Alg, denoted `A →ₐ[R] B`.  -/
«term_→ₐ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The `Functor.Monoidal` structure given by an oplax monoidal functor such
that `η` and `δ` are isomorphisms.  -/
CategoryTheory.Functor.Monoidal.ofOplaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.OplaxMonoidal] →
                [CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)] →
                  [∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)] → F.Monoidal
-- Lean.Elab.Calc
Lean.Elab.Term.CalcStepView.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (term proof : Lean.Term),
  sizeOf { ref := ref, term := term, proof := proof } = 1 + sizeOf ref + sizeOf term + sizeOf proof
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂)[k]? = t₁[k]?
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_eq_empty : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R}, p.support = ∅ ↔ p = 0
-- Mathlib.RingTheory.Finiteness.Basic
/-- The submodule generated by a finite set is `R`-finite.  -/
Module.Finite.span_of_finite : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Set M},
  A.Finite → Module.Finite R ↥(Submodule.span R A)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (X : CategoryTheory.Functor W.Localization D) {X_1 Y : C}
  (f : X_1 ⟶ Y),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.map f = X.map (W.Q.map f)
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_antidistrib_left`.  -/
Set.image2_image_left_anticomm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} {f : α' → β → γ}
  {g : α → α'} {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f (g a) b = g' (f' b a)) → Set.image2 f (g '' s) t = g' '' Set.image2 f' t s