mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableConstSMul.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : MeasurableSpace α],
  autoParam (∀ (c : M), Measurable fun x => c • x) MeasurableConstSMul.measurable_const_smul._autoParam →
    MeasurableConstSMul M α
-- Lean.Level
Lean.Level.isMax : Lean.Level → Bool
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- Two `R`-linear functors out of the `R`-linear completion are isomorphic iff their
compositions with the embedding functor are isomorphic.
 -/
CategoryTheory.Free.ext : (R : Type u_1) →
  [inst : CommRing R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [inst_4 : CategoryTheory.Linear R D] →
                {F G : CategoryTheory.Functor (CategoryTheory.Free R C) D} →
                  [F.Additive] →
                    [CategoryTheory.Functor.Linear R F] →
                      [G.Additive] →
                        [CategoryTheory.Functor.Linear R G] →
                          ((CategoryTheory.Free.embedding R C).comp F ≅ (CategoryTheory.Free.embedding R C).comp G) →
                            (F ≅ G)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_subset_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α} {m n : ℕ},
  s ⊆ t → 1 ∈ t → m ≤ n → s ^ m ⊆ t ^ n
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.isEmbedding_toContinuousMap : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], Topology.IsEmbedding toContinuousMap
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.mkEOI : Lean.Parser.InputContext → String.Pos.Raw → Lean.Syntax
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionOntoL_apply_left : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : ↥p), (p.projectionOntoL q h) ↑x = x
-- Mathlib.Analysis.Normed.Group.Pointwise
infEDist_neg : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x : E) (s : Set E), Metric.infEDist (-x) s = Metric.infEDist x (-s)
-- Mathlib.Topology.Germ
/-- The map `Germ (𝓝 x) E → E` into a monoid `E` as a monoid homomorphism  -/
Filter.Germ.valueMulHom : {X : Type u_4} → {E : Type u_5} → [inst : Monoid E] → [inst_1 : TopologicalSpace X] → {x : X} → (nhds x).Germ E →* E
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.functor_unit_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X))
      (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) =
    h
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The isomorphism from `Multiplicative (ZMod n)` to any multiplicative group
of `Nat.card` equal to `n` generated by a single element `g` which sends
`Multiplicative.ofAdd 1` to `g`.
See `zmodCyclicMulEquiv` for a version which doesn't take an explicit generator,
and instead picks one out with the axiom of choice.  -/
zmodMulEquivOfGenerator : {G : Type u_2} →
  [inst : Group G] →
    {g : G} → (∀ (x : G), x ∈ Subgroup.zpowers g) → {n : ℕ} → Nat.card G = n → Multiplicative (ZMod n) ≃* G
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.instIsIsoFunctorOppositeNatTransOp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (α : CategoryTheory.TwoSquare T L R B)
  [CategoryTheory.IsIso α.natTrans], CategoryTheory.IsIso α.op.natTrans
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The composition of an isomorphism between equivalent group extensions and a section  -/
GroupExtension.Section.equivComp : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] →
        {E : Type u_3} →
          [inst_2 : Group E] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : Group E'] → {S' : GroupExtension N E' G} → S.Section → S.Equiv S' → S'.Section
-- Mathlib.Order.Bounded
Set.bounded_gt_inter_gt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] [NoMinOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 > x2) (s ∩ {b | b < a}) ↔ Set.Bounded (fun x1 x2 => x1 > x2) s
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F],
  ProbabilityTheory.HasGaussianLaw X P → ∀ (L : E →L[ℝ] F), ProbabilityTheory.HasGaussianLaw (⇑L ∘ X) P
-- Std.Http.Data.Response
/-- The main parts of a response.
 -/
