mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iInf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {f : κ → Ideal A}, (∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)) → Ideal.IsHomogeneous 𝒜 (⨅ i, f i)
-- Mathlib.Tactic.NormNum.Pow
/-- Invariants: `a ^ b₀ = c₀`, `depth > 0`, `b >>> depth = b₀`, `p := Nat.pow $a $b₀ = $c₀`  -/
_private.Mathlib.Tactic.NormNum.Pow.0.Mathlib.Meta.NormNum.evalNatPow.go : ℕ →
  (a b₀ c₀ b : Q(ℕ)) →
    (p : Q(Prop)) →
      «$p» =Q («$a».pow «$b₀» = «$c₀») → (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowT «$p» «$a» «$b» «$c»)
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the pure predicate `p` returns `true` for
all element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.

This variant terminates after finitely mall steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.all`.
 -/
Std.Iter.Total.all : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] → [Std.Iterators.Finite α Id] → (β → Bool) → Std.Iter.Total β → Bool
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `J` is `u`-small, `RingCat.{u}` has limits of shape `J`.  -/
RingCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J RingCat
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.mul_divisors_filter_prime_pow : ∀ {a b : ℕ}, a.Coprime b → {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
-- Mathlib.Computability.TuringMachine.Computable
/-- A TM2 machine has finitely many function labels.  -/
Turing.FinTM2.ΛFin : (self : Turing.FinTM2) → Fintype self.Λ
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.log_pow_eq_self : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M},
  (Function.Injective fun m => n ^ m) → ∀ (m : ℕ), Submonoid.log (Submonoid.pow n m) = m
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData_H : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).RightHomologyData),
  (HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).H = h.H
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config.mk.inj : ∀ {useDecide emptyType : Bool} {searchFuel : ℕ} {genDiseq useDecide_1 emptyType_1 : Bool} {searchFuel_1 : ℕ}
  {genDiseq_1 : Bool},
  { useDecide := useDecide, emptyType := emptyType, searchFuel := searchFuel, genDiseq := genDiseq } =
      { useDecide := useDecide_1, emptyType := emptyType_1, searchFuel := searchFuel_1, genDiseq := genDiseq_1 } →
    useDecide = useDecide_1 ∧ emptyType = emptyType_1 ∧ searchFuel = searchFuel_1 ∧ genDiseq = genDiseq_1
-- Mathlib.Algebra.Free
/-- Lifts a magma homomorphism `α → β` to a semigroup homomorphism `Magma.AssocQuotient α → β`
given a semigroup `β`.  -/
Magma.AssocQuotient.lift : {α : Type u} → [inst : Mul α] → {β : Type v} → [inst_1 : Semigroup β] → (α →ₙ* β) ≃ (Magma.AssocQuotient α →ₙ* β)
-- Mathlib.Order.Bounds.Basic
IsGLB.exists_between : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → a < b → ∃ c ∈ s, a ≤ c ∧ c < b
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticSeverity : Inhabited Lean.Lsp.DiagnosticSeverity
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Init.Data.List.Nat.InsertIdx
List.getElem_insertIdx_of_gt : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ} (hn : i < j) (hk : j < (l.insertIdx i x).length),
  (l.insertIdx i x)[j] = l[j - 1]
-- Mathlib.AlgebraicGeometry.Normalization
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap`. -/
AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.NatTrans.Coequifibered
    ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft
      (AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap f))
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.mk.sizeOf_spec : ∀ (sysname release version machine : String),
  sizeOf { sysname := sysname, release := release, version := version, machine := machine } =
    1 + sizeOf sysname + sizeOf release + sizeOf version + sizeOf machine
-- Mathlib.NumberTheory.Height.NumberField
/-- The multiplicative height of a positive natural number `n` cast to `ℚ` equals `n`.  -/
Rat.mulHeight₁_natCast : ∀ (n : ℕ) [NeZero n], Height.mulHeight₁ ↑n = ↑n
-- Mathlib.FieldTheory.Normal.Defs
/-- [Stacks Tag 09HN](https://stacks.math.columbia.edu/tag/09HN) -/
Normal.tower_top_of_normal : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] (E : Type u_3)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [IsScalarTower F K E] [h : Normal F E], Normal K E
-- Mathlib.Computability.RegularExpressions
RegularExpression.rmatch.eq_2 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : RegularExpression α) (a : α) (as : List α),
  x.rmatch (a :: as) = (x.deriv a).rmatch as
