mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Action
/-- Every Set `X` that has a `G`-action on it can be made into a `G`-rep by using `X →₀ k` as
the base module and `G`-action on it is induced by the `G`-action on `X`.  -/
Representation.linearize : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] → [inst_1 : Semiring k] → (X : Action (Type w) G) → Representation k G (MonoidAlgebra k X.V)
-- Init.Data.UInt.Basic
instDivUInt16 : Div UInt16
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_mul_zeta : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : NonAssocSemiring 𝕜] [inst_1 : Preorder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableLE α] (a b : α), (IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.zeta 𝕜) a b = ↑(Finset.Icc a b).card
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : Monoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : Monoid G'] (toMonoidHom : G →* G')
  (contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom).toFun) (toMonoidHom_1 : G →* G')
  (contMDiff_toFun_1 : ContMDiff I I' n (↑toMonoidHom_1).toFun),
  ({ toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun } =
      { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C (Type w)}
  {obj : (U : C) → Set (F.obj U)}
  {map : ∀ {U V : C} (i : U ⟶ V), obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj V}
  {obj_1 : (U : C) → Set (F.obj U)}
  {map_1 : ∀ {U V : C} (i : U ⟶ V), obj_1 U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj_1 V},
  { obj := obj, map := map } = { obj := obj_1, map := map_1 } → obj = obj_1
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_sdiff_inter : ∀ {α : Type u_1} {s t : Set α}, Disjoint (s \ t) (s ∩ t)
-- Init.Data.ByteArray.Basic
/-- The array the iterator is for.  -/
ByteArray.Iterator.array : ByteArray.Iterator → ByteArray
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_subset_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α} {m n : ℕ},
  s ⊆ t → 0 ∈ t → m ≤ n → m • s ⊆ n • t
-- Lean.Elab.Command
/-- Follow-up elaboration snapshots, one per command if `newStx` is a sequence of commands.
 -/
Lean.Elab.Command.MacroExpandedSnapshot.next : Lean.Elab.Command.MacroExpandedSnapshot → Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.ParenthesizerM.orElse : {α : Type} →
  Lean.PrettyPrinter.ParenthesizerM α →
    (Unit → Lean.PrettyPrinter.ParenthesizerM α) → Lean.PrettyPrinter.ParenthesizerM α
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.eq_1 : ∀ {α : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_4}
  [inst_3 : Ring β] (abv : β → α) (f : ℕ → β), IsCauSeq abv f = ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - f i) < ε
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- If `x` is a Liouville number, then for any `n`, for infinitely many denominators `b` there
exists a numerator `a` such that `x ≠ a / b` and `|x - a / b| < 1 / b ^ n`.  -/
Liouville.frequently_exists_num : ∀ {x : ℝ}, Liouville x → ∀ (n : ℕ), ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_eq_zero_of_le_right : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, K ≤ L → H.relIndex K = 0 → H.relIndex L = 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A morphism in `Comma (Functor.const C) (𝟭 (C ⥤ D))` gives a morphism between the associated
functors `WithInitial C ⥤ D`.  -/
CategoryTheory.WithInitial.ofCommaMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {c c' :
            CategoryTheory.Comma (CategoryTheory.Functor.const C)
              (CategoryTheory.Functor.id (CategoryTheory.Functor C D))} →
          (c ⟶ c') → (CategoryTheory.WithInitial.ofCommaObject c ⟶ CategoryTheory.WithInitial.ofCommaObject c')
-- Mathlib.Algebra.Quaternion
Quaternion.re_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] (a : Quaternion R) [inst_1 : SMul S R] (s : S),
  (s • a).re = s • a.re
