mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SumIntegralComparisons
integral_le_sum_mul_Ico_of_antitone_monotone : ∀ {a b : ℕ} {f g : ℝ → ℝ},
  a ≤ b →
    AntitoneOn f (Set.Icc ↑a ↑b) →
      MonotoneOn g (Set.Icc (↑a - 1) (↑b - 1)) →
        0 ≤ f ↑b → 0 ≤ g (↑a - 1) → ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i
-- Lean.Level
Lean.mkLevelMaxEx : Lean.Level → Lean.Level → Lean.Level
-- Lean.Parser.Term
Lean.Parser.darrow : Lean.Parser.Parser
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.comul_def : ∀ {R : Type u} [inst : CommRing R] (X : CoalgCat R),
  CategoryTheory.ComonObj.comul = ModuleCat.ofHom CoalgebraStruct.comul
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.category.injEq : ∀ (cat cat_1 : Lean.Name),
  (Lean.Parser.ParserResolution.category cat = Lean.Parser.ParserResolution.category cat_1) = (cat = cat_1)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.iSup_lt_of_lt_cof`. -/
Ordinal.iSup_lt_ord : ∀ {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}}, Cardinal.mk α < a.cof → (∀ (i : α), f i < a) → ⨆ i, f i < a
-- Mathlib.Order.CompleteBooleanAlgebra
compl_eq_sSup_disjoint : ∀ {α : Type u} [inst : Order.Frame α] {a : α}, aᶜ = sSup {w | Disjoint w a}
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulActionHom.oneEmbeddingMap_bijective : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {one : Type u_5} [inst_2 : Unique one],
  Function.Bijective ⇑MulActionHom.oneEmbeddingMap
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.smul.eq_1 : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β],
  Function.Embedding.smul = { smul := fun g f => f.trans (Equiv.toEmbedding (MulAction.toPerm g)) }
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- `mapIdIso` gives rise to the lax unity constraint  -/
CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.LaxFunctor B C} (self : F.PseudoCore) {a : B}, (self.mapIdIso a).inv = F.mapId a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Restrict an injective non-unital star algebra homomorphism to a star algebra isomorphism  -/
StarAlgEquiv.ofInjective' : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [inst_8 : NonUnitalAlgHomClass F R A B] →
                          [inst_9 : StarHomClass F A B] →
                            (f : F) → Function.Injective ⇑f → A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range f)
-- Init.Meta.Defs
Lean.Syntax.decodeNameLit : String → Option Lean.Name
-- Lean.Syntax
Lean.Syntax.MonadTraverser.goUp : {m : Type → Type} → [t : Lean.Syntax.MonadTraverser m] → m Unit
-- Mathlib.Data.Num.Prime
PosNum.minFacAux.eq_1 : ∀ (n x : PosNum), n.minFacAux 0 x = n
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- A coalgebra homomorphism sends group-like elements to group-like elements.  -/
IsGroupLikeElem.map : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Coalgebra R A] [inst_5 : Module R B]
  [inst_6 : Coalgebra R B] {a : A} [inst_7 : FunLike F A B] [CoalgHomClass F R A B] (f : F),
  IsGroupLikeElem R a → IsGroupLikeElem R (f a)
-- Mathlib.NumberTheory.Divisors
Nat.prod_divisorsAntidiagonal : ∀ {M : Type u_1} [inst : CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ},
  ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.reverse_v : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  CliffordAlgebra.reverse ((CliffordAlgebra.EquivEven.v Q) m) = (CliffordAlgebra.EquivEven.v Q) m
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint : ∀ {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) [G.IsLeftAdjoint]
  [CategoryTheory.IsIso φ] [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPullbacks D] {M : SheafOfModules R}
  [M.IsQuasicoherent], ((SheafOfModules.pushforward φ).obj M).IsQuasicoherent
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_iInf : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ι → G.Subgraph}, (⨅ i, f i).verts = ⋂ i, (f i).verts
-- Std.Do.SPred.SPred
Std.Do.SPred.imp_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : Std.Do.SPred (σ :: σs)}, spred(P → Q) s = spred(P s → Q s)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instSubsingleton : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [Subsingleton M],
  Subsingleton (ArchimedeanClass M)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.sum : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → ∀ {y : E}, x + y ∈ insert x s → y ∈ Metric.eball 0 r → f (x + y) = p.sum y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceSub : Lean.Meta.Simp.DSimproc
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.name.inj : ∀ {n n_1 : String}, Lean.Elab.InlayHintLabel.name n = Lean.Elab.InlayHintLabel.name n_1 → n = n_1
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.isClosed_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A] [inst_5 : IsSemitopologicalSemiring A]
  (s : NonUnitalSubalgebra R A), IsClosed ↑s.topologicalClosure
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ), (-γ).shift a = -γ.shift a
-- Init.Tactics
/-- `mclear` is like `clear`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
  mintro HP
  mintro HQ
  mclear HP
  mexact HQ
```
 -/
