mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.curryAlgEquiv_symm_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (m : M) (n : N) (a : A),
  (AddMonoidAlgebra.curryAlgEquiv R).symm (AddMonoidAlgebra.single m (AddMonoidAlgebra.single n a)) =
    AddMonoidAlgebra.single (m, n) a
-- Mathlib.RingTheory.Extension.Cotangent.Basis
Algebra.Presentation.naive.eq_1 : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x),
  Algebra.Presentation.naive s hs =
    { toGenerators := Algebra.Generators.naive s hs, relation := v, span_range_relation_eq_ker := ⋯ }
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.IsScalarTower.isAlgebraic : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra F K] [inst_5 : Algebra F L] [Algebra.IsAlgebraic F K] [IsScalarTower F K L] (f : Polynomial K)
  [Polynomial.IsSplittingField K L f], Algebra.IsAlgebraic F L
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (α : Type w) [Finite α],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CompHausLike P)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.instInhabitedPaths : (V : Type u₁) → [Inhabited V] → Inhabited (CategoryTheory.Paths V)
-- Init.Data.Nat.Coprime
Nat.not_coprime_of_dvd_of_dvd : ∀ {d m n : ℕ}, 1 < d → d ∣ m → d ∣ n → ¬m.Coprime n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {k : α},
  k ∈ t.toArray ↔ k ∈ t
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go : {pu : Lean.Compiler.LCNF.Purity} →
  Array (Lean.Compiler.LCNF.CodeDecl pu) → ℕ → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?_eq_minEntry?_reverse : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β}, l.maxEntry? = l.reverse.minEntry?
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstrs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.toLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsProper f],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lmapDomain_apply : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} (f : α → α') (l : α →₀ M), (Finsupp.lmapDomain M R f) l = Finsupp.mapDomain f l
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_zero_le_of_veblen_le : ∀ {o : Ordinal.{u}}, Ordinal.veblen o 0 ≤ o → Ordinal.gamma 0 ≤ o
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.epsilon_mul_omega : Hyperreal.epsilon * Hyperreal.omega = 1
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.eval.match_1.eq_1 : ∀ (motive : Lean.Data.AC.Expr → Sort u_1) (idx : ℕ) (h_1 : (idx : ℕ) → motive (Lean.Data.AC.Expr.var idx))
  (h_2 : (l r : Lean.Data.AC.Expr) → motive (l.op r)),
  (match Lean.Data.AC.Expr.var idx with
    | Lean.Data.AC.Expr.var idx => h_1 idx
    | l.op r => h_2 l r) =
    h_1 idx
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_algHom_iff : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_6} {B : Type u_7} [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ {x : A}, IsIntegral R (f x) ↔ IsIntegral R x
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToString.serializeRatHint : ℕ × Array ℕ → String
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
thickening_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 ≤ δ → ∀ (x : E), Metric.thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- In a star `R`-module (i.e., `star (r • m) = (star r) • m`) any star-closed subset which is also
closed under the scalar action by `R` is itself a star `R`-module.  -/
StarMemClass.instStarModule : ∀ {S : Type u_1} (R : Type u_2) {M : Type u_3} [inst : Star R] [inst_1 : Star M] [inst_2 : SMul R M] [StarModule R M]
  [inst_4 : SetLike S M] [inst_5 : SMulMemClass S R M] [inst_6 : StarMemClass S M] (s : S), StarModule R ↥s
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongr_apply : ∀ {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_6} {β₂ : ι₂ → Type u_7} [inst : (i₁ : ι₁) → UniformSpace (β₁ i₁)]
  [inst_1 : (i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) (a : (i : ι₁) → β₁ i)
  (i₂ : ι₂),
  (UniformEquiv.piCongr e F) a i₂ = (Equiv.piCongrLeft β₂ e) ((Equiv.piCongrRight fun i => (F i).toEquiv) a) i₂
-- Init.Data.List.Lemmas
List.foldr.eq_def : ∀ {α : Type u} {β : Type v} (f : α → β → β) (init : β) (x : List α),
  List.foldr f init x =
    match x with
    | [] => init
    | a :: l => f a (List.foldr f init l)
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_nat_cast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), (starRingEnd K) ↑n = ↑n
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.sub_one_mul_conj : ∀ {p q : ℝ}, p.HolderConjugate q → (p - 1) * q = p
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.fst B C).mapComp f g).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When the first map `S.f` is zero, this is the right homology data on `S` given by
the chosen `kernel S.g`  -/
CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [CategoryTheory.Limits.HasKernel S.g] → S.f = 0 → S.RightHomologyData
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_eq_zero_iff`. -/
Submodule.orthogonalProjection_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, K.orthogonalProjectionOnto v = 0 ↔ v ∈ Kᗮ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  (Std.DTreeMap.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Const.get t x ⋯)).isSome
-- Mathlib.Tactic.Use
/-- `use_discharger` is used by `use` to discharge side goals.

This is an extensible tactic using `macro_rules`. By default it can:
* rewrite a goal `∃ _ : p, q` into `p ∧ q` if `p` is in Prop;
* solve the goal `p ∧ q` by creating subgoals `p` and `q`;
* apply `rfl`;
* solve a goal by applying an assumption;
* solve the goal `True`.
 -/
Mathlib.Tactic.tacticUse_discharger : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrict_apply`. -/
MonoidHom.restrict_apply : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} {S : Type u_6} [inst_1 : MulOneClass N] [inst_2 : SetLike S M]
  [inst_3 : SubmonoidClass S M] (f : M →* N) (s : S) (x : ↥s), (f.domRestrict s) x = f ↑x