Std.Http.Response.Head : Type
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.subsingleton_of_subsingleton : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [Subsingleton A], Subsingleton (NonUnitalStarSubalgebra R A)
-- Init.Data.SInt.Bitwise
Int16.zero_shiftRight : ∀ {a : Int16}, 0 >>> a = 0
-- Mathlib.Tactic.NormNum.NatFactorial
_private.Mathlib.Tactic.NormNum.NatFactorial.0.Mathlib.Meta.NormNum.evalNatDescFactorialNotZero : {x' y' : Q(ℕ)} →
  (x y z : Q(ℕ)) →
    «$x» =Q «$z» + «$y» →
      Q(Mathlib.Meta.NormNum.IsNat «$x'» «$x») →
        Q(Mathlib.Meta.NormNum.IsNat «$y'» «$y») →
          (n : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$x'».descFactorial «$y'») «$n»)
-- Lean.Parser.Extra
Lean.Parser.sepByIndent.parenthesizer : Lean.PrettyPrinter.Parenthesizer →
  String → Lean.PrettyPrinter.Parenthesizer → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `M` is a faithfully flat module, then for all linear maps `f`, the map `f ⊗ id = 0`, if and only
if `f = 0`.  -/
Module.FaithfullyFlat.zero_iff_rTensor_zero : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [h : Module.FaithfullyFlat R M] {N : Type u_1} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type u_2}
  [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'), f = 0 ↔ LinearMap.rTensor M f = 0
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_join_eq_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.join P Q = Q
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
le_padicValNat_iff_replicate_subperm_primeFactorsList : ∀ {a b n : ℕ}, Nat.Prime a → b ≠ 0 → (n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList)
-- Mathlib.Algebra.Group.Action.Defs
/-- A typeclass indicating that the right (aka `MulOpposite`) and left actions by `M` on `α` are
equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
for `•`.  -/
IsCentralScalar : (M : Type u_9) → (α : Type u_10) → [SMul M α] → [SMul Mᵐᵒᵖ α] → Prop
-- Mathlib.Algebra.Ring.Equiv
/-- The `RingEquiv` between two semirings with a unique element.  -/
RingEquiv.ofUnique : {M : Type u_7} →
  {N : Type u_8} →
    [Unique M] → [Unique N] → [inst : Add M] → [inst_1 : Mul M] → [inst_2 : Add N] → [inst_3 : Mul N] → M ≃+* N
-- Std.Do.Triple.SpecLemmas
MonadWithReader.withReader.eq_1 : ∀ {ρ : Type u} (m : Type u → Type v) [self : MonadWithReader ρ m], @withReader ρ m self = self.1
-- Mathlib.Topology.EMetricSpace.Defs
instPseudoEMetricSpaceMultiplicative : {X : Type u_1} → [PseudoEMetricSpace X] → PseudoEMetricSpace (Multiplicative X)
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.bijective_eq_sup : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  CategoryTheory.MorphismProperty.bijective C =
    CategoryTheory.MorphismProperty.injective C ⊓ CategoryTheory.MorphismProperty.surjective C
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Iio : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R},
  Int.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉
-- Lean.Compiler.InitAttr
/-- Set of modules for which we have already run the module initializer in the interpreter.  -/
Lean.interpretedModInits : IO.Ref Lean.NameSet
-- Aesop.Script.CtorNames
Aesop.CtorNames.args : Aesop.CtorNames → Array Lean.Name
-- Mathlib.Algebra.BigOperators.Associated
Prime.not_dvd_finsuppProd : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ},
  Prime p → (∀ a ∈ f.support, ¬p ∣ g a (f a)) → ¬p ∣ f.prod g
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_mapComp_hom_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (a_1 : Bᵒᵖ)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  ((CategoryTheory.Bicategory.yoneda.mapComp f g).hom.as.app a_1).toNatTrans.app X =
    (CategoryTheory.Bicategory.associator X f g).inv
-- Lean.Elab.SyntheticMVars
/-- Keep invoking `synthesizeUsingDefault` until it returns false.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultLoop : Lean.Elab.TermElabM Unit
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_mul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (f₁ f₂ : M →ₗ[A] M),
  (TensorProduct.AlgebraTensorModule.rTensor R M) (f₁ * f₂) =
    (TensorProduct.AlgebraTensorModule.rTensor R M) f₁ * (TensorProduct.AlgebraTensorModule.rTensor R M) f₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α},
  ∅.get? a = none
