mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Ray
/-- Any invertible action preserves the non-zeroness of ray vectors. This is primarily of interest
when `G = Rˣ`  -/
instMulActionRayVector : {M : Type u_2} →
  [inst : AddCommMonoid M] →
    {G : Type u_5} → [inst_1 : Group G] → [DistribMulAction G M] → {R : Type u_6} → MulAction G (RayVector R M)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_union_of_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.union m₂).contains k = true
-- Mathlib.Algebra.Module.PointwisePi
smul_pi₀ : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : GroupWithZero K] [inst_1 : (i : ι) → MulAction K (R i)]
  {r : K} (S : Set ι) (t : (i : ι) → Set (R i)), r ≠ 0 → r • S.pi t = S.pi (r • t)
-- Mathlib.Algebra.Category.Ring.Basic
/-- Build a `RingEquiv` from an isomorphism in the category `SemiRingCat`.  -/
CategoryTheory.Iso.semiRingCatIsoToRingEquiv : {R S : SemiRingCat} → (R ≅ S) → ↑R ≃+* ↑S
-- Std.Http.Data.Request
/-- Adds a single header to the request being built.
 -/
Std.Http.Request.Builder.header : Std.Http.Request.Builder → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Request.Builder
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse_apply_coe : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α)
  (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (a : α), ↑((Equiv.ofLeftInverse f f_inv hf) a) = f a
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀) =
    f
