mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
_private.Mathlib.GroupTheory.SpecificGroups.Cyclic.0.card_pow_eq_one_eq_orderOf_aux : ∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | a ^ n = 1}.card ≤ n) → ∀ (a : α), {b | b ^ orderOf a = 1}.card = orderOf a
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel and collects results in the original order,
discarding state information.

Unlike `par`, this doesn't return state information from tasks.

The final MetaM state is restored to the initial state (before tasks ran).
 -/
Lean.Meta.MetaM.par' : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (List (Except Lean.Exception α))
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_top : ∀ {a b : ENNReal}, a < ⊤ → b < ⊤ → a * b < ⊤
-- Mathlib.GroupTheory.Exponent
Group.exponent_dvd_sub_iff_zpow_eq_zpow : ∀ {G : Type u} [inst : Group G] {n m : ℤ}, ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ),
  MvPolynomial.expand p = MvPolynomial.bind₁ fun i => MvPolynomial.X i ^ p
-- Init.Data.List.Control
List.idRun_findM? : ∀ {α : Type} (p : α → Id Bool) (as : List α), (List.findM? p as).run = List.find? (fun x => (p x).run) as
-- Mathlib.Algebra.Group.Center
Set.prod_centralizer_subset_centralizer_prod : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_2} [inst_1 : Mul N] (S : Set M) (T : Set N),
  S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer
