mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The morphism between points of kernel forks induced by a morphism
in the category of arrows.  -/
CategoryTheory.Limits.KernelFork.mapOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {X' Y' : C} →
            {f' : X' ⟶ Y'} →
              (kf : CategoryTheory.Limits.KernelFork f) →
                {kf' : CategoryTheory.Limits.KernelFork f'} →
                  CategoryTheory.Limits.IsLimit kf' →
                    (CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') → (kf.pt ⟶ kf'.pt)
-- Mathlib.Analysis.Seminorm
Seminorm.continuousAt_zero' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.closedBall 0 r ∈ nhds 0 → ContinuousAt (⇑p) 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.nnnorm_exp_ofReal_mul_I : ∀ (x : ℝ), ‖Complex.exp (↑x * Complex.I)‖₊ = 1
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalGrindCore : Lean.Syntax →
  Lean.Grind.Config →
    Option Lean.Syntax →
      Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.grindParam ",") →
        Option (Lean.TSyntax `Lean.Parser.Tactic.Grind.grindSeq) →
          optParam (Option Lean.Meta.Grind.ExtensionStateArray) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.homMk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f B.hom = A.hom) CategoryTheory.MorphismProperty.Over.homMk._auto_1)
  (hf : autoParam (Q f) CategoryTheory.MorphismProperty.Over.homMk._auto_3),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Over.homMk f w hf) =
    CategoryTheory.Over.homMk f w
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory TopCat
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.isField_of_isDomain : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsDomain R], IsField R
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup
closure.  -/
AddMonoidHom.eqOn_closure : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddMonoid M] {f g : G →+ M} {s : Set G},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s)
-- Mathlib.MeasureTheory.Measure.AEDisjoint
Pairwise.aedisjoint : ∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f)
-- Lean.Message
Lean.instInhabitedMessageSeverity : Inhabited Lean.MessageSeverity
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImp.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 x_2 : L.BoundedFormula α x) →
          ((n : ℕ) →
              (φ : L.BoundedFormula α (n + 1)) →
                (ψ : L.BoundedFormula α n) →
                  motive n
                    ((φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp
                      FirstOrder.Language.BoundedFormula.falsum)
                    ψ) →
            ((n : ℕ) → (φ : L.BoundedFormula α (n + 1)) → (ψ : L.BoundedFormula α n) → motive n φ.all ψ) →
              ((x : ℕ) →
                  (φ ψ : L.BoundedFormula α x) →
                    (∀ (φ_1 : L.BoundedFormula α (x + 1)),
                        φ =
                            (φ_1.imp FirstOrder.Language.BoundedFormula.falsum).all.imp
                              FirstOrder.Language.BoundedFormula.falsum →
                          False) →
                      (∀ (φ_1 : L.BoundedFormula α (x + 1)), φ = φ_1.all → False) → motive x φ ψ) →
                motive x x_1 x_2
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toOrderIso_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (f : α ≃+*o β), ↑f = ↑f
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Directed.le_ciInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {f : ι → α} {a : α} [Nonempty ι],
  Directed (fun x1 x2 => x2 ≤ x1) f → (∀ (i : ι), a ≤ f i) → a ≤ ⨅ i, f i
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The coercion from the restricted product of additive monoids `A i` to the
(normal) product is an additive monoid homomorphism.  -/
RestrictedProduct.coeAddMonoidHom : {ι : Type u_1} →
  {R : ι → Type u_2} →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddMonoid (R i)] →
              [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)] →
                RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕 →+ (i : ι) → R i
-- Mathlib.Order.Filter.Map
Filter.map_comap_inl_sup_map_comap_inr : ∀ {α : Type u_1} {β : Type u_2} (l : Filter (α ⊕ β)),
  Filter.map Sum.inl (Filter.comap Sum.inl l) ⊔ Filter.map Sum.inr (Filter.comap Sum.inr l) = l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.ext_iff' : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (L₁' L₂' : LieSubalgebra R L), L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Limits.MulticospanIndex.multicospan.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C),
  I.multicospan =
    {
      obj := fun x =>
        match x with
        | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a
        | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b,
      map := fun {x y} f =>
        match x, y, f with
        | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) =>
          CategoryTheory.CategoryStruct.id
            (match x with
            | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a
            | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b)
        | .(CategoryTheory.Limits.WalkingMulticospan.left (J.fst b)),
          .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.fst b =>
          I.fst b
        | .(CategoryTheory.Limits.WalkingMulticospan.left (J.snd b)),
          .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.snd b =>
          I.snd b,
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.toAddSubmonoid_closure : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set M),
  Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.HasPullbacks.hasPullback : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {R : CategoryTheory.Presieve X} {Y : C} (f : Y ⟶ X)
  [self : R.HasPullbacks f] {Z : C} {h : Z ⟶ X}, R h → CategoryTheory.Limits.HasPullback h f
-- Mathlib.Data.Set.Countable
/-- If the codomain of a map is countable and the fibres are countable, the domain
is countable.  -/
Set.Countable.of_preimage_singleton : ∀ {α : Type u} {β : Type v} {f : α → β} [Countable β], (∀ (b : β), (f ⁻¹' {b}).Countable) → Countable α
-- Mathlib.Data.Subtype
Subtype.val.hcongr_3 : ∀ (α α' : Sort u),
  α = α' →
    ∀ (p : α → Prop) (p' : α' → Prop), p ≍ p' → ∀ (self : Subtype p) (self' : Subtype p'), self ≍ self' → ↑self ≍ ↑self'
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism : ∀ {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.Cone F} (hc : CategoryTheory.Limits.IsTerminal c)
  (s : CategoryTheory.Limits.Cone F), hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ioi_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], UpperSet.Ioi ⊤ = ⊤
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.nonneg_add_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  (∀ (x : α), 0 ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.le_sInf_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)},
  (∀ f ∈ s, (∀ j > i, f j = sInf s j) → e i ≤ f i) → e i ≤ sInf s i
-- Mathlib.Util.AddRelatedDecl
/-- A helper function for constructing a related declaration from an existing one.

This is currently used by the attributes `reassoc` and `elementwise`,
and has been factored out to avoid code duplication.
Feel free to add features as needed for other applications.

This helper:
* throws an error if a declaration named `tgt` already exists
  (in the current module or in an imported one),
* calls `addDeclarationRangesFromSyntax`, so jump-to-definition works,
* copies the `protected` status of the existing declaration, and
* supports copying attributes.

Arguments:
* `src : Name` is the existing declaration that we are modifying.
* `prefix_ : String` will be prepended and `suffix : String` will be appended to `src`
  to form the name of the new declaration.
* `ref : Syntax` is the syntax where the user requested the related declaration.
* `construct value levels : MetaM (Expr × List Name)`
  given an `Expr.const` referring to the original declaration, and its universe variables,
  should construct the value of the new declaration,
  along with the names of its universe variables.
* `attrs` is the attributes that should be applied to both the new and the original declaration,
  e.g. in the usage `@[reassoc (attr := simp)]`.
  We apply it to both declarations, to have the same behavior as `to_additive`, and to shorten some
  attribute commands. Note that `@[elementwise (attr := simp), reassoc (attr := simp)]` will try
  to apply `simp` twice to the current declaration, but that causes no issues.
* `docstringPrefix?` is prepended to the doc-string of `src` to form the doc-string of `tgt`.
  If it is `none`, only the doc-string of `src` is used.
* When `hoverInfo := true`, the generated constant will be shown as the hover information on `ref`.
  Warning: As a result, the original doc-string of `ref` will not be visible,
  and go-to-def on `ref` will not go to the definition of `ref`.
 -/
Mathlib.Tactic.addRelatedDecl : Lean.Name →
  Lean.Name →
    Lean.Syntax →
      Lean.TSyntax `Mathlib.Tactic.optAttrArg →
        (Lean.Expr → List Lean.Name → Lean.MetaM (Lean.Expr × List Lean.Name)) →
          optParam (Option String) none → optParam Bool false → Lean.MetaM Unit
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.χ_ne : ∀ {N : ℕ} [inst : NeZero N] (self : DirichletCharacter.BadChar✝ N), DirichletCharacter.BadChar.χ✝ self ≠ 1
-- Mathlib.Topology.EMetricSpace.Weak
instEDistWithBot : {α : Type u} → [EDist α] → EDist (WithBot α)
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.opOp_symm_apply : ∀ (M : Type u_3) [inst : Add M] (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.opOp M).symm a = AddOpposite.unop (AddOpposite.unop a)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.mk.sizeOf_spec : ∀ (toAssert : Array (Lean.Expr × Lean.Expr × ℕ)) (usedHyps : Std.HashSet Lean.FVarId),
  sizeOf { toAssert := toAssert, usedHyps := usedHyps } = 1 + sizeOf toAssert + sizeOf usedHyps
-- Mathlib.Algebra.Order.Group.PosPart
negPart_max : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α),
  (a ⊔ b)⁻ = a⁻ ⊓ b⁻
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.compl : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s ≤ᶠ[l] t → tᶜ ≤ᶠ[l] sᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.PiProd
/-- A product indexed by `I` is a binary product of the products indexed by a subset of `I` and its
complement.
 -/
CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit : {C : Type u_1} →
  {I : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      (X : I → C) →
        (P : I → Prop) →
          [inst_1 : CategoryTheory.Limits.HasProduct X] →
            [inst_2 : CategoryTheory.Limits.HasProduct fun i => X ↑i] →
              [inst_3 : CategoryTheory.Limits.HasProduct fun i => X ↑i] →
                [(i : I) → Decidable (P i)] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.binaryFanOfProp X P)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` version of `List.prod_map_pow` for `Real`.  -/
Real.list_prod_map_rpow : ∀ (l : List ℝ), (∀ x ∈ l, 0 ≤ x) → ∀ (r : ℝ), (List.map (fun x => x ^ r) l).prod = l.prod ^ r
-- Mathlib.Order.Atoms
/-- A simple partial ordered `BoundedOrder` induces a lattice.
This is not an instance to prevent loops  -/
IsSimpleOrder.lattice : {α : Type u_4} → [DecidableEq α] → [inst : PartialOrder α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → Lattice α
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv_coeff_one : ∀ {𝕜 : 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.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {d : n → α},
  Matrix.diagonal d = 1 ↔ d = 1
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.comp_hasStrictFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E),
  HasStrictDerivAt h₂ h₂' (f x) → HasStrictFDerivAt f f' x → HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Std.Data.String.ToInt
String.isSome_toInt? : ∀ {s : String}, s.toInt?.isSome = s.isInt
-- Mathlib.Algebra.Order.Floor.Div
Pi.floorDiv_apply : ∀ {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (π i)] [inst_3 : (i : ι) → PartialOrder (π i)]
  [inst_4 : (i : ι) → SMulZeroClass α (π i)] [inst_5 : (i : ι) → FloorDiv α (π i)] (f : (i : ι) → π i) (a : α) (i : ι),
  (f ⌊/⌋ a) i = f i ⌊/⌋ a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.toInt? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option (Lean.Expr × Lean.Expr))
-- Lean.Util.ParamMinimizer
/-- Marks that a solution has been found. That is, we found a bitmask where
`test` returned `true`
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.markFound : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Init.Data.String.Basic
String.Pos.cast_startPos : ∀ {s t : String} {hst : s = t}, s.startPos.cast hst = t.startPos
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This is the `norm_num` plug-in that evaluates Legendre symbols.  -/
Tactic.NormNum.evalLegendreSym : Mathlib.Meta.NormNum.NormNumExt
-- Init.Core
ULift.up.inj : ∀ {α : Type s} {down down_1 : α}, { down := down } = { down := down_1 } → down = down_1
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.mem_of_isFlat : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → ∀ {F : Set α}, M.IsFlat F → e ∈ F
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).tan = ‖x‖ / ‖y‖
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_tsum_eq_single : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → γ → α)
  (b : β) (c : γ),
  (∀ (b' : β), b' ≠ b → f b' c = 0) →
    (∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 0) → ∑' (b' : β) (c' : γ), f b' c' = f b c
-- Init.Data.List.Lemmas
List.and_any_distrib_right : ∀ {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool}, (l.any p && q) = l.any fun a => p a && q
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.star_eq_inv : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), star x = x⁻¹
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddSemigroupOfContinuousAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddSemigroup β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instAddSemigroupOfContinuousAdd = { toAdd := ContinuousMap.instAdd, add_assoc := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_sigma'`.