-- Mathlib.CategoryTheory.Action.Monoidal
Action.tensorUnit_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] {g : G},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).ρ g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)
-- Mathlib.CategoryTheory.Equivalence
/-- The inverse of an equivalence of categories is fully faithful.  -/
CategoryTheory.Equivalence.fullyFaithfulInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {E : Type u₃} → [inst_1 : CategoryTheory.Category.{v₃, u₃} E] → (e : C ≌ E) → e.inverse.FullyFaithful
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toList` always terminates after finitely many steps.
 -/
Std.Iter.toList : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → List β
-- Mathlib.Logic.Equiv.Set
Equiv.sigmaPreimageEquiv_symm_apply_snd_coe : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (x : α), ↑((Equiv.sigmaPreimageEquiv f).symm x).snd = x
-- Mathlib.Topology.Separation.Hausdorff
Homeomorph.t2Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y),
  T2Space Y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A chosen extension of a commutative square into a morphism of distinguished triangles.  -/
CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) →
                T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                  T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                    (a : T₁.obj₁ ⟶ T₂.obj₁) →
                      (b : T₁.obj₂ ⟶ T₂.obj₂) →
                        CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                          (T₁ ⟶ T₂)
-- Mathlib.Algebra.Group.Even
Even.zero : ∀ {α : Type u_2} [inst : AddZeroClass α], Even 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.toNat : Lean.Lsp.SemanticTokenModifier → ℕ
-- Mathlib.Algebra.Lie.Engel
LieEquiv.isEngelian_iff : ∀ {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂),
  LieAlgebra.IsEngelian R L ↔ LieAlgebra.IsEngelian R L₂
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular],
  μ ≠ 0 → ∀ {s : Set G}, IsOpen s → (0 < μ s ↔ s.Nonempty)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The first left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction X Y
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instMin : {α : Type u_2} → [inst : TopologicalSpace α] → Min (TopologicalSpace.Clopens α)
-- Mathlib.Order.Bounds.Image
/-- The image under a monotone function on a set `t` of a subset which has an upper bound in `t`
is bounded above.  -/
MonotoneOn.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  MonotoneOn f t → s ⊆ t → (upperBounds s ∩ t).Nonempty → BddAbove (f '' s)
-- Init.Data.Int.Lemmas
Int.natCast_add : ∀ (n m : ℕ), ↑(n + m) = ↑n + ↑m
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.mem_essImage_of_isConstant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (F : CategoryTheory.Sheaf J D) [CategoryTheory.Sheaf.IsConstant J F], (CategoryTheory.constantSheaf J D).essImage F
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.hom₂_ext_iff : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} {η θ : f ⟶ g}, η = θ ↔ η.hom = θ.hom
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If a lift of a circle map is bijective, then it is an order automorphism of the line.  -/
CircleDeg1Lift.toOrderIso : CircleDeg1Liftˣ →* ℝ ≃o ℝ
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (a : X ⟶ X), (hf.mulEquivEnd X) a = f.map a
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.lineGraph_adj_iff_exists : ∀ {V : Type u_1} {G : SimpleGraph V} {e₁ e₂ : ↑G.edgeSet}, G.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v ∈ ↑e₁, v ∈ ↑e₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.pairing_p_equivII : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : h.ι), h.pairing.p (h.equivII x) = h.equivI x
-- Mathlib.Probability.IdentDistrib
/-- A sequence of identically distributed Lᵖ functions is p-uniformly integrable.  -/
ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib : ∀ {α : Type u_1} [inst : MeasurableSpace α] {E : Type u_5} [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [BorelSpace E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_6} {f : ι → α → E} {j : ι}
  {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      MeasureTheory.MemLp (f j) p μ →
        (∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ) → MeasureTheory.UniformIntegrable f p μ
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.coe_extendRightEquiv' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (S : Type u_5) [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [inst_10 : IsScalarTower S (↥F) M]
  (a : ↥F), ↑((F.extendRightEquiv' M S) a) = (algebraMap (↥F) M) a
-- Init.Data.UInt.Lemmas
UInt8.ofFin_mk : ∀ {n : ℕ} (hn : n < UInt8.size), UInt8.ofFin ⟨n, hn⟩ = UInt8.ofNatLT n hn
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [PosMulMono M₀] [MulPosMono M₀],
  0 ≤ a → a ≤ b → ∀ (n : ℕ), a ^ n ≤ b ^ n
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_pow_injective : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ}, Function.Injective fun x => x * PowerSeries.X ^ k
-- Mathlib.Order.CompleteLatticeIntervals
subset_sSup_of_within : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
  t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s → sSup (Subtype.val '' t) = ↑(sSup t)
-- Mathlib.CategoryTheory.Limits.FintypeCat
equivIsoIso.eq_1 : ∀ {X Y : Type u},
  equivIsoIso =
    { hom := TypeCat.ofHom fun e => e.toIso, inv := TypeCat.ofHom fun i => i.toEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.id_map₂ : ∀ (B : Type u₁) [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (CategoryTheory.PrelaxFunctorStruct.id B).map₂ η = η
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.go.eq_2 : ∀ (k k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.addConst.go k (Lean.Grind.CommRing.Poly.add k_1 m p_1) =
    Lean.Grind.CommRing.Poly.add k_1 m (Lean.Grind.CommRing.Poly.addConst.go k p_1)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_ofSnowflaking_closedEBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.closedEBall x r =
    Metric.closedEBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Qq.Macro
Qq.Impl.isBad : Lean.Expr → Bool
-- Mathlib.GroupTheory.Congruence.Opposite
AddCon.unop.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon Mᵃᵒᵖ),
  c.unop = { r := fun a b => c (AddOpposite.op b) (AddOpposite.op a), iseqv := ⋯, add' := ⋯ }
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.symm_le_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.PartialEquiv M N} {g : L.PartialEquiv N M}, f.symm ≤ g ↔ f ≤ g.symm
-- Mathlib.MeasureTheory.Group.Arithmetic
AddUnits.instMeasurableSpace : {M : Type u_4} → [inst : AddMonoid M] → [MeasurableSpace M] → MeasurableSpace (AddUnits M)
-- Mathlib.AlgebraicGeometry.OpenImmersion
_private.Mathlib.AlgebraicGeometry.OpenImmersion.0.AlgebraicGeometry.IsOpenImmersion.termForget : Lean.ParserDescr
-- Init.Data.Int.LemmasAux
Int.neg_natCast_le_natCast : ∀ (n m : ℕ), -↑n ≤ ↑m
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- A linear projection onto `U` along its complement `V` is symmetric if
and only if `U` and `V` are pairwise orthogonal.  -/
Submodule.isSymmetric_projection_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), (U.projection V hUV).IsSymmetric ↔ U ⟂ V
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommGroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α], MulOpposite.instCommGroup = { toGroup := MulOpposite.instGroup, mul_comm := ⋯ }
-- Std.Time.Date.PlainDate
/-- Converts a `PlainDate` to the number of days since 1970-01-01T00:00:00.
 -/
Std.Time.PlainDate.toEpochDay : Std.Time.PlainDate → Std.Time.Day.Offset
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_eq' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) (s : Set α),
  ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain_zero : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h),
  DFinsupp.comapDomain h hh 0 = 0
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.instQuotePreresolvedMkStr1_lean : Lean.Quote Lean.Syntax.Preresolved
-- Lean.Elab.Do.Basic
/-- Whether the current `do` element is dead code. `elabDoElem` will emit a warning if not `.alive`.
 -/
Lean.Elab.Do.Context.deadCode : Lean.Elab.Do.Context → Lean.Elab.Do.CodeLiveness
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u` is a uniform structures on `β` and `f : γ → β`, then
`𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)`.  -/
UniformFun.comap_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {f : γ → β},
  UniformFun.uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (UniformFun.uniformSpace α β)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_mul : ∀ {α : Type u_2} [inst : Mul α] {t : Set α} {a : α}, {a} * t = (fun x => a * x) '' t
