mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_smul_closedEBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal),
  (fun x => c • x) ⁻¹' Metric.closedEBall x r = Metric.closedEBall (c⁻¹ • x) r
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G =
    CategoryTheory.Localization.lift₂NatIso L L W W (CategoryTheory.MonoidalCategory.curriedTensorPre G)
      (CategoryTheory.MonoidalCategory.curriedTensorPost G) (CategoryTheory.MonoidalCategory.curriedTensorPre F)
      (CategoryTheory.MonoidalCategory.curriedTensorPost F)
      (CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost G)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'Factor_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.mixedEmbedding.convexBodyLT'Factor K ≠ 0
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_set_left : ∀ (xs ys : Lean.Omega.Coeffs) (i : ℕ) (z : ℤ), (xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Linear_CC'.congr_simp : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.Linear_CC' C hsC ho = Profinite.NobelingProof.Linear_CC' C hsC ho
-- Init.Data.String.Bootstrap
String.Internal.atEnd : String → String.Pos.Raw → Bool
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.isSplitMono_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [F.Full] [F.Faithful],
  CategoryTheory.IsSplitMono (F.map f) ↔ CategoryTheory.IsSplitMono f
-- Mathlib.Data.Sym.Sym2
/-- Given `[DecidableEq α]` and `[Fintype α]`, the following instance gives `Fintype (Sym2 α)`.
 -/
Sym2.instDecidableRel : {α : Type u_1} → [DecidableEq α] → DecidableRel (Sym2.Rel α)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mul_single : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → MulZeroClass (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)]
  [inst_4 : ∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r : G i)
  (x : RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite),
  RestrictedProduct.single A i (x i * r) = x * RestrictedProduct.single A i r
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instVAdd : (p : ENNReal) → (K : Type u_1) → (V : Type u_4) → [VAdd K V] → VAdd K (WithLp p V)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_symm_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p]
  (x : M) (n : ℕ) (y : K),
  j y = x ^ p ^ n → (IsPerfectClosure.equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)
-- Init.Data.Array.Lemmas
/-- Variant of `any_filter` with a side condition for the `stop` argument.  -/
Array.any_filter' : ∀ {α : Type u_1} {stop : ℕ} {xs : Array α} {p q : α → Bool},
  stop = (Array.filter p xs).size → (Array.filter p xs).any q 0 stop = xs.any fun a => p a && q a
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivial_comon_comul_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.comul.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.lowerSemicontinuousOn_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → 0 ≤ y → LowerSemicontinuousOn (s.indicator fun _x => y) t
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
-- Mathlib.Condensed.Discrete.Colimit
/-- Given a presheaf `F` on `LightProfinite`, `lanPresheaf F` is the left Kan extension of its
restriction to finite sets along the inclusion functor of finite sets into `Profinite`.
 -/
