mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.Grp C),
  (CategoryTheory.Functor.mapGrpIdIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- An even Dirichlet character is an even function.  -/
DirichletCharacter.Even.to_fun : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} {χ : DirichletCharacter S m}, χ.Even → Function.Even ⇑χ
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivWithinAt.eq_1 : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (s : Set 𝕜) (x : 𝕜),
  HasDerivWithinAt f f' s x = HasDerivAtFilter f f' (nhdsWithin x s ×ˢ pure x)
-- Mathlib.Data.List.Perm.Basic
List.Perm.product_right : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (t₁ : List β), l₁.Perm l₂ → (l₁.product t₁).Perm (l₂.product t₁)
-- Mathlib.Analysis.Analytic.Basic
analyticWithinAt_insert : ∀ {𝕜 : 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} {s : Set E}
  {x y : E}, AnalyticWithinAt 𝕜 f (insert y s) x ↔ AnalyticWithinAt 𝕜 f s x
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- `npow` of `OreLocalization`  -/
OreLocalization.npow : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → ℕ → OreLocalization S R → OreLocalization S R
-- Mathlib.NumberTheory.Divisors
Int.neg_one_mem_divisors : ∀ {z : ℤ}, -1 ∈ z.divisors ↔ z ≠ 0
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.triangleRotation_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.triangleRotation C).unitIso = CategoryTheory.Pretriangulated.rotCompInvRot
-- Std.Data.Iterators.Producers.Repeat
/-- Creates an infinite iterator from an initial value `init` and a function `f : α → α`.
First it yields `init`, and in each successive step, the iterator applies `f` to the previous value.
So if the iterator just emitted `a`, in the next step it will yield `f a`. In other words, the
`n`-th value is `Nat.repeat f n init`.

For example, if `f := (· + 1)` and `init := 0`, then the iterator emits all natural numbers in
order.

**Termination properties:**

* `Finite` instance: not available and never possible
* `Productive` instance: always
 -/
Std.Iter.repeat : {α : Type w} → (f : α → α) → α → Std.Iter α
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- The range in the source document where the command will be inserted.  -/
SelectInsertParamsClass.replaceRange : {α : Type} → [self : SelectInsertParamsClass α] → α → Lean.Lsp.Range
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.instIsFiniteMeasureRestrictSpanningSetsTrim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : MeasureTheory.Measure α)
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)] (n : ℕ),
  MeasureTheory.IsFiniteMeasure (μ.restrict (MeasureTheory.spanningSets (μ.trim hm) n))
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ],
  s.contains pat =
    Std.Iter.any
      (fun x =>
        match x with
        | String.Slice.Pattern.SearchStep.matched startPos endPos => true
        | x => false)
      (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s)
-- Mathlib.Order.Interval.Finset.Box
Prod.card_box_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : Ring β]
  [inst_4 : PartialOrder β] [IsOrderedRing β] [inst_6 : LocallyFiniteOrder α] [inst_7 : LocallyFiniteOrder β]
  [inst_8 : DecidableEq α] [inst_9 : DecidableEq β] [inst_10 : DecidableLE (α × β)] (n : ℕ),
  (Finset.box (n + 1)).card =
    (Finset.Icc (-↑n.succ) ↑n.succ).card * (Finset.Icc (-↑n.succ) ↑n.succ).card -
      (Finset.Icc (-↑n) ↑n).card * (Finset.Icc (-↑n) ↑n).card
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.mono_inr : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.Types.Pushout.inr f g)
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable_iff_of_re_eq_re : ∀ {f : ℕ → ℂ} {s s' : ℂ}, s.re = s'.re → (LSeriesSummable f s ↔ LSeriesSummable f s')
-- Lean.Util.CollectMVars
Lean.CollectMVars.State : Type
-- Lean.ToExpr
Lean.instToExprRat.mkInt : ℤ → Lean.Expr
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A copresheaf valued in a category `A` with arbitrary coproducts, can be extended to the category
of formal coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.eval : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [CategoryTheory.Limits.HasCoproducts A] →
          CategoryTheory.Functor (CategoryTheory.Functor C A)
            (CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) A)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_inv_nat_pos : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (uniformity α).HasBasis (fun n => 0 < n) fun n => {p | dist p.1 p.2 < 1 / ↑n}
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.neg : ∀ {α : Type u_1} {n : Type u_4} [inst : AddGroup α] [inst_1 : StarAddMonoid α] {A : Matrix n n α},
  A.IsHermitian → (-A).IsHermitian
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicAbv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b),
  v.adicAbv hb = { toFun := fun x => ↑(v.adicAbvDef hb x), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
-- Mathlib.RingTheory.FinitePresentation
Algebra.FinitePresentation.mk : ∀ {R : Type w₁} {A : Type w₂} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → Algebra.FinitePresentation R A
-- Mathlib.Topology.Category.Profinite.Limits
/-- A one-element space is terminal in `Profinite`  -/
Profinite.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (Profinite.of PUnit.{u + 1})
-- Aesop.Frontend.Saturate
Aesop.Frontend.Parser.usingRuleSets : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.extension_incl : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : LieAlgebra.IsExtension i p), h.extension.incl = i
-- Mathlib.RingTheory.HahnSeries.Basic
/-- If `Γ` is linearly ordered and `R` has zero, then `R⟦Γ⟧` consists of
formal series over `Γ` with coefficients in `R`, whose supports are well-founded.  -/
HahnSeries : (Γ : Type u_1) → (R : Type u_2) → [PartialOrder Γ] → [Zero R] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
        i ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv h_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {fallback v : β}, Std.DHashMap.Raw.Const.getD (m.insert k v) k fallback = v
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.isSStronglyConnected_iff : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsSStronglyConnected V ↔ ∀ (i j : V), ∃ p, 0 < p.length
-- Mathlib.RingTheory.Polynomial.Basic
/-- The only constant in a maximal ideal over a field is `0`.  -/
Ideal.eq_zero_of_constant_mem_of_maximal : ∀ {R : Type u} [inst : Ring R],
  IsField R → ∀ (I : Ideal (Polynomial R)) [hI : I.IsMaximal] (x : R), Polynomial.C x ∈ I → x = 0