-- Mathlib.GroupTheory.GroupAction.Ring
/-- Note that `AddCommMonoid.nat_isScalarTower` requires stronger assumptions on `R`.  -/
NonUnitalNonAssocSemiring.nat_isScalarTower : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R], IsScalarTower ℕ R R
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqDSimpArgs.beq : Lean.Elab.Tactic.Grind.DSimpArgs → Lean.Elab.Tactic.Grind.DSimpArgs → Bool
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_or_aux_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.blimsup u f p ≤ Filter.blimsup u f fun x => p x ∨ q x
-- Mathlib.Data.PFun
PFun.toSubtype_apply : ∀ {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β) (a : α),
  PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommRing.toNonUnitalRing : {α : Type u} → [self : NonUnitalCommRing α] → NonUnitalRing α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp_i_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k}
  (h : (groupHomology.shortComplexH1 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 B).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₁ f φ) h)
-- Mathlib.Topology.DiscreteSubset
codiscreteWithin_le_codiscrete_inf_principal : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  Filter.codiscreteWithin s ≤ Filter.codiscrete X ⊓ Filter.principal s
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
ValueDistribution.logCounting.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (f f_1 : 𝕜 → E),
  f = f_1 →
    ∀ (a a_1 : WithTop E),
      a = a_1 →
        ∀ (a_2 a_3 : ℝ), a_2 = a_3 → ValueDistribution.logCounting f a a_2 = ValueDistribution.logCounting f_1 a_1 a_3
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment.eq_2 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.removeNegAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
-- Aesop.Stats.Basic
Aesop.instToJsonForwardRuleStateStats.toJson : Aesop.ForwardRuleStateStats → Lean.Json
-- Mathlib.Computability.DFA
/-- Lifts the state type `σ` inside `Language.IsRegular` to a different universe.  -/
_private.Mathlib.Computability.DFA.0.Language.isRegular_iff.helper : ∀ {T : Type u} {L : Language T}, (∃ σ x M, M.accepts = L) → ∃ σ' x M, M.accepts = L
-- Mathlib.Data.Set.Image
Set.Nonempty.image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s : Set α}, s.Nonempty → (f '' s).Nonempty
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.contains a = false → t.get! a = default
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_bot_left_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A : Subalgebra R S), ⊥.mulMap A = A.val.comp ↑A.lTensorBot
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The counit morphism of a comonoid object.  -/
CategoryTheory.ComonObj.«termε[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The 2-isomorphisms agree with the underlying 2-morphism of the oplax transformation.  -/
CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} (self : CategoryTheory.Oplax.OplaxTrans.StrongCore η) {a b : B}
  (f : a ⟶ b), (self.naturality f).hom = η.naturality f
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instModule : {σ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Module R (MvPowerSeries σ A)
-- Lean.Data.Lsp.Internal
/-- Direct imports of this file.  -/
Lean.Lsp.LeanILeanHeaderSetupInfoParams.directImports : Lean.Lsp.LeanILeanHeaderSetupInfoParams → Array Lean.Lsp.ImportInfo
-- Mathlib.Data.Set.Lattice
Set.iUnion_and : ∀ {α : Type u_1} {p q : Prop} (s : p ∧ q → Set α), ⋃ (h : p ∧ q), s h = ⋃ (hp : p), ⋃ (hq : q), s ⋯
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v : Fin (n + 1) → E),
  (ContinuousAlternatingMap.alternatizeUncurryFin f) v = ∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] (k : α) (v : β k), m₁.Equiv m₂ → (m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp_surjective : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M], Function.Surjective AList.lookupFinsupp
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : M →ₙ+ N},
  AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- `MVarId`s corresponding to the `.labelledStar` labels. The index in the array is the label.
It is `none` if we use `.star` instead of `labelledStar`,
for example when encoding the lookup expression.
 -/
