mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- If `g : 𝒜 →+*ᵍ ℬ` is a graded ring homomorphism and `f : A` then we have a map
`Away 𝒜 f →+* Away ℬ (g f)`.  -/
HomogeneousLocalization.Away.map : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} →
                  [inst_5 : GradedRing 𝒜] →
                    {B : Type u_4} →
                      {τ : Type u_5} →
                        [inst_6 : CommRing B] →
                          [inst_7 : SetLike τ B] →
                            [inst_8 : AddSubgroupClass τ B] →
                              {ℬ : ι → τ} →
                                [inst_9 : GradedRing ℬ] →
                                  (g : 𝒜 →+*ᵍ ℬ) →
                                    (f : A) → HomogeneousLocalization.Away 𝒜 f →+* HomogeneousLocalization.Away ℬ (g f)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM_eq_toArray_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toArray =
    (Std.IterM.mapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toArray
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.hom.app X) = CategoryTheory.CategoryStruct.id X.fst
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)
-- Mathlib.Logic.Function.Basic
Function.update_self : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a),
  Function.update f a v a = v
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Relations.tensor_relation : ∀ {A : Type u} [inst : CommRing A] (relations₁ : Module.Relations A) (relations₂ : Module.Relations A)
  (x : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R),
  (relations₁.tensor relations₂).relation x =
    match x with
    | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL relations₁.G g₂) (relations₁.relation r₁)
    | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)
-- Lean.Compiler.LCNF.Types
/-- `erased` represents type arguments, propositions and proofs which are no longer relevant at this
point in time.
 -/
Lean.Compiler.LCNF.ImpureType.erased : Lean.Expr
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ConfirmRupHintFoldEntailsMotive : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    ℕ →
      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
          Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool →
        Prop
-- Init.Data.BitVec.Bitblast
/-- If `y &&& z = 0`, `x <<< (y ||| z) = x <<< y <<< z`.
This follows as `y &&& z = 0` implies `y ||| z = y + z`,
and thus `x <<< (y ||| z) = x <<< (y + z) = x <<< y <<< z`.
 -/
BitVec.shiftLeft_or_of_and_eq_zero : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y z : BitVec w₂}, y &&& z = 0#w₂ → x <<< (y ||| z) = x <<< y <<< z
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instMonoid : {𝕜 : Type u_1} → [inst : SeminormedRing 𝕜] → [NormOneClass 𝕜] → Monoid ↑(Metric.closedBall 0 1)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- `Projective.over X` provides an arbitrarily chosen projective object equipped with
an epimorphism `Projective.π : Projective.over X ⟶ X`.
 -/
CategoryTheory.Projective.over : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnoughProjectives C] → C → C
-- Lean.Meta.LetToHave
/-- The number of transformed `let` expressions. See `incCount`.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.count : Lean.Meta.LetToHave.State✝ → ℕ
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.lift.eq_1 : ∀ (R : Type u_1) {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  FreeAlgebra.lift R =
    { toFun := FreeAlgebra.liftAux✝ R, invFun := fun F => ⇑F ∘ FreeAlgebra.ι R, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getEntryLT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.getEntryLTD k r ⟨ky, y⟩
    else Std.DTreeMap.Internal.Impl.getEntryLT k l ⋯ ⋯
-- Init.Omega.Int
Lean.Omega.Int.ofNat_pos : ∀ {a : ℕ}, 0 < ↑a ↔ 0 < a
-- Mathlib.Algebra.Group.Commute.Basic
AddSemiconjBy.function_semiconj_add_right_swap : ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Function.Semiconj (fun x => x + a) (fun x => x + c) fun x => x + b
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- A function `f` maps downwards closed sets (atBot sets) to downwards closed sets when it is a
Galois coinsertion. The Galois "coinsertion" and "connection" is weakened to only require it to be
an insertion and a connection below `b`.  -/
Filter.map_atBot_eq_of_gc_preorder : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] [inst_2 : Preorder β] [IsCodirectedOrder β]
  {f : α → β},
  Monotone f →
    ∀ (b : β), (∀ c ≤ b, ∃ x, f x = c ∧ ∀ (a : α), c ≤ f a ↔ x ≤ a) → Filter.map f Filter.atBot = Filter.atBot
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListIfNewₘ.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (l : List ((a : α) × β a)),
  m.insertListIfNewₘ l =
    match l with
    | [] => m
    | hd :: tl => (m.insertIfNew hd.fst hd.snd).insertListIfNewₘ tl
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default
-- Lean.Data.Lsp.Diagnostics
/-- A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.  -/
Lean.Lsp.DiagnosticWith.source? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option String
-- Mathlib.RingTheory.Trace.Quotient
Ideal.quotEquivOfEq.congr_simp : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I = J),
  Ideal.quotEquivOfEq h = Ideal.quotEquivOfEq h
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_eq_mrange : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M), Submonoid.closure s = MonoidHom.mrange (FreeMonoid.lift Subtype.val)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupNormClass.toNormedAddCommGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddCommGroup α] [inst_2 : AddGroupNormClass F α ℝ]
  (f : F) (x : α), ‖x‖ = f x
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.mk : ∀ {l : Filter ℂ},
  Filter.Tendsto Complex.re l Filter.atTop →
    (∀ (n : ℕ), (fun z => z.im ^ n) =O[l] fun z => Real.exp z.re) → Complex.IsExpCmpFilter l