-- Mathlib.GroupTheory.CosetCover
Subgroup.leftCoset_cover_const_iff_surjOn : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G},
  ⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.dense_image_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G}
  {s : Set G}, Dense (QuotientGroup.mk '' s) ↔ Dense (s * ↑N)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b) (i_1 : I) (t_1 : A i_1 ⟶ X)
  (b_1 : B i_1 ⟶ S) (w_1 : CategoryTheory.CategoryStruct.comp t_1 πX = CategoryTheory.CategoryStruct.comp (f i_1) b_1),
  ({ i := i, t := t, b := b, w := w } = { i := i_1, t := t_1, b := b_1, w := w_1 }) = (i = i_1 ∧ t ≍ t_1 ∧ b ≍ b_1)
-- Mathlib.GroupTheory.Divisible
/-- An additive group is `ℕ`-divisible if it `ℤ`-divisible.  -/
AddGroup.divisibleByNatOfDivisibleByInt : (A : Type u_1) → [inst : AddGroup A] → [DivisibleBy A ℤ] → DivisibleBy A ℕ
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.normalizer_addCommutator_ge_left : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), H₁ ≤ AddSubgroup.normalizer ↑⁅H₁, H₂⁆
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  {k : α} {f : β → β} {fallback : α},
  compare ((Std.ExtDTreeMap.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Order.Hom.Set
OrderIso.subsingleton_of_wellFoundedGT' : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [WellFoundedGT β] [inst_2 : Preorder α], Subsingleton (α ≃o β)
-- Mathlib.Algebra.Lie.Rank
LieModule.rank_le_card : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) {ιₘ : Type u_6} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M]
  [inst_6 : Module R M] [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] [inst_11 : Fintype ιₘ] (bₘ : Module.Basis ιₘ R M) [Nontrivial R],
  LieModule.rank R L M ≤ Fintype.card ιₘ
