mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.Basic
Odd.strictMono_pow : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} [ExistsAddOfLE R],
  Odd n → StrictMono fun a => a ^ n
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.differentiableAt : ∀ {𝕜 : 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] {x : E}
  (iso : E ≃L[𝕜] F), DifferentiableAt 𝕜 (⇑iso) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α}, a ∉ m → Std.DHashMap.Const.get! m a = default
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Given a morphism `f : Y ⟶ X`, a presieve `S` on `Y` and presieve `T` on `X`,
we say that *`S` factors through `T` along `f`*, written `S.FactorsThruAlong T f`,
provided that for any morphism `g : Z ⟶ Y` in `S`, there exists some
morphism `e : W ⟶ X` in `T` and some morphism `i : Z ⟶ W` such that the obvious
square commutes: `i ≫ e = g ≫ f`.

This is used in the definition of a coverage.
 -/
CategoryTheory.Presieve.FactorsThruAlong : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → CategoryTheory.Presieve Y → CategoryTheory.Presieve X → (Y ⟶ X) → Prop
-- Std.Http.Data.URI.Basic
Std.Http.instReprRequestTarget : Repr Std.Http.RequestTarget
-- Mathlib.Algebra.DualQuaternion
/-- The dual quaternions can be equivalently represented as a quaternion with dual coefficients,
or as a dual number with quaternion coefficients.

See also `Matrix.dualNumberEquiv` for a similar result.  -/
Quaternion.dualNumberEquiv : {R : Type u_1} → [inst : CommRing R] → Quaternion (DualNumber R) ≃ₐ[R] DualNumber (Quaternion R)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ],
  μ.compProd ProbabilityTheory.Kernel.id = MeasureTheory.Measure.map Function.diag μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_ne_zero_iff : ∀ {θ : ℂ}, Complex.sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑Real.pi
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, (m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D),
  (CategoryTheory.Functor.mapArrowEquivalence e).counitIso =
    (CategoryTheory.Functor.mapArrowFunctor D D).mapIso e.counitIso
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.instWellFoundedRelationProductive : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Productive α m] → WellFoundedRelation (Std.IterM.TerminationMeasures.Productive α m)
-- Mathlib.Order.KrullDimension
/-- The elements of coheight zero are the maximal elements.  -/
Order.coheight_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.coheight x = 0 ↔ IsMax x
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.exact : Mathlib.Tactic.GCongr.ForwardExt
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- Transfer `IsPurelyInseparable` across an `AlgEquiv`.  -/
AlgEquiv.isPurelyInseparable : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Ring K] [inst_4 : Algebra F K] (e : K ≃ₐ[F] E) [IsPurelyInseparable F K], IsPurelyInseparable F E
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), |(|a|)| = |a|
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.select.injEq : ∀ {α : Type} (finished finished_1 : Std.Async.Waiter (Option α)),
  (Std.CloseableChannel.Consumer.select✝ finished = Std.CloseableChannel.Consumer.select✝ finished_1) =
    (finished = finished_1)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `RatFunc.denom` is the denominator of a rational function,