-- Mathlib.GroupTheory.Index
Subgroup.one_lt_index_of_ne_top : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [Finite (G ⧸ H)], H ≠ ⊤ → 1 < H.index
-- Lean.Declaration
Lean.Declaration.isUnsafeInductiveDeclEx : Lean.Declaration → Bool
-- Mathlib.Dynamics.Minimal
IsOpen.iUnion_preimage_vadd : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] {U : Set α}, IsOpen U → U.Nonempty → ⋃ c, (fun x => c +ᵥ x) ⁻¹' U = Set.univ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.mk.inj : ∀ {name : String} {kind : Lean.Lsp.SymbolKind} {tags? : Option (Array Lean.Lsp.SymbolTag)} {detail? : Option String}
  {uri : Lean.Lsp.DocumentUri} {range selectionRange : Lean.Lsp.Range} {data? : Option Lean.Json} {name_1 : String}
  {kind_1 : Lean.Lsp.SymbolKind} {tags?_1 : Option (Array Lean.Lsp.SymbolTag)} {detail?_1 : Option String}
  {uri_1 : Lean.Lsp.DocumentUri} {range_1 selectionRange_1 : Lean.Lsp.Range} {data?_1 : Option Lean.Json},
  { name := name, kind := kind, tags? := tags?, detail? := detail?, uri := uri, range := range,
        selectionRange := selectionRange, data? := data? } =
      { name := name_1, kind := kind_1, tags? := tags?_1, detail? := detail?_1, uri := uri_1, range := range_1,
        selectionRange := selectionRange_1, data? := data?_1 } →
    name = name_1 ∧
      kind = kind_1 ∧
        tags? = tags?_1 ∧
          detail? = detail?_1 ∧ uri = uri_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1 ∧ data? = data?_1
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- **Alias** of `AddSubgroup.mem_normalizer_iff_addConj_image_eq`. -/
AddSubgroup.mem_normalizer_iff_conj_image_eq : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {g : G}, g ∈ AddSubgroup.normalizer s ↔ ⇑(AddAut.addConj g) '' s = s
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.mk.inj : ∀ {stained : Mathlib.Linter.Flexible.Stained✝} {stx : Lean.Syntax} {ci : Lean.Elab.ContextInfo}
  {mctx : Lean.MetavarContext} {goals : List Lean.MVarId} {stained_1 : Mathlib.Linter.Flexible.Stained✝}
  {stx_1 : Lean.Syntax} {ci_1 : Lean.Elab.ContextInfo} {mctx_1 : Lean.MetavarContext} {goals_1 : List Lean.MVarId},
  { stained := stained, stx := stx, ci := ci, mctx := mctx, goals := goals } =
      { stained := stained_1, stx := stx_1, ci := ci_1, mctx := mctx_1, goals := goals_1 } →
    stained = stained_1 ∧ stx = stx_1 ∧ ci = ci_1 ∧ mctx = mctx_1 ∧ goals = goals_1
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_iInf : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Sort u_3}
  (f : L.Hom M N) (s : ι → L.Substructure N),
  FirstOrder.Language.Substructure.comap f (⨅ i, s i) = ⨅ i, FirstOrder.Language.Substructure.comap f (s i)
