mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Godel.GodelBetaFunction
Nat.coprimes_lt : ∀ {m : ℕ} (a : Fin m → ℕ) (i : Fin m), a i < Nat.coprimes✝ a i
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₂ : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_set_mk : ∀ {M : Type u_1} [inst : Add M] (s : Set M) (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s),
  ↑{ carrier := s, add_mem' := h_add } = s
-- Init.Data.Nat.Simproc
Nat.Simproc.add_eq_add_le : ∀ (a c : ℕ) {b d : ℕ}, b ≤ d → (a + b = c + d) = (a = c + (d - b))
-- Mathlib.RingTheory.Ideal.HasGoingUp
/-- Integral algebras satisfy the going up property.  -/
Algebra.HasGoingUp.of_isIntegral : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S], Algebra.HasGoingUp R S
-- Mathlib.Geometry.Polygon.Basic
Polygon.HasNondegenerateEdges.two_le : ∀ {P : Type u_3} {n : ℕ} [NeZero n] {poly : Polygon P n}, poly.HasNondegenerateEdges → 2 ≤ n
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.instMembershipFactorSet : {α : Type u_1} → [inst : CommMonoidWithZero α] → Membership (Associates α) (Associates.FactorSet α)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqCanonArgKey.beq : Lean.Meta.Grind.CanonArgKey → Lean.Meta.Grind.CanonArgKey → Bool
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_ne_top : ∀ {a : ENNReal} {n : ℕ}, a ≠ ⊤ → a ^ n ≠ ⊤
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_add_le : ∀ {a k : ℕ}, a ≠ 0 → a ≤ k → ∀ (n : ℕ), (k + n).primeCounting ≤ k.primeCounting + a.totient * (n / a + 1)
-- Init.Data.SInt.Lemmas
instCommutativeISizeHMul : Std.Commutative fun x1 x2 => x1 * x2
-- Init.Data.Vector.Range
Vector.range'_eq_mk_range' : ∀ {start size step : ℕ}, Vector.range' start size step = Vector.mk (Array.range' start size step) ⋯
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.hasCardinalLT_arrow_shrinkHoms_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w', v, u} C]
  (κ : Cardinal.{w}),
  HasCardinalLT (CategoryTheory.Arrow (CategoryTheory.ShrinkHoms.{u} C)) κ ↔ HasCardinalLT (CategoryTheory.Arrow C) κ
-- Mathlib.Order.WithBot
WithTop.map₂_coe_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithTop α) (b : β),
  WithTop.map₂ f a ↑b = WithTop.map (fun x => f x b) a
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.squarefree_of_dvd : ∀ {R : Type u_1} [inst : Monoid R] {x y : R}, x ∣ y → Squarefree y → Squarefree x
-- Lean.Parser.Command
Lean.Parser.Command.axiom.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- Extensionality theorem for `FixedDetMatrix` with respect to the underlying matrix, not
entrywise.  -/
FixedDetMatrices.ext' : ∀ (n : Type u_1) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type u_2) [inst_2 : CommRing R] {m : R}
  {A B : FixedDetMatrix n R m}, ↑A = ↑B → A = B
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.children : Lean.Widget.LazyTraceChildren → Array (Lean.Server.WithRpcRef Lean.MessageData)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_id : ∀ {R : CommRingCat}, CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R
-- Mathlib.Algebra.Group.Submonoid.Finite
AddSubmonoid.closure_pi : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → AddZeroClass (f i)] [Finite η] {s : (i : η) → Set (f i)},
  (∀ (i : η), 0 ∈ s i) →
    AddSubmonoid.closure (Set.univ.pi fun i => s i) = AddSubmonoid.pi Set.univ fun i => AddSubmonoid.closure (s i)
