mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.X_sub_C_scaleRoots : ∀ {R : Type u_1} [inst : Ring R] (r s : R),
  (Polynomial.X - Polynomial.C r).scaleRoots s = Polynomial.X - Polynomial.C (r * s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_empty : ∀ {α : Type u} {β : Type v}, Std.DHashMap.Raw.Const.toList ∅ = []
-- Mathlib.Tactic.NormNum.Basic
/-- The result of negating a `norm_num` result.  -/
Mathlib.Meta.NormNum.Result.neg : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        (rα : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.Result.neg._auto_1) →
          Lean.MetaM (Mathlib.Meta.NormNum.Result q(-«$a»))
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.normBound.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b b_1 : Module.Basis ι ℤ ↥L),
  b = b_1 → ZLattice.normBound b = ZLattice.normBound b_1
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.instEquivLikeLinearEquiv : {R : Type u_7} →
  {S : Type u_8} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                (M : Type u_9) →
                  (M₂ : Type u_10) →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → EquivLike (M ≃ₛₗ[σ] M₂) M M₂
-- Lean.Meta.Tactic.Grind.OrderInsts
Lean.Meta.Grind.mkIsPreorderInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Topology.UniformSpace.Defs
comap_swap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.comap Prod.swap (uniformity α) = uniformity α
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the twist of the von Mangoldt function `Λ` by a Dirichlet character `χ` at `s`
equals the negative logarithmic derivative of the L-series of `χ` when `re s > 1`.  -/
DirichletCharacter.LSeries_twist_vonMangoldt_eq : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re →
    LSeries ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) s =
      -deriv (LSeries fun n => χ ↑n) s / LSeries (fun n => χ ↑n) s
-- Mathlib.CategoryTheory.Monad.Algebra
/-- A composition of monad morphisms gives the composition of corresponding functors.
 -/