LightCondensed.lanPresheaf : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u) → CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.tendsto_iff_tendstoUniformly : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {ι : Type u_2}
  {F : ι → BoundedContinuousFunction α β} {f : BoundedContinuousFunction α β} {l : Filter ι},
  Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.Pi.functor.eq_1 : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.Pi.functor α =
    { obj := fun f => ∏ᶜ f, map := fun {f g} t => CategoryTheory.Limits.Pi.map t, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.RingTheory.Ideal.GoingUp
/-- The identity in this lemma asserts that the "obvious" square
```
    R    → (R / (P ∩ R))
    ↓          ↓
R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))
```
commutes.  It is used, for instance, in the proof of `quotient_mk_comp_C_is_integral_of_jacobson`,
in the file `Mathlib/RingTheory/Jacobson/Polynomial.lean`.
 -/
Ideal.quotient_mk_maps_eq : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)),
  ((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp
          Polynomial.C).comp
      (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) =
    (Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
          (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯).comp
      ((Ideal.Quotient.mk P).comp Polynomial.C)
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.instInhabited : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Batteries.HashMap α β)
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.IsConvexDist.mk : ∀ {X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X],
  (∀ (f : Convexity.StdSimplex ℝ (X × X)),
      dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤
        Convexity.iConvexComb f fun x => dist x.1 x.2) →
    Convexity.IsConvexDist X
-- Mathlib.Algebra.Lie.Basic
/-- A Lie module bracket is compatible with scalar multiplication in its second argument.  -/
LieModule.lie_smul : ∀ {R : Type u} {L : Type v} {M : Type w} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} [self : LieModule R L M] (t : R) (x : L)
  (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆
-- Mathlib.Analysis.Convex.Segment
sameRay_of_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommRing 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y z : E}, x ∈ segment 𝕜 y z → SameRay 𝕜 (x - y) (z - x)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Field R] [inst_1 : StarRing R] [inst_2 : Ring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S) (h1 : 1 ∉ s)
  (a : Unitization R ↥s),
  ↑((NonUnitalStarSubalgebra.unitizationStarAlgEquiv s h1) a) = (algebraMap R A) a.toProd.1 + ↑a.toProd.2
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- `relName` is the relation of the lemma.  -/
Mathlib.Tactic.ClickSuggestions.GrwLemma.relName : Mathlib.Tactic.ClickSuggestions.GrwLemma → Lean.Name
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_inv_hom_id_eval_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (j : J) (Y_1 : D) {Z : E} (h : (F.obj (Y j)).obj Y_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y_1)
      (CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y_1) h) =
    h
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β} {ιf : Type u_7} {ιg : Type u_8}
  {pf : ιf → Prop} {sf : ιf → Set α} {pg : ιg → Prop} {sg : ιg → Set β},
  f.HasBasis pf sf → g.HasBasis pg sg → (f +ᵥ g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 +ᵥ sg i.2
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_3.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.Analysis.Normed.Group.NullSubmodule
isClosed_nullSubgroup : ∀ {M : Type u_1} [inst : SeminormedCommGroup M], IsClosed ↑(nullSubgroup M)
-- Mathlib.Data.List.Sublists
List.sublistsLen_of_length_lt : ∀ {α : Type u} {n : ℕ} {l : List α}, l.length < n → List.sublistsLen n l = []
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  m.WF → Std.DHashMap.Raw.forIn (fun a x d => f a d) init m = forIn m.keysArray init f
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.replaceFTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (acc : Array α) (h_1 : (acc : Array α) → motive [] acc)
  (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_1 acc
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod_right : ∀ (a : ℤ) (b : ℕ), (a + ↑b).bmod b = a.bmod b
-- Mathlib.Topology.Instances.CantorSet
preCantorSet_subset_unitInterval : ∀ {n : ℕ}, preCantorSet n ⊆ Set.Icc 0 1
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- A topological group is nonarchimedean if every neighborhood of 1 contains an open subgroup.  -/
NonarchimedeanGroup : (G : Type u_1) → [Group G] → [TopologicalSpace G] → Prop
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isRetrocompact_basicOpen : ∀ {R : Type u} [inst : CommSemiring R] {f : R}, IsRetrocompact ↑(PrimeSpectrum.basicOpen f)
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertModifier : Std.Time.Modifier → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Topology.Defs.Induced
/-- A function between topological spaces is a quotient map if it is surjective,
and for all `s : Set Y`, `s` is open iff its preimage is an open set.  -/
Topology.IsQuotientMap : {X : Type u_3} → {Y : Type u_4} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Lean.Elab.DocString
Lean.Doc.State.mk : List Lean.Elab.Command.Scope →
  List Lean.OpenDecl → Lean.LocalContext → Lean.LocalInstances → Lean.Options → Lean.Doc.State
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.WorkspaceEditClientCapabilities
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (h₁ h₂ : CategoryTheory.GrpObj X), h₁.toMonObj = h₂.toMonObj → h₁ = h₂
-- Init.Data.String.Basic
String.Slice.getUTF8Byte_copy : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.copy.rawEndPos}, s.copy.getUTF8Byte p h = s.getUTF8Byte p ⋯
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The forgetful functor from `Bipointed` to `Pointed` which forgets about the second point.  -/
bipointedToPointedFst : CategoryTheory.Functor Bipointed Pointed
-- Mathlib.Order.Lattice
SemilatticeSup.mk : {α : Type u} →
  [toPartialOrder : PartialOrder α] →
    (sup : α → α → α) →
      (∀ (a b : α), a ≤ sup a b) →
        (∀ (a b : α), b ≤ sup a b) → (∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c) → SemilatticeSup α
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofPartialTermInfo : Lean.Elab.PartialTermInfo → Lean.Elab.Info
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_eq_zero' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → ((μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0)
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`.  -/
Rep.counitIsoAddEquiv : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        {M : ModuleCat (MonoidAlgebra k G)} → ↑((Rep.ofModuleMonoidAlgebra.comp Rep.toModuleMonoidAlgebra).obj M) ≃+ ↑M
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- This takes in an `NeZero n` instance instead of an `n ≠ 0` hypothesis.  -/
ArithmeticFunction.carmichael_eq_exponent' : ∀ (n : ℕ) [NeZero n], ArithmeticFunction.carmichael n = Monoid.exponent (ZMod n)ˣ
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Assume that
1. `C` has binary products and pullbacks,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products and pullbacks.

For an object `X` in a category `D`, if every morphism of the form `F.obj a ⟶ X` is relatively
representable with respect to `F`, so is the diagonal morphism `X ⟶ X × X`.
 -/
CategoryTheory.Functor.relativelyRepresentable.diag_of_map_from_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] {X : D},
  (∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g) → F.relativelyRepresentable (CategoryTheory.Limits.diag X)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.ext : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {x y : Combinatorics.Subspace η α ι}, x.idxFun = y.idxFun → x = y
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.toBinaryTree.eq_1 : ∀ {α : Type u_1}, Ordnode.nil.toBinaryTree = BinaryTree.nil
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.setIntegral_condExp_le_of_ae_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ {f : α → ℝ}, 0 ≤ᵐ[μ] f → ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ
-- Mathlib.GroupTheory.Torsion
CommGroup.mem_torsion : ∀ {G : Type u_1} [inst : CommGroup G] (g : G), g ∈ CommGroup.torsion G ↔ IsOfFinOrder g
-- Mathlib.Topology.ContinuousOn
ContinuousOn.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α},
  ContinuousOn f s → Set.EqOn g f s → ContinuousOn g s
-- Mathlib.Data.EReal.Inv
EReal.instCommMonoidWithZero : CommMonoidWithZero EReal
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Inverse `DilationEquiv`.  -/
DilationEquiv.symm : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵈ Y → Y ≃ᵈ X
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.commonPrefix.loop.eq_def : ∀ (s t : Substring.Raw) (spos tpos : String.Pos.Raw),
  Substring.Raw.commonPrefix.loop✝ s t spos tpos =
    if h : spos < s.stopPos ∧ tpos < t.stopPos then
      if (String.Pos.Raw.get s.str spos == String.Pos.Raw.get t.str tpos) = true then
        have this := ⋯;
        Substring.Raw.commonPrefix.loop✝ s t (String.Pos.Raw.next s.str spos) (String.Pos.Raw.next t.str tpos)
      else spos
    else spos
-- Init.Internal.Order.Basic
/-- The “less-or-equal-to” or “approximates” relation is transitive.  -/
Lean.Order.PartialOrder.rel_trans : ∀ {α : Sort u} [self : Lean.Order.PartialOrder α] {x y z : α},
  Lean.Order.PartialOrder.rel x y → Lean.Order.PartialOrder.rel y z → Lean.Order.PartialOrder.rel x z
-- Mathlib.RingTheory.SimpleModule.Basic
Module.Finite.of_isComplemented_domain : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  (R₀ : Type u_6) (P : Type u_7) [inst_3 : Semiring R₀] [inst_4 : AddCommMonoid P] [inst_5 : Module R P]
  [inst_6 : Module R₀ P] [inst_7 : SMulCommClass R R₀ P] [Module.Finite R₀ (M →ₗ[R] P)],
  IsComplemented m → Module.Finite R₀ (↥m →ₗ[R] P)
-- Lean.ResolveName
Lean.aliasExtension : Lean.SimplePersistentEnvExtension Lean.AliasEntry Lean.AliasState
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ord_eq_iff_associated : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] (x y : R),
  Ring.ord R x = Ring.ord R y ↔ Associated x y
-- Mathlib.RingTheory.Length
Module.length_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], Module.length R ↥⊥ = 0
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_pow : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f : Module.End R M) (n : ℕ),
  LinearMap.baseChange A (f ^ n) = LinearMap.baseChange A f ^ n
-- Init.Data.ByteArray.Lemmas
List.data_toByteArray : ∀ {l : List UInt8}, l.toByteArray.data = l.toArray
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The normalized expression of the 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Eval.Result.expr : Mathlib.Tactic.BicategoryLike.Eval.Result → Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasDerivAt.hasGradientAt' : ∀ {g : ℝ → ℝ} {g' u : ℝ}, HasDerivAt g g' u → HasGradientAt g g' u
-- Lean.Meta.TryThis
/-- Yields `(indent, column)` given a `FileMap` and a `Lean.Syntax.Range`, where `indent` is the number
of spaces by which the line that first includes `range` is initially indented, and `column` is the
column `range` starts at in that line.  -/
Lean.Meta.Tactic.TryThis.getIndentAndColumn : Lean.FileMap → Lean.Syntax.Range → ℕ × ℕ
-- Mathlib.Analysis.Analytic.Linear
/-- `id` is entire  -/
analyticOnNhd_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, AnalyticOnNhd 𝕜 (fun x => x) s
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instReprMCasesPat.repr : Lean.Parser.Tactic.MCasesPat → ℕ → Std.Format
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- The classes of `P.relation i` form a basis of `I ⧸ I ^ 2`.  -/
Algebra.SubmersivePresentation.basisCotangent : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) → Module.Basis σ S P.toExtension.Cotangent
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_precomp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.comp f g) ↔ HomotopicalAlgebra.WeakEquivalence g
-- Mathlib.Algebra.Group.Embedding
addRightEmbedding.congr_simp : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsRightCancelAdd G] (g g_1 : G),
  g = g_1 → addRightEmbedding g = addRightEmbedding g_1
-- Mathlib.Topology.Defs.Sequences
FrechetUrysohnSpace.closure_subset_seqClosure : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : FrechetUrysohnSpace X] (s : Set X), closure s ⊆ seqClosure s
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.linearIndependent_of_add_mem_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [CharZero R]
  [IsAddTorsionFree M] [P.IsReduced] {i j : ι},
  P.root i + P.root j ∈ Set.range ⇑P.root → LinearIndependent R ![P.root i, P.root j]
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a (p + b) = toIcoMod hp a b
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.directedAffineCover_X : ∀ (X : AlgebraicGeometry.Scheme) (U : ↑X.affineOpens), X.directedAffineCover.X U = ↑↑U
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddMonoidQuotient : {R : Type u_1} → [inst : AddMonoid R] → [inst_1 : Mul R] → (c : RingCon R) → AddMonoid c.Quotient
-- Mathlib.Topology.Instances.CantorSet
zero_mem_cantorSet : 0 ∈ cantorSet
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.epi_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j), CategoryTheory.Limits.IsZero (S.X₂.homology j) → CategoryTheory.Epi (hS.δ i j hij)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
_private.Mathlib.MeasureTheory.Integral.IntegrableOn.0.MeasureTheory.integrableAtFilter_smul_iff' : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {𝕜 : Type u_7} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 E] {f : α → E} {c : 𝕜},
  c ≠ 0 → (MeasureTheory.IntegrableAtFilter (c • f) l μ ↔ MeasureTheory.IntegrableAtFilter f l μ)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isLeftDescent_inv_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i