Lean.Parser.Tactic.mclearMacro : Lean.ParserDescr
-- Lean.Widget.UserWidget
Lean.Widget.evalUserWidgetDefinition : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadOptions m] → [Lean.MonadError m] → Lean.Name → m Lean.Widget.UserWidgetDefinition
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₃ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'')
  (i j : ℕ) (h : i + 1 = j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P h).inv
      (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    CategoryTheory.CategoryStruct.comp (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst
      (HomologicalComplex.xPrevIso Q h).hom
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G] {X Y : Cᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.yonedaGrpObj G).map φ = GrpCat.ofHom (MonCat.Hom.hom ((CategoryTheory.yonedaMonObj G).map φ))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k = CategoryTheory.eqToIso ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.multipliable_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommMonoid β]
  [inst_3 : ContinuousMul β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ},
  Multipliable f L → ∀ (x : α), Multipliable (fun i => (f i) x) L
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_add : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) (x y : R), ↑(x + y) = ↑x + ↑y
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Path.Homotopic.Quotient.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (x₀ x₁ : X),
  Path.Homotopic.Quotient x₀ x₁ = Quotient (Path.Homotopic.setoid x₀ x₁)
-- Init.Prelude
Nat.lt_succ_self : ∀ (n : ℕ), n < n.succ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {S : C} (self : F.OneHypercoverDenseData J₀ J S) (i₁ i₂ : self.I₀)
  ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ self.X i₁) (p₂ : W₀ ⟶ self.X i₂),
  CategoryTheory.CategoryStruct.comp (F.map p₁) (self.f i₁) =
      CategoryTheory.CategoryStruct.comp (F.map p₂) (self.f i₂) →
    self.sieve₁₀ p₁ p₂ ∈ J₀ W₀
-- Mathlib.Order.Heyting.Hom
HeytingHomClass.toLatticeHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : HeytingAlgebra α} {inst_1 : HeytingAlgebra β}
  {inst_2 : FunLike F α β} [self : HeytingHomClass F α β], LatticeHomClass F α β
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWithAnnotateTerm : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.IsIso f], CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabSection : Lean.Elab.Command.CommandElab
-- Mathlib.Topology.Separation.Basic
/-- If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is
infinite.  -/
infinite_of_mem_nhds : ∀ {X : Type u_3} [inst : TopologicalSpace X] [T1Space X] (x : X) [hx : (nhdsWithin x {x}ᶜ).NeBot] {s : Set X},
  s ∈ nhds x → s.Infinite
-- Mathlib.Data.Countable.Defs
/-- A type `α` is uncountable if it is not countable.  -/
Uncountable : Sort u_1 → Prop
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.add_eq_sup : ∀ {α : Type u_5} [self : IdemSemiring α] (a b : α), a + b = a ⊔ b
-- Init.Data.Iterators.Basic
/-- Returns the succeeding iterator stored in an iterator step or `none` if the step is `.done`
and the iterator has finished.
 -/
Std.IterStep.successor : {α : Type u} → {β : Type w} → Std.IterStep α β → Option α
-- Lean.Parser.Term
Lean.Parser.Term.letIdDecl.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.setIntegral_tilted' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (f : α → ℝ) (g : α → E) {s : Set α},
  MeasurableSet s →
    ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) • g x ∂μ