-- Batteries.Data.List.Basic
List.swapAt.eq_1 : ∀ {α : Type u_1} (xs : List α) (i : ℕ) (v : α), xs.swapAt i v = (xs[i]?.getD v, xs.set i v)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.instFunctorHetT : {m : Type w → Type w'} → [Functor m] → Functor (Std.Iterators.HetT m)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.of_le : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {κ' : Cardinal.{w}} [inst_2 : Fact κ'.IsRegular],
  κ' ≤ κ → CategoryTheory.IsCardinalFiltered J κ'
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_descFactorial_eq_ascFactorial' : ∀ (n k : ℕ), (n + k - 1).descFactorial k = n.ascFactorial k
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.prod_normalizedFactors_eq : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizationMonoid α]
  [inst_2 : UniqueFactorizationMonoid α] {a : α},
  a ≠ 0 → (UniqueFactorizationMonoid.normalizedFactors a).prod = normalize a
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is submultiplicative.  -/
norm_mul_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P → MeasureTheory.IsProbabilityMeasure P
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_coe_nonneg : ∀ (x : ℝ), 0 ≤ ArchimedeanClass.mk ↑x
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y), P.Factors f → P.Factors g → P.Factors (f + g)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n'), CochainComplex.HomComplex.Cochain.leftUnshift 0 n hn' = 0
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isIso₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.IsIso T.mor₃ → CategoryTheory.Limits.IsZero T.obj₂
-- Lean.Elab.InfoTree.Types
/-- A source position to use for "go to definition", to override the default.  -/
Lean.Elab.DelabTermInfo.location? : Lean.Elab.DelabTermInfo → Option Lean.DeclarationLocation
-- Init.Data.List.Lemmas
/-- Loop invariant for `eraseDupsBy.loop`: membership in the result equals
membership in the remaining list or the accumulator.  -/
_private.Init.Data.List.Lemmas.0.List.mem_eraseDupsBy_loop : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l acc : List α},
  a ∈ List.eraseDupsBy.loop (fun x1 x2 => x1 == x2) l acc ↔ a ∈ l ∨ a ∈ acc
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedResolvableCompletionItem : Inhabited Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.genWeightSpaceOf_ne_bot : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M) (x : L), LieModule.genWeightSpaceOf M (χ x) x ≠ ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- If `f` and `g` are in `X.PtSimplex n x`, then `RelStruct f g i.castSucc`
identifies to `MulStruct .const f g i`.  -/
SSet.PtSimplex.relStructCastSuccEquivMulStruct : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g : X.PtSimplex n x} →
        {i : Fin n} → f.RelStruct g i.castSucc ≃ SSet.PtSimplex.MulStruct SSet.RelativeMorphism.const f g i
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.toBasisAt_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {x : M} {n : WithTop ℕ∞} (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u) (i : ι), (hs.toBasisAt hx) i = s i x
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- Sections of `F ⋙ yoneda.obj X` identify to natural
transformations `(const J).obj X ⟶ F`.  -/
CategoryTheory.Limits.compYonedaSectionsEquiv : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          (X : C) →
            ↑(F.comp (CategoryTheory.yoneda.obj X)).sections ≃
              ((CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_inf : ∀ {M : Type u_1} [inst : Monoid M] (S T : Submonoid M), (S ⊓ T).units = S.units ⊓ T.units
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if `x` and `y` commute, then
`NormedSpace.exp (x+y) = (NormedSpace.exp x) * (NormedSpace.exp y)`.  -/
NormedSpace.exp_add_of_commute : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {x y : 𝔸},
  Commute x y → NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_zero_iff : ∀ {R : Type u} [inst : LinearOrder R] {a b : Tropical (WithTop R)}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α) (b : β),
  Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b with
      | (replaced, ⟨r, property⟩) => (replaced, r)
    else (none, m)
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instProductive : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [Std.Iterators.Productive α m]
  {P : β → Prop}, Std.Iterators.Productive (Std.Iterators.Types.Attach α m P) m
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instAdd.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupNorm.instAdd =
    {
      add := fun p q =>
        let __src := p.toAddGroupSeminorm + q.toAddGroupSeminorm;
        { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.is_comm : ∀ {M : Type u_2} {inst : Mul M} [self : IsMulCommutative M], Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Topology.ClusterPt
Filter.HasBasis.clusterPt_iff_forall_mem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X},
  F.HasBasis p s → (ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure (s i))
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valueGroup₀_hom_extensionValuation.eq_1 : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  Valued.valueGroup₀_hom_extensionValuation =
    { toFun := fun x => Valued.extensionValuation.restrict ↑⋯.choose, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Tactic.Module
/-- Given a goal parseable as a linear combination `⊢ a • x + ... + b • y = c • x + ... + d • y`,
`match_scalars` splits up the goal into equalities of the scalars for each respective atom. This
means the example goal above is replaced by goals `⊢ a = c` (from `x`), ..., `⊢ b = d` (from `y`).

The `module` tactic is equivalent to `match_scalars <;> ring1`.

`match_scalars` can parse into expressions made of the operators `+`, `-`, `•` and the numeral `0`.
Any other subexpressions (including variables) are treated as atoms.
If the goal is an equality in the type `M`, then `match_scalars` requires an `AddCommMonoid M`
instance. If the goal contains a scalar multiplication `(a : R) • (x : M)`, this requires a
`Semiring R` and `Module R M` instance. If any of the instances are missing, `match_scalars` fails.

The scalar type for the goals produced by the `match_scalars` tactic is the largest scalar type
encountered; for example, if `ℕ`, `ℚ` and a characteristic-zero field `K` all occur as scalars, then
the goals produced are equalities in `K` with the appropriate casts (from `ℕ`, `ℤ`, `ℚ`) and
`algebraMap`s (otherwise) inserted. Inserted casts are simplified by lemmas tagged `@[push_cast]`.
If the set of scalar types encountered is not totally ordered (in the sense that for all rings `R`,
`S` encountered, it holds that either `Algebra R S` or `Algebra S R`), then `match_scalars` fails.

Examples:
```
example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  match_scalars
  -- one goal: `⊢ a * 1 + b * 1 = (b + a) * 1`

example [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :
    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
  match_scalars
  -- two goals:
  -- `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom)
  -- `⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom)

example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
    -(2:R) • a • x = a • (-2:ℤ) • x := by
  match_scalars
  -- one goal: `⊢ -2 * (a * 1) = a * (-2 * 1)`
```
 -/
Mathlib.Tactic.Module.tacticMatch_scalars : Lean.ParserDescr
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.isFiniteMeasure : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.HasLaw X μ P → MeasureTheory.IsFiniteMeasure P
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {A B : Set X} {f : X → ENNReal},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      Measurable f →
        MeasurableSet A →
          MeasurableSet B → ∀ (x₀ : X), ∫⁻ (x : X) in A ∩ B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂π x₀
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
/-- Inversion sends an affine subspace passing through the center to itself.  -/
EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c : P} {R : ℝ} {p : AffineSubspace ℝ P},
  c ∈ p → Set.MapsTo (EuclideanGeometry.inversion c R) ↑p ↑p
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.stdBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.stdBasis K =
    (Pi.basisFun ℝ { w // w.IsReal }).prod
      ((Pi.basis fun x => Complex.basisOneI).reindex (Equiv.sigmaEquivProd { w // w.IsComplex } (Fin 2)))
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_neg : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → AddCommute (-a) (-b)
-- Mathlib.Logic.Unique
/-- There is a unique function on an empty domain.  -/
Pi.uniqueOfIsEmpty : {α : Sort u_1} → [IsEmpty α] → (β : α → Sort v) → Unique ((a : α) → β a)
-- Init.Data.Ord.Basic
Ordering.isGE_eq_false : ∀ {o : Ordering}, o.isGE = false ↔ o = Ordering.lt
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.forIn : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Algebra.Group.Action.Prod
Prod.isScalarTowerBoth : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst_1 : Mul P] [inst_2 : SMul M N] [inst_3 : SMul M P]
  [IsScalarTower M N N] [IsScalarTower M P P], IsScalarTower M (N × P) (N × P)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_iff_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {k : α}, k ∈ t ↔ t.contains k = true
-- Mathlib.Order.Hom.Lattice
InfHom.const_apply : ∀ (α : Type u_2) {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (b : β) (a : α), (InfHom.const α b) a = b
-- Batteries.Data.String.Lemmas
String.Pos.Raw.Valid.intro : ∀ {s : String} {p : String.Pos.Raw},
  (∃ cs cs', cs ++ cs' = s.toList ∧ p.byteIdx = String.utf8Len cs) → String.Pos.Raw.Valid s p
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.toModuleCat : {R : Type u} → [inst : CommRing R] → CoalgCat R → ModuleCat R
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.map_condition_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D)
  [G.PreservesZeroMorphisms] {Z : D} (h : G.obj c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map f)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Cofork.π c)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryFin1_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×1]→L[𝕜] G') (x : G),
  ((continuousMultilinearCurryFin1 𝕜 G G') f) x = f (Fin.snoc 0 x)