Lean.Meta.RefinedDiscrTree.LazyEntry.labelledStars? : Lean.Meta.RefinedDiscrTree.LazyEntry → Option (Array Lean.MVarId)
-- Std.Internal.Do.ExceptPost
/-- Componentwise complete lattice on `EPost.Cons`, via `PProd`.  -/
Std.Internal.Do.instCompleteLatticeCons : {eh : Type u_1} →
  {et : Type u_2} →
    [Lean.Order.CompleteLattice eh] → [Lean.Order.CompleteLattice et] → Lean.Order.CompleteLattice (EPost.Cons✝ eh et)
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_isoClosure_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C),
  P.isoClosure X ↔ ∃ Y, ∃ (_ : P Y), Nonempty (X ≅ Y)
-- Mathlib.Computability.TuringMachine.Tape
/-- A modified version of `Quotient.liftOn'` specialized for `ListBlank`, with the stronger
precondition `BlankExtends` instead of `BlankRel`.  -/
Turing.ListBlank.liftOn : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {α : Sort u_2} → Turing.ListBlank Γ → (f : List Γ → α) → (∀ (a b : List Γ), Turing.BlankExtends a b → f a = f b) → α
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C}
  {inst_2 : CategoryTheory.Limits.HasPullbacks C} {X Y : CategoryTheory.Dial C} {f : X.src ⟶ Y.src}
  {F : X.src ⨯ Y.tgt ⟶ X.tgt}
  {le :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel}
  {f_1 : X.src ⟶ Y.src} {F_1 : X.src ⨯ Y.tgt ⟶ X.tgt}
  {le_1 :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F_1)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f_1 (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel},
  { f := f, F := F, le := le } = { f := f_1, F := F_1, le := le_1 } → f = f_1 ∧ F = F_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getKeyLE k t ho he = Std.DTreeMap.Internal.Impl.getKeyLE k_1 t_1 ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.pow_antitone : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  autoParam (0 ≤ a) CStarAlgebra.pow_antitone._auto_1 → a ≤ 1 → Antitone fun x => a ^ x
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.intPow_negOfNat_bit0 : ∀ {a b c b' c' : ℕ}, a.pow b' = c' → 2 * b' = b → c' * c' = c → (Int.negOfNat a).pow b = Int.ofNat c
-- Init.Data.Iterators.ToIterator
/-- Creates a pure `ToIterator` instance.  -/
Std.ToIterator.of : {γ : Type u_1} → {β : Type w} → (α : Type w) → (γ → Std.Iter β) → Std.ToIterator γ Id α β
-- Mathlib.Algebra.Module.Submodule.Finsupp
Submodule.set_smul_eq_map : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (sR : Set R)
  (N : Submodule R M) [inst_3 : SMulCommClass R R ↥N],
  sR • N = Submodule.map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ'' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc),
  CategoryTheory.CategoryStruct.comp (X.δ (i.castLT ⋯)) (X.δ j.succ) =
    CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.DTreeMap.getKeyGE! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α → α
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.ore_right_cancel : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ r₂ : R) (s : ↥S),
  r₁ + ↑s = r₂ + ↑s → ∃ s', ↑s' + r₁ = ↑s' + r₂
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The inclusion from monomorphisms over X to morphisms over X.  -/
CategoryTheory.MonoOver.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) → CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.Over X)
-- Aesop.Tree.State
Aesop.Goal.stateNoCache : Aesop.Goal → BaseIO Aesop.GoalState
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mul_smul' : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {T : Type u_1} [inst_1 : CommSemiring T] [inst_2 : Algebra R T]
  [inst_3 : IsLocalization S T] {A : Type u_3} [inst_4 : Semiring A] [inst_5 : Algebra R A] (x : T)
  (p₁ p₂ : LocalizedModule S A), p₁ * x • p₂ = x • (p₁ * p₂)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.re_inner_nonneg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 (T x) x)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- Laplace expansion of `detp` along the `none` row of an `Option`-indexed matrix.  -/
Matrix.detp_option_expand_row_none : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix (Option n) (Option n) R),
  Matrix.detp s A =
    A none none * Matrix.detp s (A.submatrix some some) +
      ∑ k, A none (some k) * Matrix.detp (-s) (A.submatrix some (Function.update some k none))
-- Lean.Parser.Extra
/-- The parser `many1(p)`, or `p+`, repeats `p` until it fails, and returns the list of results.
`p` must succeed at least once, or this parser will fail.

Note that this parser produces the same parse tree as the `many(p)` / `p*` combinator,
and one matches both `p*` and `p+` using `$[ .. ]*` syntax in a syntax match.
(There is no `$[ .. ]+` syntax.)