-- Mathlib.Algebra.CharP.Lemmas
add_pow_expChar_pow_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p n : ℕ) [hR : ExpChar R p],
  Commute x y → (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
-- Init.SizeOf
Lean.Syntax.TSepArray.mk.sizeOf_spec : ∀ {ks : Lean.SyntaxNodeKinds} {sep : String} (elemsAndSeps : Array Lean.Syntax),
  sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
-- Mathlib.Order.Bounds.Basic
IsLUB.unique : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLUB s a → IsLUB s b → a = b
-- Qq.Macro
Qq.Impl.MVarSynth.term.injEq : ∀ (quotedType : Lean.Expr) (unquotedMVar : Lean.MVarId) (quotedType_1 : Lean.Expr) (unquotedMVar_1 : Lean.MVarId),
  (Qq.Impl.MVarSynth.term quotedType unquotedMVar = Qq.Impl.MVarSynth.term quotedType_1 unquotedMVar_1) =
    (quotedType = quotedType_1 ∧ unquotedMVar = unquotedMVar_1)
-- Lean.Server.InfoUtils
Lean.Elab.instMaxHoverableInfoPrio : Max Lean.Elab.HoverableInfoPrio
-- Mathlib.Tactic.NormNum.Core
/-- The name of the `norm_num` extension.  -/
Mathlib.Meta.NormNum.NormNumExt.name : Mathlib.Meta.NormNum.NormNumExt → Lean.Name
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_8 : FirstOrder.Field.FieldAxiom.leftDistrib.toSentence =
  (((FirstOrder.Language.var ∘ Sum.inr) 0 *
              ((FirstOrder.Language.var ∘ Sum.inr) 1 + (FirstOrder.Language.var ∘ Sum.inr) 2)).bdEqual
          ((FirstOrder.Language.var ∘ Sum.inr) 0 * (FirstOrder.Language.var ∘ Sum.inr) 1 +
            (FirstOrder.Language.var ∘ Sum.inr) 0 * (FirstOrder.Language.var ∘ Sum.inr) 2)).all.all.all
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_iInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {ι : Sort u_3} {S : ι → L.Substructure M},
  ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Batteries.Data.AssocList
Batteries.AssocList.modify.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (f : α → β → β) (a_1 : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.modify a f (Batteries.AssocList.cons a_1 b es) =
    match a_1 == a with
    | true => Batteries.AssocList.cons a (f a_1 b) es
    | false => Batteries.AssocList.cons a_1 b (Batteries.AssocList.modify a f es)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_mk : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (f : UpperHalfPlane → ℂ)
  (hf : ∀ γ ∈ Γ, SlashAction.map k γ f = f), ⇑{ toFun := f, slash_action_eq' := hf } = f
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (i j : ι),
  4 • (P.RootForm (P.root i)) (P.root j) ^ 2 =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
-- Mathlib.GroupTheory.CoprodI
/-- The inclusion of a summand into the free product.  -/
Monoid.CoprodI.of : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → M i →* Monoid.CoprodI M
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.hasTermAtRoot.go : ℕ → Lean.Meta.Grind.SolverTerms → Bool
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x`, its domain chart's target `(h.domChart.extend I).target`
is mapped to its codomain chart's target `(h.domChart.extend J).target`:
see `map_target_subset_target` for a version stated using images.  -/
Manifold.IsImmersionAt.target_subset_preimage_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x),
  (h.domChart.extend I).target ⊆ (⇑h.equiv ∘ fun x_1 => (x_1, 0)) ⁻¹' (h.codChart.extend J).target
-- Mathlib.Algebra.Group.Units.Defs
divp_one : ∀ {α : Type u} [inst : Monoid α] (a : α), a /ₚ 1 = a
-- Init.Data.Range.Polymorphic.UInt
UInt8.instHasSize_1 : Std.Rxo.HasSize UInt8
-- Mathlib.Topology.Category.TopCat.Limits.Konig
_private.Mathlib.Topology.Category.TopCat.Limits.Konig.0.TopCat.FiniteDiagramArrow : {J : Type u} → [CategoryTheory.SmallCategory J] → Finset J → Type (max 0 u)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
_private.Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord.0.NumberField.mixedEmbedding.abs_of_mem_polarCoordReal_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realMixedSpace K},
  x ∈ (NumberField.mixedEmbedding.polarCoordReal K).target → ∀ (w : { w // w.IsComplex }), |(x.2 w).1| = (x.2 w).1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.unop_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op), c.unop.pt = Opposite.unop c.pt
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  {X₁ X₂ : P.FullSubcategory} (f : X₁ ⟶ X₂) (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.obj
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sections_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s t : M.sections), (∀ (X : Cᵒᵖ), ↑s X = ↑t X) → s = t
-- Mathlib.ModelTheory.Definability
Set.definable_finset_inf : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2}
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → ∀ (s : Finset ι), A.Definable L (s.inf f)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_id_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ],
  p.IsHomLift (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id R) f) φ
-- Lean.Elab.DocString
/-- Built-in docstring code blocks, for bootstrapping.
 -/
Lean.Doc.builtinDocCodeBlocks : IO.Ref (Lean.NameMap (Array (Lean.Name × Lean.Doc.DocCodeBlockExpander)))
-- Mathlib.Analysis.Convex.Uniform
UniformConvexSpace.mk : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E],
  (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ) →
    UniformConvexSpace E
-- Init.Data.Nat.Div.Basic
Nat.add_mul_div_right : ∀ (x y : ℕ) {z : ℕ}, 0 < z → (x + y * z) / z = x / z + y
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNontrivialSubalgebra : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommSemiring R] [Nontrivial Γ] [Nontrivial R], Nontrivial (Subalgebra R (HahnSeries Γ R))
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.instInhabitedState : Inhabited Lean.ParseImports.State
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.left : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence X Y] →
          CategoryTheory.MonoidalCoherence
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) Y
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
factorization.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] (n n_1 : α), n = n_1 → factorization n = factorization n_1
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.mk.injEq : ∀ (cmdName : String) (wrapper : Lean.Name) (requireProp isInstance : Bool) (cmdName_1 : String) (wrapper_1 : Lean.Name)
  (requireProp_1 isInstance_1 : Bool),
  ({ cmdName := cmdName, wrapper := wrapper, requireProp := requireProp, isInstance := isInstance } =
      { cmdName := cmdName_1, wrapper := wrapper_1, requireProp := requireProp_1, isInstance := isInstance_1 }) =
    (cmdName = cmdName_1 ∧ wrapper = wrapper_1 ∧ requireProp = requireProp_1 ∧ isInstance = isInstance_1)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum is unaffected by adding the base point, whether
or not present, to the set of points.  -/
Finset.weightedVSubOfPoint_insert : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι),
  ((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_div_prod_filter : ∀ {α : Type u_1} {M : Type u_5} {G : Type u_8} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : CommGroup G] (g : α → M → G),
  f.prod g / (Finsupp.filter p f).prod g = (Finsupp.filter (fun a => ¬p a) f).prod g