-- Mathlib.Logic.ExistsUnique
/-- This invokes the two `Decidable` arguments $O(n)$ times.  -/
List.decidableBExistsUnique : {α : Type u_2} → [DecidableEq α] → (p : α → Prop) → [DecidablePred p] → (l : List α) → Decidable (∃! x, x ∈ l ∧ p x)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest multiplicative congruence relation containing a given binary
relation.  -/
conGen : {M : Type u_1} → [inst : Mul M] → (M → M → Prop) → Con M
-- Mathlib.LinearAlgebra.Complex.Module
realPart_mono : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a b : A}, a ≤ b → realPart a ≤ realPart b
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0),
  CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.opcyclesIsoRightHomology hg).hom =
    CategoryTheory.CategoryStruct.id S.rightHomology
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mul_def : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (f g : A →A[R] A), f * g = f.comp g
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.units_mem_lipschitzGroup : ∀ {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 : (CliffordAlgebra Q)ˣ}, ↑x ∈ pinGroup Q → x ∈ lipschitzGroup Q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k},
  (t.getThenInsertIfNew? k v ⋯).2 = (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl
-- Init.Data.String.Basic
String.Slice.Pos.utf8ByteSize_byte : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, (pos.byte h).utf8ByteSize ⋯ = (pos.get h).utf8Size
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Transport an `IsCokernel` across isomorphisms.  -/
CategoryTheory.Limits.IsCokernel.ofIso : {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'} →
              {s : CategoryTheory.Limits.CokernelCofork f} →
                CategoryTheory.Limits.IsColimit s →
                  (s' : CategoryTheory.Limits.CokernelCofork f') →
                    (eX : X ≅ X') →
                      (eY : Y ≅ Y') →
                        (e : s.pt ≅ s'.pt) →
                          CategoryTheory.CategoryStruct.comp eX.hom f' = CategoryTheory.CategoryStruct.comp f eY.hom →
                            CategoryTheory.CategoryStruct.comp eY.hom (CategoryTheory.Limits.Cofork.π s') =
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) e.hom →
                              CategoryTheory.Limits.IsColimit s'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        ∀ {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k' = true},
          m.contains k = false →
            List.Pairwise (fun a b => (a == b) = false) l →
              k ∈ l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey k' h' = k
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d.eq_2 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (i j : ι), HomologicalComplex.extend.d K (some i) (some j) = K.d i j
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictAntiOn.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, StrictAntiOn f s → StrictMonoOn (fun x => -f x) s
-- Mathlib.Algebra.Order.Ring.Defs
/-- This is not an instance, as it would loop with `NeZero.charZero_one`.  -/
AddMonoidWithOne.toCharZero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [NeZero 1]
  [AddLeftStrictMono R], CharZero R
-- Mathlib.Algebra.Ring.BooleanRing
instAddBool_mathlib : Add Bool
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instIsLeftCancelSMulSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul M' α]
  [IsLeftCancelSMul M' α], IsLeftCancelSMul (↥s) α
-- Mathlib.Data.Finset.Image
Finset.mem_image_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} (f : α → β) {a : α},
  a ∈ s → f a ∈ Finset.image f s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {k v : α} {w : k ∈ t}, t.get k w = v → k ∈ t
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Submodule 𝕜 E}, U ⟂ U ↔ U = ⊥
-- Init.Data.Int.DivMod.Lemmas
Int.divExact_eq_bdiv : ∀ {a : ℤ} {b : ℕ} (h : ↑b ∣ a), a.divExact (↑b) h = a.bdiv b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c =
    (CategoryTheory.Functor.functorialityCompPostcompose α).app c
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For vector spaces, dual annihilators carry direct sum decompositions
to direct sum decompositions.  -/
Subspace.isCompl_dualAnnihilator : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  {W W' : Subspace K V₁}, IsCompl W W' → IsCompl (Submodule.dualAnnihilator W) (Submodule.dualAnnihilator W')
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_le_of_fixedPoint : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {x y : α}, edist x y ≠ ⊤ → Function.IsFixedPt f y → edist x y ≤ edist x (f x) / (1 - ↑K)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_pos_of_dvd_prodPrimes : ∀ {s : BoundingSieve} {d : ℕ}, d ∣ s.prodPrimes → 0 < s.nu d
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft_zero_right : ∀ (a : ℕ), a.factorizationLCMLeft 0 = 1
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωSup_zip : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β),
  OmegaCompletePartialOrder.ωSup (c₀.zip c₁) = (OmegaCompletePartialOrder.ωSup c₀, OmegaCompletePartialOrder.ωSup c₁)
-- Init.Data.Nat.Control
/-- Executes a monadic action on all the numbers less than some bound, in decreasing order.

Example:
````lean example
#eval Nat.forRevM 5 fun i _ => IO.println i
````
````output
4
3
2
1
0
````
 -/
Nat.forRevM : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Unit) → m Unit
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_bot : ∀ {M : Type u_2} [inst : Add M], ⊥.op = ⊥
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, a ∉ m → m.getKey! a = default
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α),
  m.contains a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.contains ⟨m, h⟩ a else false
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_mono : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (b : J), CategoryTheory.IsSplitMono (CategoryTheory.Limits.biproduct.ι f b)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_and : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, ⌜φ₁⌝ ∧ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∧ φ₂⌝
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackFstFstIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  [inst_2 : CategoryTheory.Mono i₃],
  (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f' g') i₁))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f' g') i₂))
      ⋯
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_div : ∀ (a b : UInt32), a < 65536 → b < 65536 → (a / b).toUInt16 = a.toUInt16 / b.toUInt16
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_vadd_set_add_eq_add_vadd_set : ∀ {α : Type u_2} [inst : AddSemigroup α] (a : α) (s t : Set α), (AddOpposite.op a +ᵥ s) + t = s + (a +ᵥ t)
-- Init.Core
String.Pos.Raw.mk.injEq : ∀ (byteIdx byteIdx_1 : ℕ), ({ byteIdx := byteIdx } = { byteIdx := byteIdx_1 }) = (byteIdx = byteIdx_1)
-- Mathlib.RingTheory.LaurentSeries
RatFunc.instFaithfulSMulPolynomialLaurentSeries : ∀ {F : Type u} [inst : Field F], FaithfulSMul (Polynomial F) (LaurentSeries F)
-- Mathlib.Data.Multiset.Defs
Multiset.instSizeOf : {α : Type u_1} → [SizeOf α] → SizeOf (Multiset α)
-- Mathlib.Analysis.Convex.StrictConvexBetween
/-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
middle point belongs to the segment joining two other points.  -/
dist_add_dist_eq_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {a b c : P}, dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.formatterForKind : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_pos_iff : ∀ (n : Int16), 0 < n.toNatClampNeg ↔ 0 < n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.twoTorsionPolynomial.discr = 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_mul_two_eq_iff : ∀ {n : ℕ} (a : ZMod n), a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.diff_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.TreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_int8ToInt : ∀ (x : Int8), Int32.ofIntLE x.toInt ⋯ ⋯ = x.toInt32
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.mk.inj : ∀ {mvarId : Lean.MVarId} {fields : Array Lean.Expr} {subst : Lean.Meta.FVarSubst} {mvarId_1 : Lean.MVarId}
  {fields_1 : Array Lean.Expr} {subst_1 : Lean.Meta.FVarSubst},
  { mvarId := mvarId, fields := fields, subst := subst } =
      { mvarId := mvarId_1, fields := fields_1, subst := subst_1 } →
    mvarId = mvarId_1 ∧ fields = fields_1 ∧ subst = subst_1
