mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1InfRes_X₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).X₁ = groupCohomology (A.quotientToInvariants S) 1
-- ProofWidgets.Component.RefreshComponent
/-- Create a `RefreshToken` with an initial HTML tree.  -/
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.new : Thunk ProofWidgets.Html → BaseIO ProofWidgets.RefreshToken
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- Dense sets have small doubling.  -/
Finset.mulConst_le_inv_dens : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} [inst_2 : Fintype G],
  A.mulConst B ≤ A.dens⁻¹
-- Lean.Elab.PreDefinition.Structural.IndPred
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.replaceIndPredRecApps : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions →
    Array Lean.Expr → Lean.Meta.IndPredBelow.RecursionContext → Lean.Expr → Lean.Elab.Structural.IndPredM✝ Lean.Expr
-- Mathlib.Analysis.Complex.OpenMapping
Polynomial.isOpenQuotientMap_eval : ∀ (p : Polynomial ℂ), p.natDegree ≠ 0 → IsOpenQuotientMap fun x => Polynomial.eval x p
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg.sizeOf_spec : ∀ (a : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg a) = 1 + sizeOf a
-- Mathlib.Topology.ClusterPt
ClusterPt.of_nhds_le : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f : Filter X}, nhds x ≤ f → ClusterPt x f
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.inv_inv_add_inv : ∀ (p q r : ENNReal) [p.HolderTriple q r], (p⁻¹ + q⁻¹)⁻¹ = r
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddCommMonoid` across an `Equiv`  -/
Equiv.addCommMonoid : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddCommMonoid β] → AddCommMonoid α
-- Init.Data.List.Nat.Modify
List.modify_modify_ne : ∀ {α : Type u_1} (f g : α → α) {i j : ℕ} (l : List α), i ≠ j → (l.modify i f).modify j g = (l.modify j g).modify i f
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff : ∀ {ι : 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 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι]
  (N_1 : LieSubmodule R (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → R)) {x : ↥b.support ⊕ ι → R},
  x ∈ RootPairing.GeckConstruction.ωConjLieSubmodule N_1 ↔ (RootPairing.GeckConstruction.ω b).mulVec x ∈ N_1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.smulNatTrans_apply_app : ∀ (R : Type u) [inst : Ring R] (r : R) (M : ModuleCat R), ((ModuleCat.smulNatTrans R) r).app M = M.smul r
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.ecard_lt_ecard : ∀ {α : Type u_1} {s t : Set α}, s.Finite → s ⊂ t → ENat.card ↑s < ENat.card ↑t
-- Mathlib.RingTheory.Valuation.Basic
Valuation.coe_ofClass : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  ⇑(MonoidWithZeroHom.ofClass v) = ⇑v
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_degree_eq : ∀ {σ : Type u_1} [Finite σ] (n : ℕ), {f | Finsupp.degree f = n}.Finite
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.map_bernoulliMeasure' : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] [inst_1 : MeasurableSpace Y] (x y : X) {f : X → Y},
  Measurable f →
    ∀ (p : ↑unitInterval),
      MeasureTheory.Measure.map f (ProbabilityTheory.bernoulliMeasure x y p) =
        ProbabilityTheory.bernoulliMeasure (f x) (f y) p
-- Init.Data.UInt.Lemmas
UInt32.add_comm : ∀ (a b : UInt32), a + b = b + a
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X_i)_{i \in \iota}$ are jointly Gaussian and uncorrelated, then they are independent.  -/
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_inner : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {E : ι → Type u_3}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → MeasurableSpace (E i)]
  [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [inst_5 : (i : ι) → InnerProductSpace ℝ (E i)] {X : (i : ι) → Ω → E i},
  ProbabilityTheory.HasGaussianLaw (fun ω i => X i ω) P →
    (∀ (i j : ι),
        i ≠ j →
          ∀ (x : E i) (y : E j),
            ProbabilityTheory.covariance (fun ω => inner ℝ x (X i ω)) (fun ω => inner ℝ y (X j ω)) P = 0) →
      ProbabilityTheory.iIndepFun X P
-- Mathlib.Data.Num.Bitwise
/-- `n.oneBits 0` is the list of indices of active bits in the binary representation of `n`.  -/
PosNum.oneBits : PosNum → ℕ → List ℕ
-- Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
CategoryTheory.Injective.instHasLiftingPropertyOfMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B I : C} (i : A ⟶ B) [CategoryTheory.Mono i]
  [CategoryTheory.Injective I] [inst_3 : CategoryTheory.Limits.HasZeroObject C] (p : I ⟶ 0),
  CategoryTheory.HasLiftingProperty i p
-- Std.Data.ExtDTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDTreeMap.getKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option α
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cones` is representable, then the cone corresponding to the identity morphism on
the representing object is a limit cone.
 -/