-- Mathlib.GroupTheory.Complement
/-- A left transversal can be viewed as a function mapping each element of the group
to the chosen representative from that left coset.  -/
Subgroup.IsComplement.toLeftFun : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → {S : Set G} → Subgroup.IsComplement S ↑H → G → ↑S
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.reverseAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match [], r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_1 r
-- Mathlib.Order.WellFounded
instWellFoundedGTULift : ∀ {α : Type u_1} [inst : LT α] [h : WellFoundedGT α], WellFoundedGT (ULift.{u_4, u_1} α)
-- Mathlib.Analysis.Asymptotics.TVS
/-- Eta-expanded form of `Asymptotics.IsBigOTVS.add` -/
Asymptotics.IsBigOTVS.fun_add : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F}
  {l : Filter α}, f₁ =O[𝕜; l] g → f₂ =O[𝕜; l] g → (fun i => f₁ i + f₂ i) =O[𝕜; l] g
-- Init.Data.UInt.Lemmas
UInt8.ofNat_bitVecToNat : ∀ (n : BitVec 8), UInt8.ofNat n.toNat = { toBitVec := n }
-- Aesop.Tracing
Aesop.nodeUnprovableEmoji : String
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.difference_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M}
  (hcov : IsCovariantDerivativeOn F cov s) (hcov' : IsCovariantDerivativeOn F cov' s) [inst_15 : CompleteSpace 𝕜]
  [inst_16 : FiniteDimensional 𝕜 F] [inst_17 : VectorBundle 𝕜 F V] [inst_18 : ContMDiffVectorBundle 1 F V I] {x : M},
  autoParam (x ∈ s) IsCovariantDerivativeOn.difference_apply._auto_1 →
    ∀ {σ : (x : M) → V x}, MDiffAt (T% σ) x → (hcov.difference hcov' x) (σ x) = cov σ x - cov' σ x
-- Mathlib.Data.List.Cycle
List.nextOr.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α) (x_1 x_2 : α),
  x.nextOr x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, default => default
    | [head], x, default => default
    | y :: z :: xs, x, default => if x = y then z else (z :: xs).nextOr x default
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Pulling back along the identity is naturally isomorphic to the identity functor.  -/
CategoryTheory.GrothendieckTopology.pullbackId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (X : C) → J.pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (J.Cover X)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.below : {α : Type u_1} →
  {s : Set (Set α)} →
    {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} →
      {a : Set α} → MeasurableSpace.GenerateMeasurable s a → Prop
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.IsThreeCycle.mem_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α}, f.IsThreeCycle → f ∈ alternatingGroup α
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.isCoprime_col : ∀ {R : Type v} [inst : CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) (j : Fin 2), IsCoprime (↑A 0 j) (↑A 1 j)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.instHasPullbackFst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (h : P ⟶ Y),
  CategoryTheory.Limits.HasPullback h (CategoryTheory.Limits.pullback.fst g f)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.realize_zero : ∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (v : α → R), FirstOrder.Language.Term.realize v 0 = 0
-- Init.Grind.Interactive
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
concatenating all goals produced by `tac'`.
 -/
Lean.Parser.Tactic.Grind.«grind_<;>_» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F' : Type u_21} [inst_6 : NormedDivisionRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiff p → (∀ (z : M), p z ≠ 0) → MDiff p⁻¹
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltSubmodule_le_leSubmodule : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : Γ₀ˣ), v.ltSubmodule γ ≤ v.leSubmodule ↑γ
-- Init.MetaTypes
Lean.Meta.instInhabitedTransparencyMode.default : Lean.Meta.TransparencyMode
-- Lean.Declaration
Lean.InductiveVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (numParams numIndices : ℕ) (all ctors : List Lean.Name) (numNested : ℕ)
  (isRec isUnsafe isReflexive : Bool) (toConstantVal_1 : Lean.ConstantVal) (numParams_1 numIndices_1 : ℕ)
  (all_1 ctors_1 : List Lean.Name) (numNested_1 : ℕ) (isRec_1 isUnsafe_1 isReflexive_1 : Bool),
  ({ toConstantVal := toConstantVal, numParams := numParams, numIndices := numIndices, all := all, ctors := ctors,
        numNested := numNested, isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive } =
      { toConstantVal := toConstantVal_1, numParams := numParams_1, numIndices := numIndices_1, all := all_1,
        ctors := ctors_1, numNested := numNested_1, isRec := isRec_1, isUnsafe := isUnsafe_1,
        isReflexive := isReflexive_1 }) =
    (toConstantVal = toConstantVal_1 ∧
      numParams = numParams_1 ∧
        numIndices = numIndices_1 ∧
          all = all_1 ∧
            ctors = ctors_1 ∧
              numNested = numNested_1 ∧ isRec = isRec_1 ∧ isUnsafe = isUnsafe_1 ∧ isReflexive = isReflexive_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The left Kan extension of `F : C ⥤ H` along a functor `L : C ⥤ D` is isomorphic to the
fiberwise colimit of the projection functor on the Grothendieck construction of the costructured
arrow category composed with `F`.  -/
CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] →
                  [inst_4 : L.HasLeftKanExtension F] →
                    L.leftKanExtension F ≅
                      CategoryTheory.Limits.fiberwiseColimit
                        ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).I = CategoryTheory.Abelian.image f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.isLongestRevMatch_sliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (self : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos),
  String.Slice.Pattern.Model.IsLongestRevMatch pat (endPos.sliceTo startPos ⋯)
