mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
/-- The normalised level 1 Eisenstein series of weight 6.  -/
ModularForm.E₆ : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 6
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.intCast k with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_9 k
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.cast : ∀ {s₁ s₂ : String} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂), p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂
-- Init.Data.BitVec.Lemmas
/-- For all bitvectors `x, y`, either `x` is signed less than `y`,
or is equal to `y`, or is signed greater than `y`.  -/
BitVec.slt_trichotomy : ∀ {w : ℕ} (x y : BitVec w), x.slt y = true ∨ x = y ∨ y.slt x = true
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G),
  CategoryTheory.NatTrans.unop (CategoryTheory.Functor.whiskerRight α H) =
    CategoryTheory.CategoryStruct.comp (G.unopComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.unop α) H.unop)
        (F.unopComp H).inv)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_self`. -/
Set.union_diff_self : ∀ {α : Type u_1} {s t : Set α}, s ∪ t \ s = s ∪ t
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
on the right or on the left at `b`, then the right (resp., left) derivative of
`u ↦ ∫ x in a..u, f x` at `b` equals `f b`.  -/
intervalIntegral.derivWithin_integral_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
      StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
        ContinuousWithinAt f t b →
          autoParam (UniqueDiffWithinAt ℝ s b) intervalIntegral.derivWithin_integral_right._auto_1 →
            derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = f b
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.mul_transvection_apply_same : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n]
  {m : Type u_4} (a : m) (c : R) (M : Matrix m n R), (M * Matrix.transvection i j c) a j = M a j + c * M a i
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_iff_eq_add_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.fullyFaithfulForgetToMonCat.eq_1 : CommMonCat.fullyFaithfulForgetToMonCat =
  { preimage := fun {X Y} f => CommMonCat.ofHom (MonCat.Hom.hom f),
    map_preimage := @CommMonCat.fullyFaithfulForgetToMonCat._proof_1,
    preimage_map := @CommMonCat.fullyFaithfulForgetToMonCat._proof_2 }
-- Mathlib.Algebra.Ring.CentroidHom
NonUnitalNonAssocSemiring.mem_center_iff : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α),
  a ∈ NonUnitalSubsemiring.center α ↔
    AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a ∧ AddMonoid.End.mulLeft a ∈ (CentroidHom.toEndRingHom α).rangeS
-- Mathlib.Data.TwoPointing
TwoPointing.prop_fst : TwoPointing.prop.toProd.1 = False
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Help typeclass inference to infer preservation of finite colimits for the forgetful functor.  -/
CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetFunObjFinite : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget FintypeCat)
-- Std.Data.DTreeMap.AdditionalOperations
Std.DTreeMap.instCoeTypeForall_2 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Order.BooleanAlgebra.Set
Set.inl_compl_union_inr_compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mk : {X : Type u_5} →
  {Y : Type u_6} → [inst : TopologicalSpace X] → (toFun : X → Y) → IsLocallyConstant toFun → LocallyConstant X Y
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mk : {X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toPartialEquiv : PartialEquiv X Y) →
          ContinuousOn (↑toPartialEquiv) toPartialEquiv.source →
            ContinuousOn toPartialEquiv.invFun toPartialEquiv.target → PartialHomeomorph X Y
-- Mathlib.CategoryTheory.Action.Monoidal
/-- A monoidal functor induces a monoidal functor between
the categories of `G`-actions within those categories.  -/
CategoryTheory.Functor.instMonoidalActionMapAction : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} W] →
            [inst_3 : CategoryTheory.MonoidalCategory V] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) → [F.Monoidal] → (F.mapAction G).Monoidal
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_anti : ∀ {α : Type u_1}, Antitone (@borel α)
-- Mathlib.Algebra.Order.Module.Defs
IsOrderedModule.of_smul_one_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
  [inst_4 : Preorder β] [inst_5 : MulOneClass β] [PosMulMono β] [MulPosMono β] [IsScalarTower α β β],
  (Monotone fun x => x • 1) → IsOrderedModule α β
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- Note : The proof of this statement is close to that
of `Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl`,
and while it would not be absolutely impossible to abstract both proofs,
the result would be slightly awkward because the
details of the results involved in the proof differ in annoying details.
And it would be used only twice.  -/
alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  s.Nontrivial → s.ncard < sᶜ.ncard → IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRioSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRioSlice._auto_1) →
      Std.Rio.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RioSlice α β)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinKernel.eq_1 : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.sinKernel a x = ⋯.lift a
-- Mathlib.RingTheory.Smooth.Kaehler
toAlgHom_comp_sectionOfRetractionKerToTensorAux : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P)
  (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥),
  Function.Surjective ⇑(algebraMap P S) →
    (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id R S
-- Init.Data.Ord.UInt
UInt64.instLawfulOrderOrd : Std.LawfulOrderOrd UInt64
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaObject_right_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.mkCommaObject F).right.map f = F.map (CategoryTheory.WithInitial.incl.map f)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Composition of bimodule object morphisms.  -/
Bimod.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} → {M N O : Bimod A B} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w).obj D =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj w D
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.toOption.eq_3 : ∀ {s : String.Slice} (needle : String.Slice) (table : Vector ℕ needle.utf8ByteSize)
  (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos needlePos : String.Pos.Raw)
  (hn : needlePos < needle.rawEndPos),
  String.Slice.Pattern.ForwardSliceSearcher.toOption✝
      (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn) =
    some (s.utf8ByteSize - stackPos.byteIdx, needlePos.byteIdx)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_sub_const : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ (c : ℝ), ProbabilityTheory.variance (fun ω => X ω - c) μ = ProbabilityTheory.variance X μ
-- Init.Data.List.Lemmas
List.head_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l₁ = []), (l₁ ++ l₂).head w = l₂.head ⋯
-- Mathlib.Order.Ideal
/-- The ideal is upward directed.  -/
Order.IsIdeal.Directed : ∀ {P : Type u_2} [inst : LE P] {I : Set P}, Order.IsIdeal I → DirectedOn (fun x1 x2 => x1 ≤ x2) I
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.π_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] (j : J),
  (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₃ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₃) j
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.isOrtho_comm : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} {x y : M}, Q.IsOrtho x y ↔ Q.IsOrtho y x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instFinite : ∀ {V : Type u} {G : SimpleGraph V} [Finite V], Finite G.Subgraph
-- Mathlib.GroupTheory.Index
Subgroup.finite_quotient_of_finiteIndex : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [H.FiniteIndex], Finite (G ⧸ H)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCocircuit.delete_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {K D : Set α}, M.IsCocircuit K → D ⊂ K → (M.delete D).IsCocircuit (K \ D)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b)
  (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.Limits.Pi.π g b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mul_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Mul γ] [inst_3 : ContinuousMul γ] (f g : α →ₘ[μ] γ), (f * g).toGerm = f.toGerm * g.toGerm
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.labelledStar.inj : ∀ {id id_1 : ℕ},
  Lean.Meta.RefinedDiscrTree.Key.labelledStar id = Lean.Meta.RefinedDiscrTree.Key.labelledStar id_1 → id = id_1
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.one_le : ∀ {p : ℕ}, Nat.Prime p → 1 ≤ p
-- Mathlib.Algebra.MvPolynomial.Coeff
MvPolynomial.coeff_linearCombination_X_pow : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] (a : σ →₀ R) (s : σ →₀ ℕ) (n : ℕ),
  MvPolynomial.coeff s ((Finsupp.linearCombination R MvPolynomial.X) a ^ n) =
    if (s.sum fun x m => m) = n then ↑s.multinomial * s.prod fun r m => a r ^ m else 0
-- Init.PropLemmas
Decidable.not_and_iff_not_or_not : ∀ {a b : Prop} [Decidable a], ¬(a ∧ b) ↔ ¬a ∨ ¬b
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `MDifferentiable` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMDifferentiable : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥
-- Mathlib.Order.Hom.Lattice
/-- `Subtype.val` as a `SupHom`.  -/
SupHom.subtypeVal : {β : Type u_3} →
  [inst : SemilatticeSup β] → {P : β → Prop} → (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) → SupHom { x // P x } β
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.of_add_of : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Add A] (f g : Matrix m n A),
  CStarMatrix.ofMatrix f + CStarMatrix.ofMatrix g = CStarMatrix.ofMatrix (f + g)
-- Lean.Expr
/-- Returns true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter,
or in the range if `considerRange == true`.
Additionally, if the bound variable appears in an implicit parameter,
it transitively looks for that implicit parameter.
 -/
Lean.Expr.hasLooseBVarInExplicitDomain : Lean.Expr → ℕ → Bool → Bool
-- Init.Data.List.Basic
List.eraseIdx_nil : ∀ {α : Type u} {i : ℕ}, [].eraseIdx i = []
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_right_square : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k) →
    CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) =
      CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_injective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ], Function.Injective DFunLike.coe
-- Mathlib.Tactic.Group
/-- `group` normalizes expressions in multiplicative groups that occur in the goal. `group` does not
assume commutativity, instead using only the group axioms without any information about which group
is manipulated. If the goal is an equality, and after normalization the two sides are equal, `group`
closes the goal.

For additive commutative groups, use the `abel` tactic instead.

* `group at l1 l2 ...` normalizes at the given locations.

Example:
```lean
example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
  group at h -- normalizes `h` which becomes `h : c = d`
  rw [h]     -- the goal is now `a*d*d⁻¹ = a`
  group      -- which then normalized and closed