-- Mathlib.Logic.Function.Basic
Function.factorsThrough_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) [Nonempty γ],
  Function.FactorsThrough g f ↔ ∃ e, g = e ∘ f
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.continuous_proj : ∀ {I : Type u} (J : I → Prop) [inst : (i : I) → Decidable (J i)], Continuous (Profinite.NobelingProof.Proj J)
-- Mathlib.Topology.Order.Monotone
IsClosed.isGreatest_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → s.Nonempty → BddAbove s → IsGreatest s (sSup s)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instEmptyCollection : {α : Type u} → {cmp : α → α → Ordering} → EmptyCollection (Std.ExtTreeSet α cmp)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mk : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N → G → N ⋊[φ] G
-- Mathlib.Topology.UniformSpace.Cauchy
instUniformSpaceProd.eq_1 : ∀ {α : Type ua} {β : Type ub} [u₁ : UniformSpace α] [u₂ : UniformSpace β],
  instUniformSpaceProd = UniformSpace.comap Prod.fst u₁ ⊓ UniformSpace.comap Prod.snd u₂
-- Mathlib.SetTheory.Cardinal.ENNReal
ENNReal.toReal_enatCard : ∀ (α : Type u_1), (↑(ENat.card α)).toReal = ↑(Nat.card α)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift_mk' : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] {φ : G →* M}
  (HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) ↑g = φ g
-- Lean.Compiler.LCNF.Types
/-- `isArrowClass? type` return `some ClsName` if the LCNF `type` is an instance of the class `ClsName`, or
if it is arrow producing an instance of the class `ClsName`.
 -/
Lean.Compiler.LCNF.isArrowClass? : Lean.Expr → Lean.CoreM (Option Lean.Name)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_affine_Ioo : ∀ {K : Type u_2} [inst : DivisionSemiring K] [inst_1 : PartialOrder K] [PosMulReflectLT K] [IsOrderedCancelAddMonoid K]
  [ExistsAddOfLE K] {a : K},
  0 < a → ∀ (b c d : K), (fun x => a * x + b) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)
-- Mathlib.RingTheory.Artinian.Module
/-- In a module over an Artinian ring, the submodule generated by finitely many vectors is
Artinian.  -/
isArtinian_span_of_finite : ∀ (R : Type u_1) {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinianRing R]
  {A : Set M}, A.Finite → IsArtinian R ↥(Submodule.span R A)