CategoryTheory.Limits.IsLimit.ofRepresentableBy : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} →
            (h : F.cones.RepresentableBy X) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.mk.inj : ∀ {α : Type u_1} {before : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α} {val : α}
  {node : Batteries.BinomialHeap.Imp.HeapNode α} {next : Batteries.BinomialHeap.Imp.Heap α}
  {before_1 : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α} {val_1 : α}
  {node_1 : Batteries.BinomialHeap.Imp.HeapNode α} {next_1 : Batteries.BinomialHeap.Imp.Heap α},
  { before := before, val := val, node := node, next := next } =
      { before := before_1, val := val_1, node := node_1, next := next_1 } →
    before = before_1 ∧ val = val_1 ∧ node = node_1 ∧ next = next_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.negThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.Algebra.Group.Prod
/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `N` to `M × N`.  -/
MonoidHom.inr : (M : Type u_3) → (N : Type u_4) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → N →* M × N
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubAddAction.ofStabilizer.isPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {a b : α},
  AddAction.IsPretransitive ↥(AddAction.stabilizer G a) ↥(SubAddAction.ofStabilizer G a) ↔
    AddAction.IsPretransitive ↥(AddAction.stabilizer G b) ↥(SubAddAction.ofStabilizer G b)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The middle left map in the forward hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenIsoSpec.congr_simp : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m m_1 : ℕ} (e_m : m = m_1) (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm = AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f ⋯ ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_pow : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {g : α → γ},
  Measurable g → ∀ (c : β), Measurable fun x => c ^ g x
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_smul_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ), Metric.closedBall 0 r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
/-- A continuous map between two normed affine spaces is an affine map provided that
it sends midpoints to midpoints.  -/
AffineMap.ofMapMidpoint : {V : Type u_1} →
  {P : Type u_2} →
    {W : Type u_3} →
      {Q : Type u_4} →
        [inst : SeminormedAddCommGroup V] →
          [inst_1 : PseudoMetricSpace P] →
            [inst_2 : NormedAddTorsor V P] →
              [inst_3 : NormedAddCommGroup W] →
                [inst_4 : MetricSpace Q] →
                  [inst_5 : NormedAddTorsor W Q] →
                    [inst_6 : NormedSpace ℝ V] →
                      [inst_7 : NormedSpace ℝ W] →
                        (f : P → Q) →
                          (∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)) → Continuous f → P →ᵃ[ℝ] Q
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.eq_set_map_one_map_mul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Semiring A]
  [inst_7 : Algebra 𝕜 A] [Nontrivial 𝕜],
  WeakDual.characterSpace 𝕜 A = {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}
-- Mathlib.Order.Circular.ZMod
Fin.sbtw_iff : ∀ {n : ℕ} {a b c : Fin n}, sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- `Finset.noncommProd` is “injective” in `f` if `f` maps into independent subgroups.  This
generalizes (one direction of) `Subgroup.disjoint_iff_mul_eq_one`.  -/
Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} (s : Finset ι) (f : ι → G)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (K : ι → Subgroup G),
  iSupIndep K → (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
-- Aesop.RuleSet
/-- The names of all rules in `forwardRules`.  -/
Aesop.BaseRuleSet.forwardRuleNames : Aesop.BaseRuleSet → Lean.PHashSet Aesop.RuleName
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.familyOfBFamily'.congr_simp : ∀ {α : Type u_1} {ι : Type u} (r r_1 : ι → ι → Prop) (e_r : r = r_1) [inst : IsWellOrder ι r] {o : Ordinal.{u}}
  (ho : Ordinal.type r = o) (f f_1 : (a : Ordinal.{u}) → a < o → α),
  f = f_1 → ∀ (a a_1 : ι), a = a_1 → Ordinal.familyOfBFamily' r ho f a = Ordinal.familyOfBFamily' r_1 ⋯ f_1 a_1
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredOrEmptyForall : ∀ {α : Type w} {I : α → Type u₁} [inst : (i : α) → CategoryTheory.Category.{v₁, u₁} (I i)]
  [∀ (i : α), CategoryTheory.IsFilteredOrEmpty (I i)], CategoryTheory.IsFilteredOrEmpty ((i : α) → I i)
-- Mathlib.MeasureTheory.Integral.Prod
/-- Reversed version of **Fubini's Theorem** (symmetric version).  -/
MeasureTheory.integral_integral_symm : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : α → β → E},
  MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
    ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : β × α), f z.2 z.1 ∂ν.prod μ