CategoryTheory.Monad.algebraFunctorOfMonadHomComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ T₂ T₃ : CategoryTheory.Monad C} →
      (f : T₁ ⟶ T₂) →
        (g : T₂ ⟶ T₃) →
          CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g) ≅
            (CategoryTheory.Monad.algebraFunctorOfMonadHom g).comp (CategoryTheory.Monad.algebraFunctorOfMonadHom f)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [inst_2 : CategoryTheory.IsIso η],
  F.map₂ (CategoryTheory.inv η) = CategoryTheory.inv (F.map₂ η)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_inj : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (A B : T) {f g : A ⟶ B},
  CategoryTheory.Arrow.mk f = CategoryTheory.Arrow.mk g ↔ f = g
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_insert_le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true
-- Aesop.Forward.State
Aesop.instInhabitedHyp : Inhabited Aesop.Hyp
-- Mathlib.Order.Filter.Extr
IsMinOn.on_preimage : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
  IsMinOn f s (g b) → IsMinOn (f ∘ g) (g ⁻¹' s) b
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopRight` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `y ∈ s`.  -/
MonoidHom.ofClosureMEqTopRight : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        {s : Set M} →
          (f : M → N) → Submonoid.closure s = ⊤ → f 1 = 1 → (∀ (x y : M), y ∈ s → f (x * y) = f x * f y) → M →* N
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- The bijection `C(X, Y) ≃ Y` when `Y` is totally disconnected and `X` is connected.  -/
TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace : (X : Type u_3) →
  (Y : Type u_4) →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [TotallyDisconnectedSpace Y] → [ConnectedSpace X] → C(X, Y) ≃ Y
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv_eq_rightInv : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → p.leftInv i x = p.rightInv i x
-- Mathlib.Analysis.MeanInequalities
/-- **HM-GM inequality**: The harmonic mean is less than or equal to the geometric mean, weighted
version for real-valued nonnegative functions.  -/
Real.harm_mean_le_geom_mean_weighted : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  s.Nonempty → (∀ i ∈ s, 0 < w i) → ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 < z i) → (∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
-- Batteries.Recycling.RBTree.Basic
/-- `O(n log n)`. Build a tree from an unsorted array by inserting them one at a time.  -/
RBTree.RBMap.ofArray : {α : Type u} → {β : Type v} → Array (α × β) → (cmp : α → α → Ordering) → RBTree.RBMap α β cmp
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Convert a real number to a multiseries in an empty basis.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal : ℝ → Tactic.ComputeAsymptotics.MultiseriesExpansion []
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.normal.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a a_1 : Λ},
  Turing.TM1to1.Λ'.normal a = Turing.TM1to1.Λ'.normal a_1 → a = a_1
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_eq_image : ∀ {α : Type u} [inst : TopologicalSpace α] {F : Set α} {x : α} (h : x ∈ F),
  connectedComponentIn F x = Subtype.val '' connectedComponent ⟨x, h⟩
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.div_left : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b c : G₀}, Commute a c → Commute b c → Commute (a / b) c
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- `0` in the additive localization, defined as `0 -ₒ 0`.  -/
AddOreLocalization.zero : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → [Zero X] → AddOreLocalization S X
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.support_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : MulZeroOneClass R] [Nontrivial R],
  HahnSeries.support 1 = {0}
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.ExtDTreeMap.ofList : {α : Type u} →
  {β : α → Type v} →
    List ((a : α) × β a) → (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.ofList._auto_1) → Std.ExtDTreeMap α β cmp
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_le : ∀ {G : Type u_2} [inst : Group G] (S T : Submonoid G), S⁻¹ ≤ T ↔ S ≤ T⁻¹
-- Mathlib.Computability.PartrecCode
/-- A code for the identity function.  -/
Nat.Partrec.Code.id : Nat.Partrec.Code
-- Mathlib.Combinatorics.Matroid.Sum
/-- The sum of two matroids on `α` with disjoint ground sets, as a `Matroid α`.  -/
Matroid.disjointSum : {α : Type u_1} → (M N : Matroid α) → Disjoint M.E N.E → Matroid α
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.to_isEvenlyCovered_preimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X}, IsEvenlyCovered f x I → IsEvenlyCovered f x ↑(f ⁻¹' {x})
-- Init.Data.Option.Lemmas
Option.dite_none_right_eq_some : ∀ {α : Type u_1} {a : α} {p : Prop} {x : Decidable p} {b : p → Option α},
  (if h : p then b h else none) = some a ↔ ∃ (h : p), b h = some a
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.exportEntriesFn : {α β σ : Type} →
  Lean.ScopedEnvExtension.Descr α β σ →
    Lean.Environment →
      Lean.ScopedEnvExtension.StateStack α β σ → Lean.OLeanEntries (Array (Lean.ScopedEnvExtension.Entry α))
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.flat_of_preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteLimits F], CategoryTheory.RepresentablyFlat F
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.roots_charpoly_eq_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The kernel of a functor between subgroupoid is the preimage.  -/
CategoryTheory.Subgroupoid.ker : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type u_1} → [inst_1 : CategoryTheory.Groupoid D] → CategoryTheory.Functor C D → CategoryTheory.Subgroupoid C
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt : ∀ {pat s : String.Slice} {pos : s.Pos},
  pat.isEmpty = false →
    (String.Slice.Pattern.Model.MatchesAt pat pos ↔
      ∃ (h : String.Pos.Raw.IsValidForSlice s (pos.offset.increaseBy pat.utf8ByteSize)),
        String.Slice.Pattern.Model.IsLongestMatchAt pat pos (s.pos (pos.offset.increaseBy pat.utf8ByteSize) h))
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isInvInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_coe_le_norm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (x : α), ‖f x‖ ≤ ‖f‖
-- Mathlib.Algebra.Group.Nat.Hom
powersMulHom_symm_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (f : Multiplicative ℕ →* M), (powersMulHom M).symm f = f (Multiplicative.ofAdd 1)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
has_fderiv_at_filter_real_equiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ] F} {x : E} {L : Filter E},
  Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (nhds 0) ↔
    Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (nhds 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_base : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (i : ↑(IsProperLinearSet.basisSet✝ hs)),
  IsProperLinearSet.floor✝ hs (IsProperLinearSet.base✝ hs) i = 0
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f → Monotone f
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.forall : ∀ {X : Type u_1} {p : OnePoint X → Prop}, (∀ (x : OnePoint X), p x) ↔ p OnePoint.infty ∧ ∀ (x : X), p ↑x
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.comp_C_mul_X_coeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {r : R} {n : ℕ},
  (p.comp (Polynomial.C r * Polynomial.X)).coeff n = p.coeff n * r ^ n
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_induced : ∀ {X : Type u_1} {Y : Type u_2} {t : TopologicalSpace Y},
  CompletelyRegularSpace Y → ∀ (f : X → Y), CompletelyRegularSpace X
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.TreeMap.Raw.minKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_opIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.opIso P Q).inv =
    CategoryTheory.Limits.biprod.fst.op
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₃_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₃.Rel i₃ (c₃.next i₃) → ⋯ = ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
deriv_csin : ∀ {f : ℂ → ℂ} {x : ℂ}, DifferentiableAt ℂ f x → deriv (fun x => Complex.sin (f x)) x = Complex.cos (f x) * deriv f x
-- Lean.Expr
Lean.Expr.bvarIdx! : Lean.Expr → ℕ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_succ_eq_append : ∀ {n : ℕ}, (*...n + 1).toList = (*...n).toList ++ [n]
-- Mathlib.Algebra.Regular.Basic
AddCommute.isAddRightRegular_iff : ∀ {R : Type u_1} [inst : Add R] {a : R}, (∀ (b : R), AddCommute a b) → (IsAddRightRegular a ↔ IsAddLeftRegular a)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.proj_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D}, (CategoryTheory.StructuredArrow.proj S T).Faithful
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.symm_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hv : f v = 0) (hv' : autoParam (f (-v) = 0) LinearEquiv.transvection.symm_eq._auto_1),
  (LinearEquiv.transvection hv).symm = LinearEquiv.transvection hv'
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul`. -/
MonoidAlgebra.mul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : DecidableEq M] (x y : MonoidAlgebra R M)
  (m : M), (x * y).coeff m = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => if m₁ * m₂ = m then r₁ * r₂ else 0
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.coe_dfinsuppProd : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : CommMonoid M]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : Con M) (h : (i : ι) → β i → M)
  (f : Π₀ (i : ι), β i), ↑(f.prod h) = f.prod fun i b => ↑(h i b)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_ite : ∀ {c : Prop} {t e : UInt8} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.mkHomeomorph.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  DomAddAct.mkHomeomorph = { toEquiv := DomAddAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.finrank : ∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K] [h : NumberField.IsTotallyReal K],
  Module.finrank ℚ K = NumberField.InfinitePlace.nrRealPlaces K