-- Lean.Parser.Command
Lean.Parser.Command.optDefDeriving : Lean.Parser.Parser
-- Mathlib.Data.List.AList
AList.lookup_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} (s : AList β),
  AList.lookup a (AList.insert a b s) = some b
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk.sizeOf_spec : ∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  [inst_2 : SizeOf V] [inst_3 : SizeOf W] (toPrefunctor : V ⥤q W)
  (map_id :
    autoParam
      (∀ (X : V), toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X))
      CategoryTheory.ReflPrefunctor.map_id._autoParam),
  sizeOf { toPrefunctor := toPrefunctor, map_id := map_id } = 1 + sizeOf toPrefunctor
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_apply_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {p : ι → Prop} [inst_1 : DecidablePred p]
  (f : Π₀ (i : ι), β i) {i : ι}, ¬p i → (DFinsupp.filter p f) i = 0
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.name : Lean.Meta.ElimAltInfo → Lean.Name
-- Mathlib.RingTheory.Ideal.Maps
Ideal.isMaximal_iff_of_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Bijective ⇑f → (⊥.IsMaximal ↔ ⊥.IsMaximal)
-- Std.Data.DTreeMap.Raw.Lemmas
_private.Std.Data.DTreeMap.Raw.Lemmas.0.Std.DTreeMap.Raw.ext : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t t' : Std.DTreeMap.Raw α β cmp}, t.inner = t'.inner → t = t'
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
`Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
AddMonoidHom.mulOp : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ)
-- Mathlib.Combinatorics.Matroid.Sum
/-- The sum of two matroids as a matroid on the sum type.  -/
Matroid.sum : {α : Type u} → {β : Type v} → Matroid α → Matroid β → Matroid (α ⊕ β)
-- Mathlib.Probability.ProductMeasure
measurePreserving_eval_infinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι),
  MeasureTheory.MeasurePreserving (Function.eval i) (MeasureTheory.Measure.infinitePi μ) (μ i)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conj_smul_eq_self_of_mem : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} {h : G}, h ∈ H → MulAut.conj h • H = H
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homEquiv_symm_naturality : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W W' : C}
  (f : (CategoryTheory.Functor.const J).obj W ⟶ F) (g : W' ⟶ W),
  h.homEquiv.symm (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map g) f) =
    CategoryTheory.CategoryStruct.comp g (h.homEquiv.symm f)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : NonUnitalSubalgebra R A) (h1 : 1 ∈ S), (S.toSubalgebra h1).toNonUnitalSubalgebra = S
-- Mathlib.Topology.Algebra.ConstMulAction
/-- **Alias** of the reverse direction of `smul_mem_nhds_smul_iff`. -/
smul_mem_nhds_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α}, t ∈ nhds a → g • t ∈ nhds (g • a)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_injective : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] (i : σ), Function.Injective ⇑(PowerSeries.toMvPowerSeries i)
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear. This lemma is an auxiliary version
assuming all spaces live in the same universe, to enable an induction. Use instead
`ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear` that removes this assumption.  -/
ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {Du Eu Fu Gu : Type u} [inst_1 : NormedAddCommGroup Du]
  [inst_2 : NormedSpace 𝕜 Du] [inst_3 : NormedAddCommGroup Eu] [inst_4 : NormedSpace 𝕜 Eu]
  [inst_5 : NormedAddCommGroup Fu] [inst_6 : NormedSpace 𝕜 Fu] [inst_7 : NormedAddCommGroup Gu]
  [inst_8 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du},
  ContDiffOn 𝕜 (↑n) f s →
    ContDiffOn 𝕜 (↑n) g s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
            ‖B‖ *
              ∑ i ∈ Finset.range (n + 1),
                ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitBackward_unitForward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : C), CategoryTheory.OverPresheafAux.unitBackward η X ∘ CategoryTheory.OverPresheafAux.unitForward η X = id
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Constant function as a `SimpleFunc`.  -/
MeasureTheory.SimpleFunc.const : (α : Type u_5) → {β : Type u_6} → [inst : MeasurableSpace α] → β → MeasureTheory.SimpleFunc α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → t.maxKey?.isSome = true
-- Mathlib.RingTheory.Ideal.Prime
Ideal.notMem_of_isUnit : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) [I.IsPrime] {x : α}, IsUnit x → x ∉ I
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is disjoint to `s`.  -/
SimpleGraph.isBipartiteWith_neighborFinset_disjoint : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)],
  G.IsBipartiteWith ↑s ↑t → v ∈ s → Disjoint (G.neighborFinset v) s
-- Mathlib.Order.Hom.CompleteLattice
infsInfHom_apply : ∀ {α : Type u_2} [inst : CompleteLattice α] (x : α × α), infsInfHom x = x.1 ⊓ x.2
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_smul_null : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α},
  μ s = 0 → ∀ (c : G), μ (c • s) = 0
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.instFunLikeAlternatingMapForallFinCarrier : {R : Type u} →
  [inst : CommRing R] → (M : ModuleCat R) → (N : ModuleCat R) → (n : ℕ) → FunLike (M.AlternatingMap N n) (Fin n → ↑M) ↑N
-- Mathlib.Topology.Category.Profinite.Extend
/-- If `c` and `G.mapCone c` are limit cones and the projection maps in `c` are epimorphic,
then `cone G c.pt` is a limit cone.
 -/
Profinite.Extend.isLimitCone : {I : Type u} →
  [inst : CategoryTheory.SmallCategory I] →
    [CategoryTheory.IsCofiltered I] →
      {F : CategoryTheory.Functor I FintypeCat} →
        (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
          {C : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} C] →
              (G : CategoryTheory.Functor Profinite C) →
                CategoryTheory.Limits.IsLimit c →
                  [∀ (i : I), CategoryTheory.Epi (c.π.app i)] →
                    CategoryTheory.Limits.IsLimit (G.mapCone c) →
                      CategoryTheory.Limits.IsLimit (Profinite.Extend.cone G c.pt)
-- Mathlib.Data.Finset.NAry
/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Finset.image₂ f`.  -/
Finset.image₂_right_identity : ∀ {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : γ → β → γ} {b : β},
  (∀ (a : γ), f a b = a) → ∀ (s : Finset γ), Finset.image₂ f s {b} = s
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  {H : J.OneHypercoverFamily} [self : H.IsGenerating] {X : C}, ∀ S ∈ J X, ∃ E, ∃ (_ : H E), E.sieve₀ ≤ S
-- Lean.Meta.WHNF
/-- Auxiliary method for unfolding a class projection. Recall that class fields are not marked with
`[reducible]`, but we want to reduce them when the transparency setting is `.instances`.
For example, given `a b : Nat`, the term `a ≤ b` is `LE.le Nat instLENat a b`.
Unfolding the class field `LE.le` gives `instLENat.1 a b`. This method goes further and
reduces the instance projection to return `Nat.le a b`.
 -/