-- Mathlib.Analysis.Seminorm
Seminorm.exists_apply_eq_finset_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) {s : Finset ι}, s.Nonempty → ∀ (x : E), ∃ i ∈ s, (s.sup p) x = (p i) x
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A map `incl(X) ⟶ Y` is specified by an element of `Y`'s indexing set, and then a morphism
`X ⟶ Y.obj i` in the original category.  -/
CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {Y : CategoryTheory.Limits.FormalCoproduct C} →
        (i : Y.I) → (X ⟶ Y.obj i) → ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_eq_affineCombination : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.incenter = (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights ∅)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {f : (a : α) → β a → Bool} {k : α},
  (Std.DHashMap.filter f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)).get!
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `Fin n` into `Fin (n + 1)` with a hole around `last n` embeds by `castSucc`.  -/
Fin.succAbove_last : ∀ {n : ℕ}, (Fin.last n).succAbove = Fin.castSucc
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Consider using `congr($H x)` instead.  -/
GradedAlgHom.congr_fun : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ}, f₁ = f₂ → ∀ (x : A), f₁ x = f₂ x
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.toStringAux : {α : Type} → Lean.Data.Trie α → List Std.Format
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_subset_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ -t ↔ s ⊆ t
-- Mathlib.Data.Nat.Dist
Nat.dist_comm : ∀ (n m : ℕ), n.dist m = m.dist n
-- Mathlib.Analysis.Real.Cardinality
Cardinal.summable_cantor_function : ∀ {c : ℝ} (f : ℕ → Bool), 0 ≤ c → c < 1 → Summable (Cardinal.cantorFunctionAux c f)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- All sets of the family have nonempty interior.  -/
VitaliFamily.nonempty_interior : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (x : X), ∀ s ∈ self.setsAt x, (interior s).Nonempty
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
      {P : CategoryTheory.ObjectProperty C} → HomotopicalAlgebra.CategoryWithWeakEquivalences P.FullSubcategory