-- Mathlib.Probability.Distributions.Gamma
/-- The gamma pdf is positive for all positive reals  -/
ProbabilityTheory.gammaPDFReal_pos : ∀ {x a r : ℝ}, 0 < a → 0 < r → 0 < x → 0 < ProbabilityTheory.gammaPDFReal a r x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_minKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, cmp (Std.DTreeMap.Raw.Const.modify t k f).minKey! t.minKey! = Ordering.eq
-- Init.Data.Nat.Simproc
Nat.Simproc.add_sub_add_le : ∀ (a c : ℕ) {b d : ℕ}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
-- Mathlib.GroupTheory.GroupExtension.Defs
SemidirectProduct.toGroupExtension_inl : ∀ {N : Type u_1} {G : Type u_3} [inst : Group G] [inst_1 : Group N] (φ : G →* MulAut N),
  (SemidirectProduct.toGroupExtension φ).inl = SemidirectProduct.inl
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.mem_ball : ∀ {V : Type u_1} {G : SimpleGraph V} {c v : V} {r : ℕ∞}, v ∈ G.ball c r ↔ G.edist v c < r
-- Std.Internal.UV.System
/-- Represents the breakdown of CPU time usage in milliseconds.
 -/
Std.Internal.UV.System.CPUTimes : Type
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.eq.sizeOf_spec : sizeOf Mathlib.Ineq.WithStrictness.eq = 1
-- Mathlib.Tactic.Widget.Conv
/-- The conv widget.  -/
Mathlib.Tactic.Conv.SelectionPanel : ProofWidgets.Component SelectInsertParams
-- Mathlib.RingTheory.Spectrum.Prime.LTSeries
_private.Mathlib.RingTheory.Spectrum.Prime.LTSeries.0.term𝔪 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₁ : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₁ = X₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
Std.Tactic.BVDecide.BVPred.mkEq_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (pair : aig.BinaryRefVec w)
  (assign : α → Bool) (lhs rhs : BitVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ⟦assign, Std.Tactic.BVDecide.BVPred.mkEq aig pair⟧ = (lhs == rhs)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.compEvaluation_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (b : B) (X : A),
  (CategoryTheory.compEvaluation F b).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj b)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.asyncConsts : Lean.Environment → Lean.AsyncConsts✝
-- Mathlib.Topology.Constructions.SumProd
nhdsWithin_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y) (s : Set X)
  (t : Set Y), nhdsWithin (x, y) (s ×ˢ t) = nhdsWithin x s ×ˢ nhdsWithin y t
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- Given a Cauchy sequence `f` with nonzero limit, create a Cauchy sequence with values equal to
the inverses of the values of `f`.  -/
CauSeq.inv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [IsAbsoluteValue abv] → (f : CauSeq β abv) → ¬f.LimZero → CauSeq β abv
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instAddEquivClass : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N], AddEquivClass (M ≃+ N) M N
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_C : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ) (r : R), (LaurentPolynomial.C r).smeval x = r • 1
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to `TopCat` creates pullbacks if they exist.  -/
CompHausLike.instCreatesLimitTopCatWalkingCospanCospanCompHausLikeToTop : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) →
      (g : Y ⟶ B) →
        [CompHausLike.HasExplicitPullback f g] →
          CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.compHausLikeToTop P)