normalized such that it is monic.  -/
RatFunc.denom : {K : Type u} → [inst : Field K] → RatFunc K → Polynomial K
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y},
  (∀ {f : A ⟶ X} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift) → CategoryTheory.HasLiftingProperty i p
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuousOn.comp` -/
ScottContinuousOn.fun_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {D : Set (Set α)} {f : α → β} {g : β → γ} {D' : Set (Set β)},
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) →
    Set.MapsTo (fun x => f '' x) D D' →
      ScottContinuousOn D' g → ScottContinuousOn D f → ScottContinuousOn D fun x => g (f x)
-- Mathlib.Data.Fintype.Lattice
Finset.fold_sup_univ : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : SemilatticeSup α] [inst_2 : OrderTop α] (a : α),
  Finset.fold max a (fun x => x) Finset.univ = ⊤
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Bijective ⇑e
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.head_support : ∀ {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b), p.support.head ⋯ = a
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.subsingletonInst.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.subsingletonInst = 1
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- Simpler expression for the differential in the standard resolution of `k` as a
`G`-representation. It sends `(g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁)`.  -/
Rep.standardComplex.d_eq : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G] (n : ℕ),
  (Rep.Hom.hom ((Rep.standardComplex k G).d (n + 1) n)).toLinearMap = Rep.standardComplex.d k G (n + 1)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
map_finsuppProd : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M] [inst_1 : CommMonoid N]
  [inst_2 : CommMonoid P] {H : Type u_16} [inst_3 : FunLike H N P] [MonoidHomClass H N P] (h : H) (f : α →₀ M)
  (g : α → M → N), h (f.prod g) = f.prod fun a b => h (g a b)
-- Mathlib.Analysis.Calculus.LogDerivUniformlyOn
logDeriv_tprod_eq_tsum : ∀ {ι : Type u_1} {s : Set ℂ},
  IsOpen s →
    ∀ {x : ℂ},
      x ∈ s →
        ∀ {f : ι → ℂ → ℂ},
          (∀ (i : ι), f i x ≠ 0) →
            (∀ (i : ι), DifferentiableOn ℂ (f i) s) →
              (Summable fun i => logDeriv (f i) x) →
                MultipliableLocallyUniformlyOn f s →
                  ∏' (i : ι), f i x ≠ 0 → logDeriv (fun x => ∏' (i : ι), f i x) x = ∑' (i : ι), logDeriv (f i) x
-- Init.Prelude
Nat.brecOn.eq : ∀ {motive : ℕ → Sort u} (t : ℕ) (F_1 : (t : ℕ) → Nat.below t → motive t),
  Nat.brecOn t F_1 = F_1 t (Nat.brecOn.go t F_1).2
-- Mathlib.Order.Heyting.Basic
snd_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : Compl α] [inst_1 : Compl β] (a : α × β), aᶜ.2 = a.2ᶜ
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_add_left_of_denseRange_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant],
      Ergodic (fun x => g + x) μ
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `Δ f` is the Laplacian of `f`. The meaning of this notation is type-dependent.  -/
Laplacian.termΔ : Lean.ParserDescr
-- Mathlib.Data.Rat.Star
Rat.addSubmonoid_closure_range_mul_self : AddSubmonoid.closure (Set.range fun x => x * x) = AddSubmonoid.nonneg ℚ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The topological group isomorphism between a profinite group and the projective limit of
its quotients by open normal subgroups  -/
ProfiniteGrp.continuousMulEquivLimittoFiniteQuotientFunctor : (P : ProfiniteGrp.{u}) → ↑P.toProfinite.toTop ≃ₜ* ↑(ProfiniteGrp.limit P.diagram).toProfinite.toTop
-- Lean.Parser.Term
Lean.Parser.Term.letEqnsDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.promise : ProofWidgets.RefreshToken → IO.Ref (IO.Promise Unit)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.starAlgHom.congr_simp : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : TopologicalSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra R S] [inst_13 : Algebra R A] [inst_14 : Algebra S A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S] {a : A}
  (φ φ_1 : C(↑(spectrum S a), S) →⋆ₐ[S] A),
  φ = φ_1 →
    ∀ {f f_1 : C(S, R)} (e_f : f = f_1) (h : SpectrumRestricts a ⇑f),
      SpectrumRestricts.starAlgHom φ h = SpectrumRestricts.starAlgHom φ_1 ⋯
-- Mathlib.Order.Preorder.Finite
/-- If the cofinality of a linear order is finite, it's at most one.  -/
Set.Finite.exists_subsingleton_isCofinal : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α}, s.Finite → IsCofinal s → ∃ t, t.Subsingleton ∧ IsCofinal t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.instInhabited : {V : Type u} → (G : SimpleGraph V) → (v : V) → Inhabited (G.Walk v v)
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- Cursor position in the file at which the widget is being displayed.  -/
SelectInsertParamsClass.pos : {α : Type} → [self : SelectInsertParamsClass α] → α → Lean.Lsp.Position
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getKeyLE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match hkky : compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLED k r ky
      | Ordering.eq => ky
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyLE k l ⋯ ⋯
-- Mathlib.Algebra.GroupWithZero.Action.Defs
ite_zero_smul : ∀ {M₀ : Type u_2} {A : Type u_7} [inst : MonoidWithZero M₀] [inst_1 : Zero A] [inst_2 : MulActionWithZero M₀ A]
  (p : Prop) [inst_3 : Decidable p] (a : M₀) (b : A), (if p then a else 0) • b = if p then a • b else 0
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (f g : A ⟶ B),
  f.hom₁ = g.hom₁ → f.hom₂ = g.hom₂ → f.hom₃ = g.hom₃ → f = g
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_mul_complex_Ioi : ∀ {a : ℂ},
  a.re < 0 → ∀ (c : ℝ), MeasureTheory.IntegrableOn (fun x => Complex.exp (a * ↑x)) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Data.Sum.Order
Sum.noMaxOrder_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β], NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_modify : ∀ {α : Type u} {instOrd : Ord α} [inst : Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Internal.Impl.Const.modify k f t},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey k' hc = if compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Init.Data.Int.OfNat
Int.Nonneg.num : ∀ (a : ℤ), Int.Nonneg.num_cert a = true → a ≥ 0
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.hasIntegral : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol → BoxIntegral.HasIntegral I l f vol (BoxIntegral.integral I l f vol)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `X ⟶ Y` with `Y` being a strict initial object, then `X` is also an initial object.  -/
CategoryTheory.Limits.IsInitial.ofStrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      {X Y : C} → (X ⟶ Y) → CategoryTheory.Limits.IsInitial Y → CategoryTheory.Limits.IsInitial X
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.span R ↑p = p
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst' : ∀ {M : Type u_1} [inst : DivInvOneMonoid M] {l l_d d : M}, l = 1 / l_d → l_d = d → l = d⁻¹
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.existsAddOfLE : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsStrictOrderedRing α] [ExistsAddOfLE α],
  ExistsAddOfLE { x // 0 ≤ x }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_singleton : ∀ {m n : ℕ}, n = m + 2 → (m<...n).toList = [m + 1]
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (d : D), (CategoryTheory.Join.mkFunctor F G α).obj (CategoryTheory.Join.right d) = G.obj d
-- Aesop.RuleSet
Aesop.BaseRuleSet.mk.inj : ∀ {normRules : Aesop.Index Aesop.NormRuleInfo} {unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo}
  {safeRules : Aesop.Index Aesop.SafeRuleInfo} {unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)}
  {forwardRules : Aesop.ForwardIndex} {forwardRuleNames : Lean.PHashSet Aesop.RuleName}
  {rulePatterns : Aesop.RulePatternIndex} {erased : Lean.PHashSet Aesop.RuleName}
  {ruleNames : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)}
  {normRules_1 : Aesop.Index Aesop.NormRuleInfo} {unsafeRules_1 : Aesop.Index Aesop.UnsafeRuleInfo}
  {safeRules_1 : Aesop.Index Aesop.SafeRuleInfo} {unfoldRules_1 : Lean.PHashMap Lean.Name (Option Lean.Name)}
  {forwardRules_1 : Aesop.ForwardIndex} {forwardRuleNames_1 : Lean.PHashSet Aesop.RuleName}
  {rulePatterns_1 : Aesop.RulePatternIndex} {erased_1 : Lean.PHashSet Aesop.RuleName}
  {ruleNames_1 : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)},
  { normRules := normRules, unsafeRules := unsafeRules, safeRules := safeRules, unfoldRules := unfoldRules,
        forwardRules := forwardRules, forwardRuleNames := forwardRuleNames, rulePatterns := rulePatterns,
        erased := erased, ruleNames := ruleNames } =
      { normRules := normRules_1, unsafeRules := unsafeRules_1, safeRules := safeRules_1, unfoldRules := unfoldRules_1,
        forwardRules := forwardRules_1, forwardRuleNames := forwardRuleNames_1, rulePatterns := rulePatterns_1,
        erased := erased_1, ruleNames := ruleNames_1 } →
    normRules = normRules_1 ∧
      unsafeRules = unsafeRules_1 ∧
        safeRules = safeRules_1 ∧
          unfoldRules = unfoldRules_1 ∧
            forwardRules = forwardRules_1 ∧
              forwardRuleNames = forwardRuleNames_1 ∧
                rulePatterns = rulePatterns_1 ∧ erased = erased_1 ∧ ruleNames = ruleNames_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Simplices in the nerve of categories are uniquely determined by their spine.
Indeed, this property describes the essential image of the nerve functor.  -/
CategoryTheory.Nerve.strictSegal : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.nerve C).StrictSegal
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instTransOrdOffset : Std.TransOrd Std.Time.Hour.Offset
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.IsComplete.out : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ.IsComplete → ∀ (s : Set α), μ s = 0 → MeasurableSet s
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {c : ℝ} {g : α → F}
  {l : Filter α} {f : α → R},
  Asymptotics.IsBigOWith c l f g → ∀ (c' : R), Asymptotics.IsBigOWith (‖c'‖ * c) l (fun x => c' * f x) g
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pullback_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X}
  {Z : C} {g : Z ⟶ Y}, CategoryTheory.Presieve.pullback f R g ↔ R (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.range_toFreeAddMonoid : ∀ {α : Type u_1}, Set.range ⇑FreeAddSemigroup.toFreeAddMonoid = {0}ᶜ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.ker_lift : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M)
  (HN : N ≤ φ.ker), (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc' : CategoryTheory.Limits.IsColimit c') {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (s : ↑(F.comp P).sections),
  (CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv hc').symm s =
    hc'.desc
      { pt := P,
        ι := { app := fun j => CategoryTheory.shrinkYonedaEquiv.symm (↑s (Opposite.unop j)), naturality := ⋯ } }
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The product of `AddSubmonoid`s is isomorphic to their product as `AddMonoid`s.  -/
AddSubmonoid.prodEquiv : {N : Type u_2} →
  [inst : AddZeroClass N] →
    {M : Type u_5} → [inst_1 : AddZeroClass M] → (s : AddSubmonoid M) → (t : AddSubmonoid N) → ↥(s.prod t) ≃+ ↥s × ↥t
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.halt.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ], sizeOf Turing.TM2.Stmt.halt = 1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R)
  (t : Subsemiring S), ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleObjApplyIsoOfEq.eq_1 : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) (X : C) (i : J) (h : i = j),
  CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_equiv_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), Subsemigroup.map ↑f ⊤ = ⊤
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_mul : ∀ {M : Type u_4} [inst : AddMonoid M] {x y : WithZero (Multiplicative M)}, x ≠ 0 → y ≠ 0 → (x * y).log = x.log + y.log
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instSMul : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      (I : Ideal R) →
        (M : Type u_4) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : SMul S R] → [inst_4 : SMul S M] → [IsScalarTower S R M] → SMul S (AdicCompletion I M)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mkPostcomp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y),
  CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.match_1.eq_1 : ∀ {α : Type u_2} (n : ℕ) (motive : { i // i ≤ n } → α → Sort u_1) (property : 0 ≤ n) (x : α)
  (h_1 : (property : 0 ≤ n) → (x : α) → motive ⟨0, property⟩ x)
  (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive ⟨i.succ, h⟩ x),
  (match ⟨0, property⟩, x with
    | ⟨0, property⟩, x => h_1 property x
    | ⟨i.succ, h⟩, x => h_2 i h x) =
    h_1 property x
-- Mathlib.Algebra.Order.Group.Lattice
mul_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] (a b c : α), c * (a ⊔ b) = c * a ⊔ c * b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The pushforward of presheaves of modules commutes with the forgetful functor
to presheaves of abelian groups.  -/
PresheafOfModules.pushforwardCompToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
            {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
              (φ : S ⟶ F.op.comp R) →
                (PresheafOfModules.pushforward φ).comp (PresheafOfModules.toPresheaf S) ≅
                  (PresheafOfModules.toPresheaf R).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ Ab).obj F.op)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- The only divisors of prime powers are prime powers. See `eq_pow_find_of_dvd_irreducible_pow`
for an explicit expression as a p-power (without using `count`).  -/
Associates.eq_pow_count_factors_of_dvd_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {p a : Associates α},
  Irreducible p → ∀ {n : ℕ}, a ∣ p ^ n → a = p ^ p.count a.factors
-- Mathlib.Order.RelSeries
LTSeries.head_le_last : ∀ {α : Type u_1} [inst : Preorder α] (x : LTSeries α), RelSeries.head x ≤ RelSeries.last x
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_add_length_eq_ringKrullDim_of_isRegular : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [IsLocalRing R] (rs : List R),
  RingTheory.Sequence.IsRegular R rs → ringKrullDim (R ⧸ Ideal.ofList rs) + ↑rs.length = ringKrullDim R
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
/-- The inclusion from an irreducible component of a Noetherian scheme.  -/
AlgebraicGeometry.Scheme.irreducibleComponentι : (X : AlgebraicGeometry.Scheme) →
  (Z : Set ↥X) →
    (hZ : Z ∈ irreducibleComponents ↥X) → [inst : AlgebraicGeometry.IsNoetherian X] → X.irreducibleComponent Z hZ ⟶ X
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.All.decidable : {α : Type u_1} → {P : α → Prop} → (t : Ordnode α) → [DecidablePred P] → Decidable (Ordnode.All P t)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} {z : ℤ}, a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p]