The argument `p` is "auto-grouped", meaning that if the arity is greater than 1 it will be
automatically replaced by `group(p)` to ensure that it produces exactly 1 value.

This parser has arity 1: it produces a `nullKind` node containing one argument for each
invocation of `p` (or `group(p)`).  -/
Lean.Parser.many1 : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_naturality_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a) ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y)) =
    (F.map g).toFunctor.map ((F.map f).toFunctor.map a)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α)
  (u : Equiv.Perm ↑(Function.fixedPoints ⇑f)) (v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)),
  (Equiv.Perm.ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)
-- Mathlib.Analysis.Convex.Mul
ConvexOn.smul' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F},
  ConvexOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → MonovaryOn f g s → ConvexOn 𝕜 s (f • g)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Two continuous additive isomorphisms agree if they are defined by
the same underlying function.  -/
ContinuousAddEquiv.ext : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {f g : M ≃ₜ+ N}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.MeasureTheory.Integral.CircleIntegral
CircleIntegrable.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable g c R → CircleIntegrable (f + g) c R
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.instCategory : CategoryTheory.Category.{u, u + 1} PartOrdEmb
-- Mathlib.Data.Finset.Insert
Finset.prodPiCons.congr_simp : ∀ {α : Type u_1} {s : Finset α} {inst : DecidableEq α} [inst_1 : DecidableEq α] (f : α → Type u_3) {a : α} (has : a ∉ s)
  (x x_1 : f a × ((i : α) → i ∈ s → f i)),
  x = x_1 →
    ∀ (i : α) (a_1 : i ∈ Finset.cons a s has), Finset.prodPiCons f has x i a_1 = Finset.prodPiCons f has x_1 i a_1
-- Init.Internal.Order.Basic
Lean.Order.monotone_optionTRun : ∀ {γ : Sort u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [inst : Lean.Order.PartialOrder γ] [Monad m]
  [inst_2 : (α : Type u_2) → Lean.Order.PartialOrder (m α)] (f : γ → OptionT m α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => (f x).run
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatTrans.pi_app : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] {F G : (i : I) → CategoryTheory.Functor (C i) (D i)}
  (α : (i : I) → F i ⟶ G i) (f : (i : I) → C i) (i : I), (CategoryTheory.NatTrans.pi α).app f i = (α i).app (f i)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- **Pentagonal number theorem** for power series, expressed as an infinite product. See also
`PowerSeries.WithPiTopology.hasSum_pentagonalSeries` that expresses `pentagonalSeries` as an
infinite sum.  -/
PowerSeries.WithPiTopology.hasProd_one_sub_X_pow : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R],
  HasProd (fun n => 1 - PowerSeries.X ^ (n + 1)) (PowerSeries.pentagonalSeries R)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Int.zmultiples_one : AddSubgroup.zmultiples 1 = ⊤
-- Lean.Data.Position
Lean.MonadFileMap.mk : {m : Type → Type} → m Lean.FileMap → Lean.MonadFileMap m
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_15.eq_1 : ∀ (C : Type u_1) (motive : CategoryTheory.WithInitial Cᵒᵖ → Sort u_2) (x : Cᵒᵖ)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithInitial.of x)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of x with
    | CategoryTheory.WithInitial.of x => h_1 x
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 x
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- If `S₀ / R₀` and `S₁ / R₁` are algebras, `i : R₀ ≃+* R₁` and `j : S₀ ≃+* S₁` are
ring isomorphisms, such that `R₀ → R₁ → S₁` and `R₀ → S₀ → S₁` commute,
then the `finrank` of `S₀ / R₀` is equal to the finrank of `S₁ / R₁`.  -/
Algebra.finrank_eq_of_equiv_equiv : ∀ {R₀ : Type u_1} {S₀ : Type u_2} [inst : CommSemiring R₀] [inst_1 : Semiring S₀] [inst_2 : Algebra R₀ S₀]
  {R₁ : Type u_3} {S₁ : Type u_4} [inst_3 : CommSemiring R₁] [inst_4 : Semiring S₁] [inst_5 : Algebra R₁ S₁]
  (i : R₀ ≃+* R₁) (j : S₀ ≃+* S₁),
  (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀) →
    Module.finrank R₀ S₀ = Module.finrank R₁ S₁