-- Mathlib.Topology.Metrizable.Urysohn
/-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second
countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the
same topology.  -/
TopologicalSpace.metrizableSpace_of_t3_secondCountable : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T3Space X] [SecondCountableTopology X], TopologicalSpace.MetrizableSpace X
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.mul : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ},
  Asymptotics.IsBigOWith c₁ l f₁ g₁ →
    Asymptotics.IsBigOWith c₂ l f₂ g₂ → Asymptotics.IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.prop : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] (self : Topology.ContinuousMapGeneratedBy X Y Z),
  Topology.ContinuousGeneratedBy X self.toFun
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then some k else none
    else t.getKey? k'
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β},
  m.WF → ∀ {hc : k ∈ Std.DHashMap.Raw.Const.modify m k f}, (Std.DHashMap.Raw.Const.modify m k f).getKey k hc = k
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B} (a : A),
  MonoidWithZeroHom.ValueGroup₀.embedding ((MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a) = f a
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instInhabitedSpan : Inhabited Std.Time.Nanosecond.Span
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_div : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f g : α → G),
  (s.mulIndicator fun a => f a / g a) = fun a => s.mulIndicator f a / s.mulIndicator g a
-- Init.Data.SInt.Bitwise
Int16.toBitVec_shiftLeft : ∀ (a b : Int16), (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 16
-- Mathlib.NumberTheory.RatFunc.Ostrowski
/-- **Ostrowski's Theorem** for `K(X)` with `K` any field:
A discrete valuation of rank 1 that is trivial on `K` is equivalent either to the valuation
at infinity or to the `p`-adic valuation for a unique maximal ideal `p` of `K[X]`.  -/
RatFunc.valuation_isEquiv_infty_or_adic : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [v.IsRankOneDiscrete] [Valuation.IsTrivialOn K v] [inst_4 : DecidableEq (RatFunc K)],
  Xor (v.IsEquiv (RatFunc.inftyValuation K))
    (∃! u, v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u))
-- Mathlib.Data.List.PeriodicityLemma
/-- If `w` has a period `p`, and we extend it to the left by its prefix whose length divides `p`,
then the resulting word also has a period `p`.  -/
List.HasPeriod.take_append : ∀ {α : Type u_1} (p n : ℕ) (w : List α), p ∣ n → n ≤ w.length → w.HasPeriod p → (List.take n w ++ w).HasPeriod p
-- Mathlib.Algebra.Group.Subgroup.Pointwise
op_vadd_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : AddGroup G] [inst_1 : SetLike S G] [AddSubgroupClass S G] {s : S} {a : G},
  a ∈ s → AddOpposite.op a +ᵥ ↑s = ↑s
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.lintegral_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {μ ν : MeasureTheory.Measure M}
  [MeasureTheory.SFinite ν] {f : M → ENNReal},
  Measurable f → ∫⁻ (z : M), f z ∂μ.conv ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x + y) ∂ν ∂μ
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply_combination_of_mem : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι},
  i ∈ s → ∀ {w : ι → k}, s.sum w = 1 → (b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.wellFoundedLT_of_finite : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Π₀ (i : ι), α i)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat) {Z : CommRingCat}
  (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv ((CategoryTheory.ConcreteCategory.hom e.hom.base) x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom x) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h
-- Mathlib.RingTheory.Ideal.Over
Ideal.algebraMapSubmonoid_primeCompl_of_liesOver_surjective : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : p.IsPrime] [inst_4 : P.IsPrime] [P.LiesOver p],
  Function.Surjective ⇑(algebraMap A B) → Algebra.algebraMapSubmonoid B p.primeCompl = P.primeCompl
-- Mathlib.Data.Fintype.Defs
Finset.coe_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, ↑s = Set.univ ↔ s = Finset.univ
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.equivalenceRightToLeft_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve),
  (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).right = G.right
-- Mathlib.Logic.Equiv.Fin.Basic
prodEquivPiFinTwo_symm_apply : ∀ (α β : Type u), ⇑(prodEquivPiFinTwo α β).symm = fun f => (f 0, f 1)
-- Std.Async.System
Std.Async.System.GroupId.mk : ℕ → Std.Async.System.GroupId
-- Mathlib.RingTheory.WittVector.Compare
WittVector.toPadicInt.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.toPadicInt p = PadicInt.lift ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (CategoryTheory.StrictPseudofunctor.id B).map₂ η = η