-- Std.Async.TCP
/-- Creates a new TCP client socket.
 -/
Std.Async.TCP.Socket.Client.mk : IO Std.Async.TCP.Socket.Client
-- Mathlib.Topology.Compactness.CompactSystem
/-- In this equivalent formulation for a compact system,
note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`.  -/
isCompactSystem_iff_nonempty_iInter_of_lt : ∀ {α : Type u_1} (S : Set (Set α)),
  IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.ring : (self : RingCat) → Ring ↑self
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The natural equivalence `E × E₂ ≃ E₂ × E` is a linear isometry.  -/
LinearIsometryEquiv.prodComm : (R : Type u_1) →
  (E : Type u_5) →
    (E₂ : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : SeminormedAddCommGroup E₂] → [inst_3 : Module R E] → [inst_4 : Module R E₂] → E × E₂ ≃ₗᵢ[R] E₂ × E
-- Mathlib.Topology.Inseparable
Inseparable.rfl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, Inseparable x x
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- An auxiliary declaration to speed up typechecking.
 -/
ModuleCat.forget₂AddCommGroup_preservesLimitsAux : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            CategoryTheory.Limits.IsLimit
              ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).mapCone (ModuleCat.HasLimits.limitCone F))
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedMatcherInfo.default : Lean.Meta.MatcherInfo
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_subtype_embedding_eq : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (p' : Submodule R ↥p), (Submodule.MapSubtype.orderEmbedding p) p' = Submodule.map p.subtype p'
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative additive group and `n : ℕ`, `h : G → ℝ` satisfy
* there is `C : ℝ` such that for all `x y : G`, `|h (x + y) + h(x - y) - 2 * (h x + h y)| ≤ C`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

then the torsion subgroup of `G` is finite.  -/
AddCommGroup.finite_torsion_of_descent' : ∀ {G : Type u_1} [inst : AddCommGroup G] {h : G → ℝ} {C : ℝ},
  (∀ (x y : G), |h (x + y) + h (x - y) - 2 * (h x + h y)| ≤ C) → ∀ [Northcott h], Finite ↥(AddCommGroup.torsion G)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_log_nhdsLT_zero : Filter.Tendsto Real.log (nhdsWithin 0 (Set.Iio 0)) Filter.atBot
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.inv.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.inv = { inv := fun a => ⟨(↑a)⁻¹, ⋯⟩ }
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
some `ZMod (n i)` for some natural numbers `n i > 1`.  -/
AddCommGroup.equiv_directSum_zmod_of_finite' : ∀ (G : Type u_1) [inst : AddCommGroup G] [Finite G],
  ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ DirectSum ι fun i => ZMod (n i))
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_starProjection_apply : ∀ {𝕜 : 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}, v ∈ K → ‖K.starProjection v‖ = ‖v‖
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.mul.eq_1 : ∀ {n : ℕ} (a b : ZMod (2 * n)),
  QuaternionGroup.mul✝ (QuaternionGroup.a a) (QuaternionGroup.a b) = QuaternionGroup.a (a + b)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidalStruct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Mon.monMonoidalStruct =
    {
      tensorObj := fun M N =>
        { X := CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X,
          mon := CategoryTheory.MonObj.tensorObj.instTensorObj },
      whiskerLeft := fun X x x_1 g =>
        { hom := CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X g.hom, isMonHom_hom := ⋯ },
      whiskerRight := fun {X₁ X₂} f Y =>
        { hom := CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X, isMonHom_hom := ⋯ },
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g =>
        { hom := CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom, isMonHom_hom := ⋯ },
      tensorUnit :=
        { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, mon := CategoryTheory.MonObj.instTensorUnit },
      associator := fun M N P =>
        CategoryTheory.Mon.mkIso' (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X),
      leftUnitor := fun M => CategoryTheory.Mon.mkIso' (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X),
      rightUnitor := fun M => CategoryTheory.Mon.mkIso' (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X) }
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.coe_copy : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : CocompactMap α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpLoop : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.succ_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y}, Φ.prop f → Φ.succ X = Y
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.byCases`. -/
Classical.by_cases : ∀ {p q : Prop}, (p → q) → (¬p → q) → q
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_iff_relIndex_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsFiniteRelIndex K ↔ H.relIndex K ≠ 0
-- Mathlib.Order.Concept
upperPolar_union : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s₁ s₂ : Set α),
  upperPolar r (s₁ ∪ s₂) = upperPolar r s₁ ∩ upperPolar r s₂
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.le_comap_pow_ramificationIdx' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, p ≤ Ideal.comap (algebraMap R S) (P ^ p.ramificationIdx' P)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_map_of_gt : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i) (j : Fin (n + 2)),
  i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) self.map = SSet.const x