Lean.Meta.unfoldProjInst? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Order.Fin.Tuple
/-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
values are retained. This is the `OrderIso` version of `Fin.castLE`.  -/
Fin.castLEOrderIso : {n m : ℕ} → n ≤ m → Fin n ≃o { i // ↑i < n }
-- Mathlib.Data.Rel.Separated
/-- Given a relation `R`, a set `s` is `R`-separated if its elements are pairwise `R`-unrelated from
each other.  -/
SetRel.IsSeparated : {X : Type u_1} → SetRel X X → Set X → Prop
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The quotient map to `α ⧸ G` is measure-preserving between the restriction of `volume` to a
fundamental domain in `α` and a related measure satisfying `QuotientMeasureEqMeasurePreimage`.  -/
MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} {𝓕 : Set α},
  MeasureTheory.IsFundamentalDomain G 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)))
      [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict 𝓕) μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon k m p =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 0
    else
      bif m == Lean.Grind.CommRing.Mon.unit then Lean.Grind.CommRing.Poly.mulConst k p
      else Lean.Grind.CommRing.Poly.mulMon.go k m p
-- Mathlib.Data.Set.Inclusion
Set.inclusion_mk : ∀ {α : Type u_1} {s t : Set α} {h : s ⊆ t} (a : α) (ha : a ∈ s), Set.inclusion h ⟨a, ha⟩ = ⟨a, ⋯⟩
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_injective_iff : ∀ {n : ℕ} {α : Type u_1} {x₀ : α} {x : Fin n → α},
  Function.Injective (Fin.cons x₀ x) ↔ x₀ ∉ Set.range x ∧ Function.Injective x