-- Mathlib.Probability.BrownianMotion.Basic
/-- If `B` is a pre-Brownian motion and `c > 0`, then
`t ↦ (√c)⁻¹ B (c t)` is a pre-Brownian motion.  -/
ProbabilityTheory.IsPreBrownianReal.smul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ {c : NNReal}, c ≠ 0 → ProbabilityTheory.IsPreBrownianReal (fun t ω => (√↑c)⁻¹ * B (c * t) ω) P
-- Qq.Macro
Qq.Impl.MVarSynth.level.injEq : ∀ (unquotedMVar unquotedMVar_1 : Lean.LMVarId),
  (Qq.Impl.MVarSynth.level unquotedMVar = Qq.Impl.MVarSynth.level unquotedMVar_1) = (unquotedMVar = unquotedMVar_1)
-- Init.Data.BitVec.Lemmas
BitVec.add_left_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), x + z = y + z ↔ x = y
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_map : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
  UniformContinuous (SeparationQuotient.map f)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.prod_ext : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {f g : M × M₂ →L[R] M₃},
  f ∘SL ContinuousLinearMap.inl R M M₂ = g ∘SL ContinuousLinearMap.inl R M M₂ →
    f ∘SL ContinuousLinearMap.inr R M M₂ = g ∘SL ContinuousLinearMap.inr R M M₂ → f = g
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {Z : Type u_3} [inst_2 : MetricSpace Z]
  (D : Delone.DeloneSet X) (f : X ≃ Y) (g : Y ≃ Z) (K₁f K₂f K₁g K₂g : NNReal) (hf₁_pos : 0 < K₁f) (hf₂_pos : 0 < K₂f)
  (hg₁_pos : 0 < K₁g) (hg₂_pos : 0 < K₂g) (hf_anti : AntilipschitzWith K₁f ⇑f) (hf_lip : LipschitzWith K₂f ⇑f)
  (hg_anti : AntilipschitzWith K₁g ⇑g) (hg_lip : LipschitzWith K₂g ⇑g),
  Delone.DeloneSet.mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
      (Delone.DeloneSet.mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    Delone.DeloneSet.mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a function `f` is continuous on a closed set `s` and it is
smaller than a value in its image away from compact sets, then it has a maximum on this set.  -/
ContinuousOn.exists_isMaxOn' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] {s : Set β} {f : β → α},
  ContinuousOn f s →
    IsClosed s →
      ∀ {x₀ : β}, x₀ ∈ s → (∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x ≤ f x₀) → ∃ x ∈ s, IsMaxOn f s x
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The adjunction between forming the free category on a reflexive quiver, and forgetting a category
to a reflexive quiver.
 -/
CategoryTheory.ReflQuiv.adj : CategoryTheory.Cat.freeRefl ⊣ CategoryTheory.ReflQuiv.forget
-- Mathlib.Order.WithBot
/-- `WithTop.ofDual` is the equivalence sending `⊤` to `⊥` and any `a : αᵒᵈ` to `ofDual a : α`.
See `WithTop.toDualBotEquiv` for the related order-iso.  -/
WithTop.ofDual : {α : Type u_1} → WithTop αᵒᵈ ≃ WithBot α
-- Mathlib.NumberTheory.NumberField.House
/-- `c` is defined as the product of the maximum absolute
value of the entries of the inverse of the matrix `basisMatrix` and  `finrank ℚ K`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c : (K : Type u_1) → [inst : Field K] → [NumberField K] → [DecidableEq (K →+* ℂ)] → ℝ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_1 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.yield c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.yield c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_1 c property
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.inc_eqOn : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → Set.EqOn H.Inc G.Inc H.edgeSet
-- Init.Data.SInt.Lemmas
ISize.ofInt_int64ToInt : ∀ (x : Int64), ISize.ofInt x.toInt = x.toISize
-- Mathlib.Data.Multiset.FinsetOps
Multiset.le_ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u
-- Mathlib.Data.Ordmap.Ordset
Ordset.pos_size_of_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] {x : α} {t : Ordset α}, x ∈ t → 0 < t.size
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.comap_pure : ∀ {α : Type u} {β : Type v} {m : α → β} (a : α) (inj : Function.Injective m) (large : Set.range m ∈ pure (m a)),
  (pure (m a)).comap inj large = pure a
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.nilpotent : ∀ (G : Type u_2) [inst : Group G] [Group.IsNilpotent G], ∃ n, Subgroup.upperCentralSeries G n = ⊤
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} {c : C},
  (∀ (E : L.LeftExtension F) (a : E.IsPointwiseLeftKanExtensionAt c),
      Nonempty (((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c)) →
    G.PreservesPointwiseLeftKanExtensionAt F L c
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.isUniformEmbedding_toFun_finite : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β], IsUniformEmbedding ⇑(UniformOnFun.toFun {s | s.Finite})
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.add_compLinearMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M),
  (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g
-- Lean.DocString.Markdown
/-- Looks up the inline Markdown renderer registered for `typeName`, if any.  -/
Lean.Doc.inlineRendererFor : Lean.Name → Lean.CoreM (Option Lean.Doc.InlineMdRenderer)
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_strictMono : StrictMono Nat.centralBinom
-- Mathlib.SetTheory.Cardinal.Order
/-- We define the order on cardinal numbers by `#α ≤ #β` if and only if
there exists an embedding (injective function) from α to β.  -/
Cardinal.instLE : LE Cardinal.{u}
-- Init.Data.UInt.Bitwise
UInt8.toUSize_shiftLeft : ∀ (a b : UInt8), (a <<< b).toUSize = a.toUSize <<< (b % 8).toUSize % 256
-- Mathlib.Data.Setoid.Partition
/-- Makes the equivalence classes of an equivalence relation.  -/
Setoid.classes : {α : Type u_1} → Setoid α → Set (Set α)
-- Mathlib.Geometry.Manifold.Instances.Quotient
/-- The induced charted space structure on the quotient of a charted space by a free, properly
discontinuous group action.  -/
MulAction.instChartedSpaceQuotient : {M : Type u_1} →
  [inst : TopologicalSpace M] →
    {G : Type u_2} →
      [inst_1 : Group G] →
        [inst_2 : MulAction G M] →
          [ProperlyDiscontinuousSMul G M] →
            [ContinuousConstSMul G M] →
              [IsCancelSMul G M] →
                [T2Space M] →
                  [LocallyCompactSpace M] →
                    {H : Type u_3} →
                      [inst_8 : TopologicalSpace H] →
                        [ChartedSpace H M] → ChartedSpace H (MulAction.orbitRel.Quotient G M)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure.eq_1 : ∀ (p : ↑unitInterval),
  ProbabilityTheory.geometricMeasure p =
    if p ≠ 0 then MeasureTheory.Measure.sum fun n => ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • MeasureTheory.Measure.dirac n
    else MeasureTheory.Measure.dirac 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.toMultiplicative_single : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Add M] (m : M) (r : R),
  (AddMonoidAlgebra.toMultiplicative R M) (AddMonoidAlgebra.single m r) =
    MonoidAlgebra.single (Multiplicative.ofAdd m) r
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_setOfPred_im_lt : ∀ (a : ℝ), closure {z | z.im < a} = {z | z.im ≤ a}
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_prodMap' : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {M₄ : Type u_5} [inst_10 : TopologicalSpace M₄] [inst_11 : AddCommMonoid M₄]
  [inst_12 : Module R M₄] (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄), ⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The sum of two right homotopies is a right homotopy between the sum of the respective