-- Mathlib.Order.Antichain
IsAntichain.empty : ∀ {α : Type u_1} {r : α → α → Prop}, IsAntichain r ∅
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normForwardRule.injEq : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.NormRule) (r₁_1 : Aesop.ForwardRule) (r₂_1 : Aesop.NormRule),
  (Aesop.BaseRuleSetMember.normForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.normForwardRule r₁_1 r₂_1) =
    (r₁ = r₁_1 ∧ r₂ = r₂_1)
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.below.inter : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → generatePiSystem S a → Prop} {s t : Set α}
  (h_s : generatePiSystem S s) (h_t : generatePiSystem S t) (h_nonempty : (s ∩ t).Nonempty),
  generatePiSystem.below h_s → motive s h_s → generatePiSystem.below h_t → motive t h_t → generatePiSystem.below ⋯
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.nondegenerate_iff_separatingLeft : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.Nondegenerate ↔ M.SeparatingLeft
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- An ordered variant of `primeSpectrumEquiv`.  -/
ValuationSubring.primeSpectrumOrderEquiv : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → (PrimeSpectrum ↥A)ᵒᵈ ≃o { S // A ≤ S }
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The identity diffeomorphism between a manifold with model `I` and the same manifold
with model `I.trans_diffeomorph e`.  -/
ContinuousLinearEquiv.toTransContinuousLinearEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_4} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      (M : Type u_9) →
                        [inst_6 : TopologicalSpace M] →
                          [inst_7 : ChartedSpace H M] →
                            {n : WithTop ℕ∞} → (e : E ≃L[𝕜] F) → Diffeomorph I (I.transContinuousLinearEquiv e) M M n
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.toContextExpr : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Interval.Finset.Basic
Finset.notMem_uIcc_of_gt : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}, a < c → b < c → c ∉ Finset.uIcc a b
-- Std.Internal.Parsec.ByteArray
/-- Skip a sequence of bytes equal to the given `ByteArray`.
 -/
Std.Internal.Parsec.ByteArray.skipBytes : ByteArray → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Analysis.Meromorphic.Order
/-- If the order of a meromorphic function is nonnegative, then this function converges
at this point. See also the iff version `tendsto_nhds_iff_meromorphicOrderAt_nonneg`.  -/
tendsto_nhds_of_meromorphicOrderAt_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → 0 ≤ meromorphicOrderAt f x → ∃ c, Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformAddGroup.cauchy_map_iff_tendsto_swapped : ∀ {ι : Type u_3} {G : Type u_4} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter ι)
  (f : ι → G), Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => f p.2 - f p.1) (𝓕 ×ˢ 𝓕) (nhds 0)
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), (a ::ₘ s).powerset = s.powerset + Multiset.map (Multiset.cons a) s.powerset
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃Functor_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) (H : C₂) {X Y : C₁}
  (f : X ⟶ Y), (((CategoryTheory.Functor.flip₁₃Functor.obj F).obj G).obj H).map f = ((F.map f).app H).app G
-- Mathlib.Order.Fin.Tuple
/-- `Π i : Fin 2, α i` is order equivalent to `α 0 × α 1`. See also `OrderIso.finTwoArrowEquiv`
for a non-dependent version.  -/
OrderIso.piFinTwoIso : (α : Fin 2 → Type u_2) → [inst : (i : Fin 2) → Preorder (α i)] → ((i : Fin 2) → α i) ≃o α 0 × α 1
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentEdit : Lean.ToJson Lean.Lsp.TextDocumentEdit
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ (X₂ ⊗ X₁) ⊗ X₃`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The inf of two `AddSubsemigroup`s is their intersection.  -/
AddSubsemigroup.instMin : {M : Type u_1} → [inst : Add M] → Min (AddSubsemigroup M)
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_zero_right : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime x 0 ↔ IsUnit x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.mulAssoc.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.mulAssoc = 1
-- Mathlib.Data.Complex.Basic
Complex.reProdIm_nonempty : ∀ {s t : Set ℝ}, (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommMonoid : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : CommMonoid M] → [ContinuousMul M] → CommMonoid (SeparationQuotient M)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_eq_pow_single : ∀ {α : Type u_2} {M : Type u_4} [inst : Monoid M] [inst_1 : DecidableEq α] {l : List α} (a : α) (f : α → M),
  (∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1) → (List.map f l).prod = f a ^ List.count a l