-- Init.Data.List.Nat.TakeDrop
List.head?_drop : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.drop i l).head? = l[i]?
-- Mathlib.Tactic.NormNum.Abs
Mathlib.Meta.NormNum.isNNRat_abs_nonneg : ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {num den : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a num den → Mathlib.Meta.NormNum.IsNNRat |a| num den
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rcc_eq_zero : ∀ {m n i : ℕ}, n + 1 ≤ i + m → (m...=n).toArray[i]! = 0
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.coe_mkHomeomorph : ∀ {M : Type u_1} [inst : TopologicalSpace M], ⇑DomAddAct.mkHomeomorph = ⇑DomAddAct.mk
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasGoodReduction_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.HasGoodReduction R W ↔
    WeierstrassCurve.IsMinimal R W ∧
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_map_subtype_le`. -/
lowerCentralSeries_map_subtype_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (n : ℕ),
  Subgroup.map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.encard_minimalCover : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.coveringNumber ε A ≠ ⊤ → (Metric.minimalCover ε A).encard = Metric.coveringNumber ε A
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (a_1 : a ⟶ b) {a_2 b_1 : Bᵒᵖ} (g : a_2 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_2 ⟶ a))),
  ((CategoryTheory.Bicategory.yoneda.map a_1).naturality g).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X a_1).inv
-- Mathlib.Algebra.Algebra.Basic
Module.algebraMap_end_eq_smul_id : ∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
  [inst_7 : IsScalarTower R S M] (a : R), (algebraMap R (Module.End S M)) a = a • LinearMap.id
-- Mathlib.Data.DFinsupp.Multiset
Multiset.equivDFinsupp_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (a : Multiset α), Multiset.equivDFinsupp a = Multiset.toDFinsupp a
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_iff_of_fintype : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  [inst_3 : Fintype ↑s] {x : M}, x ∈ Submodule.span R s ↔ ∃ f, ∑ a, f a • ↑a = x
-- Init.Data.Nat.Bitwise.Basic
/-- Asserts that the `(n+1)`th least significant bit of `m` is not set.

(This definition is used by Lean internally for compact bitmaps.)
 -/
Nat.hasNotBit : ℕ → ℕ → Prop
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_mul_sub : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c * ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x