-- Mathlib.Data.Multiset.UnionInter
Multiset.map_union : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ {s t : Multiset α}, Multiset.map f (s ∪ t) = Multiset.map f s ∪ Multiset.map f t
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAdjointPair.add : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {f f' : M → M₁}
  {g g' : M₁ → M}, B.IsAdjointPair B' f g → B.IsAdjointPair B' f' g' → B.IsAdjointPair B' (f + f') (g + g')
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The morphism `reflection W Z κ : Z ⟶ reflectionObj W Z κ` exhibits `reflectionObj W Z κ`
as the image of `Z` by the left adjoint of the inclusion `W.isLocal.ι`.  -/
CategoryTheory.OrthogonalReflection.corepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [inst_4 :
                  ∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                {κ : Cardinal.{w}} →
                  [inst_5 : OrderBot κ.ord.ToType] →
                    [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] →
                      [inst_7 : Fact κ.IsRegular] →
                        (hW :
                            ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                              W f →
                                CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
                          (W.isLocal.ι.comp (CategoryTheory.coyoneda.obj (Opposite.op Z))).CorepresentableBy
                            { obj := CategoryTheory.OrthogonalReflection.reflectionObj W Z κ, property := ⋯ }
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.trans_one : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.trans 1 = e
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_list_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, Std.ExtDTreeMap.Const.insertMany t l = ∅ ↔ t = ∅ ∧ l = []
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.eq_go : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (x : Option ((a : α) × β a))
  (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.getEntryGE? k t).or x = Std.DTreeMap.Internal.Impl.getEntryGE?.go k x t
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The class of morphisms containing a single morphism.  -/
CategoryTheory.MorphismProperty.single : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → CategoryTheory.MorphismProperty C
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The change of variables base changed to an algebra `A` over `R`.  -/
WeierstrassCurve.VariableChange.baseChange : {R : Type u} →
  [inst : CommRing R] →
    WeierstrassCurve.VariableChange R →
      (A : Type v) → [inst_1 : CommRing A] → [Algebra R A] → WeierstrassCurve.VariableChange A
-- Mathlib.Topology.MetricSpace.Defs
eq_of_forall_dist_le : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, (∀ ε > 0, dist x y ≤ ε) → x = y
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The inverse map of a homeomorphism is a continuous function.  -/
ContinuousMulEquiv.continuous_invFun : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (self : G ≃ₜ* H), Continuous self.invFun
-- Init.Tactics
/-- The `norm_cast` attribute should be given to lemmas that describe the
behaviour of a coercion with respect to an operator, a relation, or a particular
function.

It only concerns equality or iff lemmas involving `↑`, `⇑` and `↥`, describing the behavior of
the coercion functions.
It does not apply to the explicit functions that define the coercions.

Examples:
```lean
@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n

@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1

@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n

@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n

@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n

@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
```

Lemmas tagged with `@[norm_cast]` are classified into three categories: `move`, `elim`, and
`squash`. They are classified roughly as follows:

* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

`norm_cast` uses `move` and `elim` lemmas to factor coercions toward the root of an expression
and to cancel them from both sides of an equation or relation. It uses `squash` lemmas to clean
up the result.

It is typically not necessary to specify these categories, as `norm_cast` lemmas are
automatically classified by default. The automatic classification can be overridden by
giving an optional `elim`, `move`, or `squash` parameter to the attribute.

```lean
@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
  rw [← of_real_nat_cast, of_real_re]
```

Don't do this unless you understand what you are doing.
 -/
Lean.Parser.Attr.norm_cast : Lean.ParserDescr
-- Mathlib.NumberTheory.Bertrand
/-- Proves that Bertrand's postulate holds over all positive naturals less than n by identifying a
descending list of primes, each no more than twice the next, such that the list contains a witness
for each number ≤ n.
 -/
Nat.exists_prime_lt_and_le_two_mul_succ : ∀ {n : ℕ} (q : ℕ) {p : ℕ},
  Nat.Prime p →
    p ≤ 2 * q → (n < q → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) → n < p → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-- Mathlib.Order.Filter.Map
Filter.comap_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, (Filter.comap m f).NeBot ↔ ∀ t ∈ f, ∃ a, m a ∈ t
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH2_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  (groupCohomology.shortComplexH2 A).f = groupCohomology.d₁₂ A
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- A tensor product analogue of `mul_left_comm`.  -/
TensorProduct.leftComm : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (N : Type u_6) →
        (P : Type u_7) →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      TensorProduct R M (TensorProduct R N P) ≃ₗ[R] TensorProduct R N (TensorProduct R M P)
-- Std.Async.Basic
/-- Creates a new `ETask` that will run after `x` has finished. If `x`:
- errors, return an `ETask` that resolves to the error.
- succeeds, return an `ETask` that resolves to `f x`.
 -/
Std.Async.ETask.map : {α β ε : Type} →
  (α → β) →
    Std.Async.ETask ε α → optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.ETask ε β
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported : {α : Type u_1} →
  {γ : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : NonUnitalNormedRing γ] → SMul C(α, γ) ↥(compactlySupported α γ)
-- Mathlib.Topology.Compactness.Compact
/-- A set `s` is compact if and only if
for every open cover of `s`, there exists a finite subcover.  -/
isCompact_iff_finite_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.instInhabitedOfNatNat : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → [Inhabited P] → Inhabited (Affine.Simplex k P 0)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instMax.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instMax = { max := fun s t => { carrier := ↑s ∪ ↑t, vadd_mem' := ⋯ } }
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift an injective ring homomorphism `R[X] →+* L` to a `R⟮X⟯ →+* L`
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.liftRingHom : {L : Type u_2} →
  {R : Type u_3} →
    [inst : Field L] →
      [inst_1 : CommRing R] →
        (φ : Polynomial R →+* L) →
          nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L) → RatFunc R →+* L
-- Mathlib.Data.TypeVec
TypeVec.Curry.inhabited : {n : ℕ} →
  (F : TypeVec.{u} (n + 1) → Type u_1) →
    (α : Type u) → (β : TypeVec.{u} n) → [I : Inhabited (F (β ::: α))] → Inhabited (TypeVec.Curry F α β)
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.instPrecoherentSmallModel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C]
  [inst_2 : CategoryTheory.EssentiallySmall.{u_3, v_1, u_1} C],
  CategoryTheory.Precoherent (CategoryTheory.SmallModel.{u_3, v_1, u_1} C)
-- Mathlib.Algebra.Free
FreeMagma.instLawfulMonad : LawfulMonad FreeMagma