-- Mathlib.Order.Bounded
Set.unbounded_le_univ : ∀ {α : Type u_1} [inst : LE α] [NoTopOrder α], Set.Unbounded (fun x1 x2 => x1 ≤ x2) Set.univ
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_toSpanSingleton : ∀ {E : Type u_2} [inst : AddCommMonoid E] [inst_1 : StarAddMonoid E] {S : Type u_5} [inst_2 : Semiring S]
  [inst_3 : StarAddMonoid S] [inst_4 : StarModule S S] [inst_5 : Module S E] [inst_6 : StarModule S E] (a : E),
  star (WithConv.toConv (LinearMap.toSpanSingleton S E a)) = WithConv.toConv (LinearMap.toSpanSingleton S E (star a))
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_cert x k p =
    p.beq' (Int.Internal.Linear.Poly.add 1 x (Int.Internal.Linear.Poly.num (-k)))
-- Mathlib.Data.Set.Finite.Range
Set.Finite.exists_subset_finite_image_eq : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {u : Set β},
  u.Finite → u ⊆ f '' s → ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
-- Init.Data.Order.Lemmas
Std.not_lt_iff_not_le_or_ge : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {a b : α}, ¬a < b ↔ ¬a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_lt_zero : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, ⌊a⌋ < 0 ↔ a < 0
-- Init.Control.Except
/-- Use a monadic action that may throw an exception as an action that may return an exception's value.