morphisms.  -/
CategoryTheory.Arrow.RightHomotopy.add : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f₁ g₁ f₂ g₂ : u ⟶ v} →
          CategoryTheory.Arrow.RightHomotopy f₁ g₁ →
            CategoryTheory.Arrow.RightHomotopy f₂ g₂ → CategoryTheory.Arrow.RightHomotopy (f₁ + f₂) (g₁ + g₂)
-- Mathlib.FieldTheory.Finite.Basic
Subfield.roots_X_pow_char_sub_X_bot : ∀ (F : Type u_3) [inst : Field F] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP F p],
  (Polynomial.X ^ p - Polynomial.X).roots = Finset.univ.val
-- Std.Internal.Parsec.ByteArray
/-- Skip whitespace: tabs, newlines, carriage returns, and spaces.
 -/
Std.Internal.Parsec.ByteArray.ws : Std.Internal.Parsec.ByteArray.Parser Unit
-- Init.Data.Option.Array
Option.mem_toArray : ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ o.toArray ↔ o = some a
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.TacticMVarKind.maybeWithoutRecovery : {α : Type} → Lean.Elab.Term.TacticMVarKind → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mk.congr_simp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (dpow dpow_1 : ℕ → A → A) (e_dpow : dpow = dpow_1)
  (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1)
  (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I)
  (dpow_add :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y)
  (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x)
  (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x)
  (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x),
  { dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem,
      dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } =
    { dpow := dpow_1, dpow_null := ⋯, dpow_zero := ⋯, dpow_one := ⋯, dpow_mem := ⋯, dpow_add := ⋯, dpow_mul := ⋯,
      mul_dpow := ⋯, dpow_comp := ⋯ }
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_iUnion_eq_of_finite : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {U : Set S} {κ : Type u_4} [Finite κ] (s : κ → Set S),
  ⋃ i, s i = U → (∀ (i : κ), IsCompactOpenCovered f (s i)) → IsCompactOpenCovered f U
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A sufficient criteria for a convex cone `C` to be generating is that top is less than or equal
to the linear span of `C`.  -/
ConvexCone.IsGenerating.of_top_le_span : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C : ConvexCone R M}, ⊤ ≤ Submodule.span R ↑C → C.IsGenerating
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rcc_eq_some_iff : ∀ {k m n i : ℕ}, (m...=n).toList[i]? = some k ↔ i < n + 1 - m ∧ m + i = k
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_1 ()
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.find_contract : ∀ {k : Type u_1} [inst : Field k] {a : Polynomial k},
  a ≠ 0 →
    Polynomial.derivative a = 0 →
      ringChar k ≠ 0 →
        ∃ ca, ca ≠ 0 ∧ a = (Polynomial.expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (b : β k) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- Left quasi-inverses compose in the opposite order.  -/
LinearMap.IsLeftQuasiInverse.comp : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂},
  u'.IsLeftQuasiInverse u → v'.IsLeftQuasiInverse v → (u' ∘ₗ v').IsLeftQuasiInverse (v ∘ₗ u)
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_antitone : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCancelCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β}, Antitone fun x => IsAddFreimanHom x A B f
-- Mathlib.Data.Set.Function
Set.BijOn.iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α}, Set.BijOn f s s → ∀ (n : ℕ), Set.BijOn f^[n] s s
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.normedAddCommGroup : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [AddSubgroupClass S E] → (s : S) → NormedAddCommGroup ↥s
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Algebraically closed fields are infinite since `Xⁿ⁺¹ - 1` is separable when `#K = n`  -/
IsAlgClosed.instInfinite : ∀ {K : Type u_1} [inst : Field K] [IsAlgClosed K], Infinite K