-- Mathlib.Order.MinMax
le_max_of_le_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → a ≤ max b c
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_inf : ∀ {M : Type u_1} [inst : AddZeroClass M] (p p' : AddSubmonoid M), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_inv_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.IsIso f] {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (CategoryTheory.CategoryStruct.comp (F.map f) h) = h
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofNat_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (n : ℕ) [inst_2 : n.AtLeastTwo],
  OfNat.ofNat n = MonoidAlgebra.single 1 (OfNat.ofNat n)
-- Init.Data.Format.Basic
Std.Format.instCoeString : Coe String Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The morphism `A ⟶ S.leftHomology` obtained from a morphism `k : A ⟶ S.X₂`
such that `k ≫ S.g = 0.`  -/
CategoryTheory.ShortComplex.liftLeftHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          (k : A ⟶ S.X₂) →
            CategoryTheory.CategoryStruct.comp k S.g = 0 → [inst_2 : S.HasLeftHomology] → A ⟶ S.leftHomology
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : AddMonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B],
  ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass =
    { coe := ContinuousAddMonoidHom.toContinuousAddMonoidHom }
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `get?_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.get?_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.filter f t) k = Option.filter (f k) (Std.DTreeMap.Const.get? t k)
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = f mn.1 * g mn.2
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- The natural map that reindexes a matrix's rows and columns with equivalent types,
`Matrix.reindex`, is a linear equivalence.  -/
Matrix.reindexLinearEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {m' : Type u_6} →
      {n' : Type u_7} →
        (R : Type u_11) →
          (A : Type u_12) →
            [inst : Semiring R] →
              [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → m ≃ m' → n ≃ n' → Matrix m n A ≃ₗ[R] Matrix m' n' A
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec'_one : ∀ {motive : ℕ → Sort u} (zero : motive 0)
  (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)),
  Nat.binaryRec' zero bit 1 = bit true 0 Nat.binaryRec'_one._proof_1 zero
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∃ G, CategoryTheory.IsDetector G) → CategoryTheory.HasDetector C
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_inv_of_isMulCocycle₁ : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulAction G M] {f : G → M},
  groupCohomology.IsMulCocycle₁ f → ∀ (g : G), g • f g⁻¹ = (f g)⁻¹
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- As a graded monoid, `⨂[R]^i M` has a `1 : ⨂[R]^0 M`.  -/
TensorPower.gOne : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → GradedMonoid.GOne fun i => TensorPower R i M
-- Mathlib.NumberTheory.Dioph
/-- The underlying function of a `Poly` is a polynomial  -/
Poly.isPoly : ∀ {α : Type u_1} (f : Poly α), IsPoly ⇑f
-- Init.Data.List.ToArray
List.findSomeRevM?_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → m (Option β))
  (l : List α), Array.findSomeRevM? f l.toArray = List.findSomeM? f l.reverse
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.mul_neg : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a b : α), a * -b = -(a * b)
-- Init.Data.List.Basic
List.prod_cons : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] {a : α} {l : List α}, (a :: l).prod = a * l.prod
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : Group N} {inst_1 : Group E} {inst_2 : Group G}
  {S : GroupExtension N E G} {E' : Type u_4} {inst_3 : Group E'} {S' : GroupExtension N E' G} {toMulEquiv : E ≃* E'}
  {inl_comm : ⇑toMulEquiv ∘ ⇑S.inl = ⇑S'.inl} {rightHom_comm : ⇑S'.rightHom ∘ ⇑toMulEquiv = ⇑S.rightHom}
  {toMulEquiv_1 : E ≃* E'} {inl_comm_1 : ⇑toMulEquiv_1 ∘ ⇑S.inl = ⇑S'.inl}
  {rightHom_comm_1 : ⇑S'.rightHom ∘ ⇑toMulEquiv_1 = ⇑S.rightHom},
  { toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
      { toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 } →
    toMulEquiv = toMulEquiv_1
-- Mathlib.GroupTheory.Divisible
RootableBy.root_zero : ∀ {A : Type u_1} {α : Type u_2} {inst : Monoid A} {inst_1 : Pow A α} {inst_2 : Zero α} [self : RootableBy A α] (a : A),
  RootableBy.root a 0 = 1
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.le_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M), s ≤ s.topologicalClosure
-- Mathlib.FieldTheory.Finite.Basic
mem_bot_iff_intCast : ∀ (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_4) [inst : DivisionRing K] [CharP K p] {x : K}, x ∈ ⊥ ↔ ∃ n, ↑n = x
-- Init.Grind.Interactive
/-- Executes the given tactic block to close the current goal.  -/
Lean.Parser.Tactic.Grind.nestedTacticCore : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.ofSimplex_map_of_epi : ∀ {X : SSet} {n m : ℕ} (f : { len := n } ⟶ { len := m }) [CategoryTheory.Epi f] (x : X.obj (Opposite.op { len := m })),
  SSet.Subcomplex.ofSimplex ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) x) = SSet.Subcomplex.ofSimplex x
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul_comm : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → CommSemiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (x y : PiTensorProduct R fun i => A i),
  (PiTensorProduct.mul x) y = (PiTensorProduct.mul y) x
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- A bijective linear map is a linear equivalence.  -/
LinearEquiv.ofBijective : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        (f : M →ₛₗ[σ₁₂] M₂) →
                          [inst_4 : RingHomInvPair σ₁₂ σ₂₁] →
                            [inst_5 : RingHomInvPair σ₂₁ σ₁₂] → Function.Bijective ⇑f → M ≃ₛₗ[σ₁₂] M₂
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_involutive : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Function.Involutive ⇑CliffordAlgebra.involute
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsUltrahomogeneous.amalgamation_age : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  L.IsUltrahomogeneous M → FirstOrder.Language.Amalgamation (L.age M)
-- Init.Data.BEq
instSymmEqBoolBeqTrueOfPartialEquivBEq : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α], Std.Symm fun x1 x2 => (x1 == x2) = true
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.forRevM.loop : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Unit) → (i : ℕ) → i ≤ n → m Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_cancel_var : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (c : ℤ)
  (x : Lean.Grind.CommRing.Var) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.cancel_var_cert c x p₁ p₂ = true →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p₂ = 0
-- Mathlib.Algebra.Ring.Int.Defs
Int.instCommSemiring : CommSemiring ℤ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.revSkipWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos},
  pos.toSlice.revSkipWhile pat = (pos.revSkipWhile pat).toSlice
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.core_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Bool
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.feature.quot : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (m₁ ∩ m₂) k fallback =
    if k ∈ m₂ then Std.ExtDHashMap.Const.getD m₁ k fallback else fallback
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mapDomain.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} (f f_1 : α → β) (e_f : f = f_1) [inst : AddCommMonoid M]
  [inst_1 : Filter.TendstoCofinite f] (v v_1 : α → M),
  v = v_1 →
    ∀ (a a_1 : β), a = a_1 → Filter.TendstoCofinite.mapDomain f v a = Filter.TendstoCofinite.mapDomain f_1 v_1 a_1
-- Std.Do.PredTrans
Std.Do.PredTrans.ext_iff : ∀ {ps : Std.Do.PostShape} {α : Type u} {t₁ t₂ : Std.Do.PredTrans ps α},
  t₁ = t₂ ↔ ∀ (Q : Std.Do.PostCond α ps), t₁.apply Q = t₂.apply Q
-- Mathlib.Topology.Separation.Hausdorff
lim_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {f : Filter X} {x : X} [f.NeBot], f ≤ nhds x → f.lim = x
-- Lean.Meta.LetToHave
/-- The transformed expression.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.expr : Lean.Meta.LetToHave.Result✝ → Lean.Expr
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} {b : β},
  Array.mapIdx f xs = Array.replicate xs.size b ↔ ∀ (i : ℕ) (h : i < xs.size), f i xs[i] = b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mkIso'_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom], (CategoryTheory.AddMon.mkIso' e).hom.hom = e.hom