This is the inverse of `ExceptT.mk`.
 -/
ExceptT.run : {ε : Type u} → {m : Type u → Type v} → {α : Type u} → ExceptT ε m α → m (Except ε α)
-- Std.Data.DTreeMap.Raw.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.DTreeMap.Raw.Const.forMUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} →
      [Monad m] → {β : Type v} → (α × β → m PUnit.{w + 1}) → Std.DTreeMap.Raw α (fun x => β) cmp → m PUnit.{w + 1}
-- Mathlib.Algebra.Algebra.Pi
/-- Apply an algebra map component-wise along a vector.  -/
Pi.algebraMap : (ι : Type u_1) →
  (R : Type u_2) →
    (A : Type u_3) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (ι → R) →ₗ[R] ι → A
-- Mathlib.Algebra.Torsor.Defs
Equiv.constVSub.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  Equiv.constVSub p = { toFun := fun x => p -ᵥ x, invFun := fun x => -x +ᵥ p, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → Std.DTreeMap.Const.get! (Std.DTreeMap.Const.ofList l cmp) k = default
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.refl_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), (LinearIsometryEquiv.refl R E).trans e = e
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftPNatNat : Mathlib.Tactic.Ring.CSLift ℕ+ ℕ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.forIn_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ} {f : α × β → δ → m (ForInStep δ)},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] (P Q : W.Point),
  (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
-- Mathlib.Data.Sym.Sym2
Sym2.congr_right : ∀ {α : Type u_1} {a b c : α}, s(a, b) = s(a, c) ↔ b = c
-- Mathlib.GroupTheory.Divisible
ULift.instDivisibleBy.eq_1 : ∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α] [inst_3 : DivisibleBy A α],
  ULift.instDivisibleBy A α = { div := fun x a => { down := DivisibleBy.div x.down a }, div_zero := ⋯, div_cancel := ⋯ }
-- Batteries.Data.HashMap.Basic
/-- Variant of `ofList` which accepts a function that combines values of duplicated keys.
```
ofListWith [("one", 1), ("one", 2)] (fun v₁ v₂ => v₁ + v₂) = {"one" => 3}
```
 -/
Batteries.HashMap.ofListWith : {α : Type u_1} →
  {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → (β → β → β) → Batteries.HashMap α β
-- Mathlib.Data.Fintype.Perm
Fintype.card_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Fintype α]
  [inst_3 : Fintype β] (e : α ≃ β), Fintype.card (α ≃ β) = (Fintype.card α).factorial
-- Mathlib.Algebra.Group.Defs
AddMonoid.toAddZeroClass : {M : Type u} → [self : AddMonoid M] → AddZeroClass M
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.instIsIPCType : CategoryTheory.Limits.IsIPC (Type u)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.category : {J : Type w} → CategoryTheory.SmallCategory (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Alias** of `EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle`.

---

**Law of cosines** (cosine rule), angle-at-point form.  -/
EuclideanGeometry.law_cos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P),
  dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ -
      2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `G` is an extremal graph satisfying `p` if `G` has the maximum number of edges of any simple
graph, with fixed vertices, satisfying `p`.  -/
SimpleGraph.IsExtremal : {V : Type u_1} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → (SimpleGraph V → Prop) → Prop