-- Mathlib.Order.Filter.Basic
Filter.sup_join : ∀ {α : Type u} {f₁ f₂ : Filter (Filter α)}, f₁.join ⊔ f₂.join = (f₁ ⊔ f₂).join
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.MonoidalLinear.mk : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C],
  autoParam
      (∀ (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z),
        CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (r • f) =
          r • CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      CategoryTheory.MonoidalLinear.whiskerLeft_smul._autoParam →
    autoParam
        (∀ (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C),
          CategoryTheory.MonoidalCategoryStruct.whiskerRight (r • f) X =
            r • CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
        CategoryTheory.MonoidalLinear.smul_whiskerRight._autoParam →
      CategoryTheory.MonoidalLinear R C
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalizer_eq_top_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, AddSubgroup.normalizer ↑H = ⊤ ↔ H.Normal
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.natDegree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] [Nontrivial R] (p : Polynomial.MonicDegreeEq R n), (↑p).natDegree = n
-- Mathlib.Data.Multiset.Antidiagonal
/-- A pair `(t₁, t₂)` of multisets is contained in `antidiagonal s`
if and only if `t₁ + t₂ = s`.  -/
Multiset.mem_antidiagonal : ∀ {α : Type u_1} {s : Multiset α} {x : Multiset α × Multiset α}, x ∈ s.antidiagonal ↔ x.1 + x.2 = s
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.get.match_1.eq_1 : ∀ {α : Type u_1} {δ : Type u_2} [inst : Ord α] (k : α)
  (motive : (t : Std.DTreeMap.Internal.Impl α fun x => δ) → Std.DTreeMap.Internal.Impl.contains k t = true → Sort u_3)
  (size : ℕ) (k' : α) (v' : δ) (l r : Std.DTreeMap.Internal.Impl α fun x => δ)
  (hlk : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true)
  (h_1 :
    (size : ℕ) →
      (k' : α) →
        (v' : δ) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => δ) →
            (hlk : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) hlk),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk => h_1 size k' v' l r hlk) =
    h_1 size k' v' l r hlk
-- Init.Data.SInt.Lemmas
ISize.neg_nonpos_iff : ∀ (n : ISize), -n ≤ 0 ↔ n = ISize.minValue ∨ 0 ≤ n
-- Mathlib.Data.Set.Lattice
Set.pi_iUnion_eq_iInter_pi : ∀ {α : Type u_1} {π : α → Type u_12} {α' : Type u_13} (s : α' → Set α) (t : (a : α) → Set (π a)),
  (⋃ i, s i).pi t = ⋂ i, (s i).pi t
-- Mathlib.Order.Category.CompleteLat
CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier : CategoryTheory.ConcreteCategory CompleteLat fun x1 x2 => CompleteLatticeHom ↑x1 ↑x2
-- Lean.Util.SCC
Lean.SCC.State.data : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SCC.State α → Std.HashMap α Lean.SCC.Data
-- Batteries.Tactic.HelpCmd
/-- The command `#help conv` shows all tactics that have been defined in the current environment.
See `#help cat` for more information.
 -/
Batteries.Tactic.«command#help_Conv+____» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_neg : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ‖-a‖₊ = ‖a‖₊
-- Qq.Macro
Qq.withProcessPostponed : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT Lean.MetaM m] → m α → m α
-- Init.Tactics
/-- Syntax for adding or removing a term, or `*`, in `solve_by_elim`.  -/
Lean.Parser.Tactic.SolveByElim.arg : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.MonoidalCategory.tensoringRight_μ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensoringRight C) X Y).app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Odd.eq_1 : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m), ψ.Odd = (ψ (-1) = -1)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instVAdd : {ι : Type u_1} → {α : Type u_2} → {M : ι → Type u_5} → [(i : ι) → VAdd α (M i)] → VAdd α ((i : ι) → M i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} [inst_2 : Inhabited α] {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getKey! a = default
-- Mathlib.NumberTheory.ModularForms.Discriminant
ModularForm.exp_isBigO_discriminant : (fun τ => Real.exp (-2 * Real.pi * τ.im)) =O[UpperHalfPlane.atImInfty] ModularForm.discriminant
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorphOfImageEq_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t), (e.toOpenPartialHomeomorphOfImageEq s hs t h).target = t
-- Init.Internal.Order.Tactic
/-- `monotonicity` performs one compositional step solving `monotone` goals,
using lemma tagged with `@[partial_fixpoint_monotone]`.

This tactic is mostly used internally by lean in `partial_fixpoint` definitions, but
can be useful on its own for debugging or when proving new `@[partial_fixpoint_monotone]` lemmas.
 -/
Lean.Order.monotonicity : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_one_iff_of_pos : ∀ {x y : ℝ}, 0 < x → (x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂),
  (s.map f.toAffineMap ⋯).excenterWeights = s.excenterWeights
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.mkWhitespaceDiff : String → String → Array (Lean.Diff.Action × String)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.integral ↑f = MeasureTheory.L1.SimpleFunc.integral f
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensor_β : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C) (U : C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).snd.β U =
    CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst U ≪≫
      CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫
        (CategoryTheory.MonoidalCategoryStruct.associator X.fst U Y.fst).symm ≪≫
          CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫
            CategoryTheory.MonoidalCategoryStruct.associator U X.fst Y.fst
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instMax.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G],
  OpenAddSubgroup.instMax = { max := fun U V => { toAddSubgroup := ↑U ⊔ ↑V, isOpen' := ⋯ } }
-- Lean.Message
Lean.MessageData.nest.inj : ∀ {a : ℕ} {a_1 : Lean.MessageData} {a_2 : ℕ} {a_3 : Lean.MessageData},
  Lean.MessageData.nest a a_1 = Lean.MessageData.nest a_2 a_3 → a = a_2 ∧ a_1 = a_3