See also `Fintype.sum_sigma` for the sum over the whole type.  -/
Finset.sum_sigma : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
  (f : Sigma σ → β), ∑ x ∈ s.sigma t, f x = ∑ a ∈ s, ∑ s ∈ t a, f ⟨a, s⟩
-- Mathlib.Order.SetAccumulate
Set.accumulate_eq_biInter_lt : ∀ {β : Type u_2} {s : ℕ → Set β} {n : ℕ}, Set.accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basis_repr_symm_apply' : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : A) (i : ι),
  a • (Algebra.TensorProduct.basis A b) i = a ⊗ₜ[R] b i
-- Mathlib.Combinatorics.Enumerative.Schroder
/-- The recursive definition of the sequence of the large Schröder numbers :
`a (n + 1) = a n + ∑ i : Fin n.succ, a i * a (n - i)`  -/
Nat.largeSchroder : ℕ → ℕ
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.eq_3 : ∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), (p₁.num n₁).beq (p₂.num n₂) = (n₁ == n₂ && p₁.beq p₂)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A comonoid object in a functor category induces a functor to the category of comonoid objects.
 -/
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (A : CategoryTheory.Functor C D) →
            [CategoryTheory.ComonObj A] → CategoryTheory.Functor C (CategoryTheory.Comon D)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMap_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY)]
  {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πY) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right τ) h)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1))
  (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β),
  x = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
        h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) ≍
      h_2 size k v r
-- Mathlib.Data.Holor
/-- Right associator for `HolorIndex`  -/
HolorIndex.assocRight : {ds₁ ds₂ ds₃ : List ℕ} → HolorIndex (ds₁ ++ ds₂ ++ ds₃) → HolorIndex (ds₁ ++ (ds₂ ++ ds₃))
-- Mathlib.Analysis.Convex.Star
/-- The preimage of a star-convex set under an affine map is star-convex.  -/
StarConvex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : Set F},
  StarConvex 𝕜 (f x) s → StarConvex 𝕜 x (⇑f ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.instFaithfulFunctorTensoringLeft : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalCategory.tensoringLeft C).Faithful