```
 -/
Mathlib.Tactic.Group.group : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F],
  CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i →
    CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) → CategoryTheory.IsPushout f g h i
-- Std.Time.DateTime
/-- Subtract `Nanosecond.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subNanoseconds : Std.Time.DateTime → Std.Time.Nanosecond.Offset → Std.Time.DateTime
-- Init.Data.List.MinMaxOn
List.foldl.match_1.congr_eq_1 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (x : α) (x_1 : List β) (h_1 : (a : α) → motive a [])
  (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)) (a : α),
  x = a →
    x_1 = [] →
      (match x, x_1 with
        | a, [] => h_1 a
        | a, b :: l => h_2 a b l) ≍
        h_1 a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)}, (↑(t.insertMany l ⋯)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableEq.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSet (Set.diagonal α) → MeasurableEq α
-- Mathlib.Algebra.Order.Ring.Idempotent
instComplSubtypeProdAndEqHMulFstSndOfNatHAdd : {R : Type u_1} → [inst : CommMonoid R] → [inst_1 : AddCommMonoid R] → Compl { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.prod_mono_right : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (s : NonUnitalSubsemiring R), Monotone fun t => s.prod t
-- Mathlib.Topology.Category.Profinite.Basic
/-- The fully faithful embedding of `Profinite` in `CompHaus`.  -/
profiniteToCompHaus : CategoryTheory.Functor Profinite CompHaus
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.instArbitraryInt : Plausible.Arbitrary (Plausible.InjectiveFunction ℤ)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
iterateInduction.eq_2 : ∀ {X : ℕ → Type u_1} {a : ℕ} (x : (i : ↥(Finset.Iic a)) → X ↑i)
  (ind : (n : ℕ) → ((i : ↥(Finset.Iic n)) → X ↑i) → X (n + 1)) (k : ℕ),
  iterateInduction x ind k.succ = if h : k + 1 ≤ a then x ⟨k + 1, ⋯⟩ else ind k fun i => iterateInduction x ind ↑i
-- Mathlib.Algebra.Lie.Weights.Chain
LieAlgebra.isNilpotent_ad_of_mem_rootSpace : ∀ {L : Type u_2} [inst : LieRing L] {K : Type u_4} [inst_1 : Field K] [CharZero K] [inst_3 : LieAlgebra K L]
  (H : LieSubalgebra K L) [inst_4 : LieRing.IsNilpotent ↥H] [LieModule.IsTriangularizable K (↥H) L]
  [FiniteDimensional K L] {x : L} {χ : ↥H → K},
  χ ≠ 0 → x ∈ LieAlgebra.rootSpace H χ → IsNilpotent ((LieAlgebra.ad K L) x)
-- Mathlib.Data.Nat.Nth
Nat.isLeast_nth_of_infinite : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → ∀ (n : ℕ), IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseOp_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M),
  CliffordAlgebra.reverseOp ((CliffordAlgebra.ι Q) m) = MulOpposite.op ((CliffordAlgebra.ι Q) m)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is a cancel additive monoid if `β` is a cancel additive monoid.  -/
FunLike.addCancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddCancelMonoid β] →
                [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddCancelMonoid F
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instSetLike : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → SetLike (NonUnitalSubsemiring R) R
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L)
  {Z : HomotopyCategory C (ComplexShape.up ℤ)}
  (h :
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
        (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ)))
      h
-- Lean.Server.CodeActions.Basic
/-- Handler for `"codeAction/resolve"`.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
 -/
Lean.Server.handleCodeActionResolve : Lean.Lsp.CodeAction → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.CodeAction)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.eq_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {x : X} {y : Y}, x ∈ e.source → y ∈ e.target → (x = ↑e.symm y ↔ ↑e x = y)
-- Mathlib.Algebra.Polynomial.Sequence
/-- The `i`-th element in the sequence. Use `S i` instead, defined via `CoeFun`.  -/
Polynomial.Sequence.elems' : {R : Type u_1} → [inst : Semiring R] → Polynomial.Sequence R → ℕ → Polynomial R