-- Mathlib.Data.List.Permutation
List.permutationsAux2_fst : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β),
  (List.permutationsAux2 t ts r ys f).1 = ys ++ ts
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsCancelMul α], IsCancelMul αᵒᵈ
-- Init.Data.UInt.Lemmas
UInt16.sub_right_inj : ∀ {a b : UInt16} (c : UInt16), c - a = c - b ↔ a = b
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_nhdsWithin : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) {s : Set X},
  x ∈ e.source → ((∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p y) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p (↑e x))
-- Init.PropLemmas
/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches.  -/
dite_not : ∀ {p : Prop} {α : Sort u_1} [hn : Decidable ¬p] [h : Decidable p] (x : ¬p → α) (y : ¬¬p → α),
  dite (¬p) x y = dite p (fun h => y ⋯) x
-- Mathlib.Data.List.Basic
List.head!_eq_head? : ∀ {α : Type u} [inst : Inhabited α] (l : List α), l.head! = l.head?.getD default
-- Mathlib.Data.Finset.Max
/-- **Alias** of `Finset.card_le_sdiff_of_interleaved`.

---

If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card (t \ s) + 1`.  -/
Finset.card_le_diff_of_interleaved : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α},
  (∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) → s.card ≤ (t \ s).card + 1
-- Mathlib.GroupTheory.Exponent
AddCommute.of_addOrderOf_dvd_two : ∀ {G : Type u} [inst : AddMonoid G] [IsCancelAdd G], (∀ (g : G), addOrderOf g ∣ 2) → ∀ (a b : G), AddCommute a b
-- Mathlib.Order.Antisymmetrization
wellFounded_antisymmetrization_iff : ∀ {α : Type u_1} [inst : Preorder α], WellFounded LT.lt ↔ WellFounded LT.lt
-- Init.Data.Vector.Lex
Vector.instReflLeOfIrreflLt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Star.TensorProduct
TensorProduct.instStarAddMonoid : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : Module R A] →
                [StarModule R A] →
                  [inst_6 : AddCommMonoid B] →
                    [inst_7 : StarAddMonoid B] →
                      [inst_8 : Module R B] → [StarModule R B] → StarAddMonoid (TensorProduct R A B)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.alternatingMapLinearEquiv_apply_ιMulti : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M [⋀^Fin n]→ₗ[R] N) (a : Fin n → M),
  (exteriorPower.alternatingMapLinearEquiv f) ((exteriorPower.ιMulti R n) a) = f a
-- Lean.Meta.Tactic.Grind.Action
/-- If the `goal` is already inconsistent, returns `.closed []`. Otherwise, executes
then not applicable continuation.
 -/
Lean.Meta.Grind.Action.done : Lean.Meta.Grind.Action
-- Mathlib.Topology.Instances.Irrational
eventually_residual_irrational : ∀ᶠ (x : ℝ) in residual ℝ, Irrational x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' ∈ t
-- Mathlib.Data.Finsupp.Single
Finsupp.uniqueEquiv_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) [inst_1 : Subsingleton α] (f : α →₀ M),
  (Finsupp.uniqueEquiv a) f = f a
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_associated : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α), Associated (normalize x) x
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.coe_sup : ∀ {E : Type u_3} [inst : AddGroup E] (p q : NonarchAddGroupNorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprInList.repr : Lean.Doc.Parser.InList → ℕ → Std.Format
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalNonAssocRingOfIsTopologicalRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocRing β] → [IsTopologicalRing β] → NonUnitalNonAssocRing C(α, β)
-- Mathlib.GroupTheory.CoprodI
/-- The `Word M` represented by a `NeWord M i j`  -/
Monoid.CoprodI.NeWord.toWord : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j : ι} → Monoid.CoprodI.NeWord M i j → Monoid.CoprodI.Word M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyPrepareParams : Lean.ToJson Lean.Lsp.CallHierarchyPrepareParams
-- Mathlib.LinearAlgebra.Isomorphisms
Submodule.quotientQuotientEquivQuotientAux_mk_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M)
  (h : S ≤ T) (x : M),
  (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk (Submodule.Quotient.mk x)) = Submodule.Quotient.mk x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorHom_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.Limits.pullback.map R.hom T.hom S.hom U.hom (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.Over.Hom.left g) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.edgeTransform_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x : C × D), (CategoryTheory.Join.edgeTransform C D).app x = CategoryTheory.Join.edge x.1 x.2
-- Lean.Meta.Sym.Arith.Types
/-- Result of classifying a type's algebraic structure.  -/
Lean.Meta.Sym.Arith.ClassifyResult : Type
-- Mathlib.Order.Nucleus
Nucleus.ext_iff : ∀ {X : Type u_1} [inst : SemilatticeInf X] {m n : Nucleus X}, m = n ↔ ∀ (a : X), m a = n a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ConditionallyCompleteLattice.toConditionallyCompletePartialOrder : {α : Type u_1} → [ConditionallyCompleteLattice α] → ConditionallyCompletePartialOrder α
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instPowUInt8UintOfNatNat : Lean.Grind.ToInt.Pow UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.IsPretransitive.of_isScalarTower : ∀ (M : Type u_5) {N : Type u_6} {α : Type u_7} [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : MulAction N α]
  [inst_3 : SMul M α] [IsScalarTower M N α] [MulAction.IsPretransitive M α], MulAction.IsPretransitive N α
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.sub_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a - b).toProd.2 = a.toProd.2 - b.toProd.2
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_iff_of_subsingleton : ∀ {R : Type u_1} [inst : Semiring R] [Subsingleton R] {p : Polynomial R} {n : ℕ}, p.IsMonicOfDegree n ↔ n = 0
-- Mathlib.Topology.EMetricSpace.Defs
Metric.closedEBall_mem_nhds : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → Metric.closedEBall x ε ∈ nhds x
-- Aesop.Tree.Traversal
Aesop.TreeRef.goal.sizeOf_spec : ∀ (gref : Aesop.GoalRef), sizeOf (Aesop.TreeRef.goal gref) = 1 + sizeOf gref
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxCat : Lean.Parser.Parser
-- Mathlib.GroupTheory.Coset.Basic
/-- Given an additive subgroup `s`,
the function that sends an additive subgroup `t` to the pair consisting of
its intersection with `s` and its image in the quotient `α ⧸ s`
is strictly monotone, even though it is not injective in general.  -/
QuotientAddGroup.strictMono_comap_prod_image : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α),
  StrictMono fun t => (AddSubgroup.comap s.subtype t, QuotientAddGroup.mk '' ↑t)
-- Mathlib.Data.List.Rotate
List.rotate_cons_succ : ∀ {α : Type u} (l : List α) (a : α) (n : ℕ), (a :: l).rotate (n + 1) = (l ++ [a]).rotate n
-- Mathlib.Order.WellFounded
/-- The minimal element of a trichotomous well-founded order is unique  -/
WellFounded.min_eq_of_forall_not_lt : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (wf : WellFounded r) {s : Set α} {m : α} (hms : m ∈ s),
  (∀ x ∈ s, ¬r x m) → wf.min s ⋯ = m
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_zero : ∀ (d : ℕ) (a : Fin 0 → ℕ), (Behrend.map d) a = 0