mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Inverse
/-- The inverse `1/f` of a multivariable power series `f` over a field  -/
MvPowerSeries.inv : {σ : Type u_1} → {k : Type u_3} → [Field k] → MvPowerSeries σ k → MvPowerSeries σ k
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.append.inj : ∀ {l r w : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr l} {rhs : Std.Tactic.BVDecide.BVExpr r} {h : w = l + r} {l_1 r_1 : ℕ}
  {lhs_1 : Std.Tactic.BVDecide.BVExpr l_1} {rhs_1 : Std.Tactic.BVDecide.BVExpr r_1} {h_1 : w = l_1 + r_1},
  lhs.append rhs h = lhs_1.append rhs_1 h_1 → l = l_1 ∧ r = r_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instNoSuffixPatternModelForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.NoSuffixPatternModel p
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_simple : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.infNndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → ∀ {s : Set α}, Measurable fun x => Metric.infNndist (f x) s
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv_symm_apply : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B) (x : L),
  (IsFractionRing.semilinearEquivOfRingEquiv K L f).symm x = (IsFractionRing.ringEquivOfRingEquiv f).symm x
-- Mathlib.FieldTheory.SeparableClosure
separableClosure_le_separableClosure_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra K E] [inst_6 : IsScalarTower F K E] {L : IntermediateField F E},
  IntermediateField.restrictScalars F (separableClosure (↥L) E) ≤
      IntermediateField.restrictScalars F (separableClosure K E) ↔
    L ≤ IntermediateField.restrictScalars F (separableClosure K E)
-- Init.Data.Vector.Algebra
Vector.instAddCommMonoid : {α : Type u_1} → {n : ℕ} → [Lean.Grind.AddCommMonoid α] → Lean.Grind.AddCommMonoid (Vector α n)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.homEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) (Y : D),
  adj.homEquiv X Y =
    { toFun := fun f => CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f),
      invFun := fun g => CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y), left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mk.injEq : ∀ {X : Type u_3} [inst : MetricSpace X] (carrier : Set X) (packingRadius : NNReal)
  (packingRadius_pos : 0 < packingRadius) (isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier)
  (coveringRadius : NNReal) (coveringRadius_pos : 0 < coveringRadius)
  (isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier) (carrier_1 : Set X)
  (packingRadius_1 : NNReal) (packingRadius_pos_1 : 0 < packingRadius_1)
  (isSeparated_packingRadius_1 : Metric.IsSeparated (↑packingRadius_1) carrier_1) (coveringRadius_1 : NNReal)
  (coveringRadius_pos_1 : 0 < coveringRadius_1)
  (isCover_coveringRadius_1 : Metric.IsCover coveringRadius_1 Set.univ carrier_1),
  ({ carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
        isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
        coveringRadius_pos := coveringRadius_pos, isCover_coveringRadius := isCover_coveringRadius } =
      { carrier := carrier_1, packingRadius := packingRadius_1, packingRadius_pos := packingRadius_pos_1,
        isSeparated_packingRadius := isSeparated_packingRadius_1, coveringRadius := coveringRadius_1,
        coveringRadius_pos := coveringRadius_pos_1, isCover_coveringRadius := isCover_coveringRadius_1 }) =
    (carrier = carrier_1 ∧ packingRadius = packingRadius_1 ∧ coveringRadius = coveringRadius_1)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.instLieRingModuleSubtypeMemLieSubmodule : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [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] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      (χ : L → R) →
                        [LieModule.LinearWeights R L M] → LieRingModule L ↥(LieModule.shiftedGenWeightSpace R L M χ)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_Ici_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {a : α} {f : β → ↑(Set.Ici a)} {l : Filter β},
  Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atTop
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra of a Lie algebra is submodule that is closed under the Lie bracket.
This is a sufficient condition for the subset itself to form a Lie algebra.  -/
LieSubalgebra : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type v
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_sup : ∀ {G : Type u_2} [inst : Group G] (S₁ S₂ : Subgroup Gᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_parts_or_eq_sdiff_of_mem_extendOfLE : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a ≤ b) {p : α}, p ∈ (P.extendOfLE hab).parts → p ∈ P.parts ∨ p = b \ a
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_fibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.Fibration f],
  HomotopicalAlgebra.fibrations C f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km fallback : α},
  t.min? = some km → t.getD km fallback = km
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
counit of the adjunction `adj`, then we get a formula for `e₁.hom` in terms of `e₂`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityCounit_left : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityCounit adj e₁ e₂ →
    ∀ (X : C),
      e₁.hom.app X =
        CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X)))
          (CategoryTheory.CategoryStruct.comp (F.map (e₂.inv.app (F.obj X)))
            (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))
-- Mathlib.Data.Stream.Defs
/-- `a ∈ s` means that `a = Stream'.get n s` for some `n`.  -/
Stream'.instMembership : {α : Type u} → Membership α (Stream' α)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (m : Std.DTreeMap.Internal.Impl α β) →
      (Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true) → Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hm :
    Std.DTreeMap.Internal.Impl.contains' k l = true →
      Std.DTreeMap.Internal.Impl.contains' k (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) = true)
  (h_1 :
    (hm :
        Std.DTreeMap.Internal.Impl.contains' k l = true →
          Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = true) →
      motive Std.DTreeMap.Internal.Impl.leaf hm)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l_2 r : Std.DTreeMap.Internal.Impl α β) →
            (hm :
                Std.DTreeMap.Internal.Impl.contains' k l = true →
                  Std.DTreeMap.Internal.Impl.contains' k (Std.DTreeMap.Internal.Impl.inner size k' v' l_2 r) = true) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l_2 r) hm),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r, hm with
    | Std.DTreeMap.Internal.Impl.leaf, hm => h_1 hm
    | Std.DTreeMap.Internal.Impl.inner size k' v' l_2 r, hm => h_2 size k' v' l_2 r hm) =
    h_2 size k' v' l_1 r hm
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.comap_map_eq_self_of_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {f : A →ₐ[R] B},
  Function.Injective ⇑f → ∀ (S : Subalgebra R A), Subalgebra.comap f (Subalgebra.map f S) = S
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_roi : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (List.drop (lo + 1) xs).toArray
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β}, (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.compare_getKey_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (h' : k ∈ t), cmp (t.getKey k h') k = Ordering.eq
-- Init.Tactics
/-- The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
empty pattern match, closing the goal if the introduced pattern is impossible.
 -/
Lean.Parser.Tactic.tacticNofun : Lean.ParserDescr
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- The identity isometric equivalence between a bilinear form and itself.  -/
LinearMap.BilinForm.IsometryEquiv.refl : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (B : LinearMap.BilinForm R M) → B.IsometryEquiv B
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiff.comp_contMDiffAt : ∀ {𝕜 : 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_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {x : M},
  ContDiff 𝕜 n g →
    ContMDiffAt I (modelWithCornersSelf 𝕜 F) n f x → ContMDiffAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) x
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpStep : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Init.Core
Task.pure.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (get : α), sizeOf { get := get } = 1 + sizeOf get
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.mk.inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} {inst : L.Structure M} {inst_1 : L.Structure N} {toEquiv : M ≃ N}
  {map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam}
  {map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam}
  {toEquiv_1 : M ≃ N}
  {map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv_1.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv_1.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam}
  {map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv_1.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam},
  { toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } =
      { toEquiv := toEquiv_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Order.Filter.Map
Filter.pure_seq_eq_map : ∀ {α : Type u_1} {β : Type u_2} (g : α → β) (f : Filter α), (pure g).seq f = Filter.map g f
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.snd_pow : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ℕ),
  (x ^ n).snd = GradedMonoid.GMonoid.gnpow n x.snd
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `-a`,
such that `norm_num` successfully recognises `a`.  -/
Mathlib.Meta.NormNum.evalNeg : Mathlib.Meta.NormNum.NormNumExt
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.modifyDiag : (Lean.Meta.Simp.Diagnostics → Lean.Meta.Simp.Diagnostics) → Lean.Meta.SimpM Unit
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context : Type
-- Mathlib.Data.List.Duplicate
List.Duplicate.below.cons_duplicate : ∀ {α : Type u_1} {x : α} {motive : (a : List α) → List.Duplicate x a → Prop} {y : α} {l : List α}
  (a : List.Duplicate x l), List.Duplicate.below a → motive l a → List.Duplicate.below ⋯
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.forgetAdjStar_counit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] (X Y : C),
  (CategoryTheory.Over.forgetAdjStar X).counit.app Y = CategoryTheory.Limits.prod.snd
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.div_C_mul : ∀ {R : Type u} {a : R} [inst : Field R] {p q : Polynomial R}, p / (Polynomial.C a * q) = Polynomial.C a⁻¹ * (p / q)
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The conjugate of the golden ratio is irrational.  -/
Real.goldenConj_irrational : Irrational Real.goldenConj
-- Mathlib.MeasureTheory.Group.Measure
/-- A measure is invariant under inversion if `μ⁻¹ = μ`. Equivalently, this means that for all
measurable `A` we have `μ (A⁻¹) = μ A`, where `A⁻¹` is the pointwise inverse of `A`.  -/
MeasureTheory.Measure.IsInvInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Inv G] → MeasureTheory.Measure G → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_eq_castSucc_iff : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (y : Fin (n + 1)),
  SimplexCategory.II.map' f x = y.castSucc ↔ x ≤ (f y).castSucc ∧ ∀ i < y, (f i).castSucc < x
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The continuous `ℚ`-algebra isomorphism between `v.adicCompletion ℚ` and `ℚ_[primesEquiv v]`.  -/
Rat.HeightOneSpectrum.adicCompletion.padicEquiv : {R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : Algebra R ℚ] →
      [inst_2 : IsIntegralClosure R ℤ ℚ] →
        [inst_3 : IsDedekindDomain R] →
          [inst_4 : IsFractionRing R ℚ] →
            (v : IsDedekindDomain.HeightOneSpectrum R) →
              IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ v ≃A[ℚ] ℚ_[↑(Rat.HeightOneSpectrum.primesEquiv v)]
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `N` is flat, `M` is contained in `i(R)`, where `i : R → S` is the structure map,
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_left_le_one_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  M ≤ 1 → ∀ [Module.Flat R ↥N], M.LinearDisjoint N
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
/-- Basis vectors are eigenvectors of associated diagonal linear operator.  -/
hasEigenvector_toLin_diagonal : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [Nontrivial R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] (d : n → R) (i : n) (b : Module.Basis n R M),
  Module.End.HasEigenvector ((Matrix.toLin b b) (Matrix.diagonal d)) (d i) (b i)
-- Mathlib.Topology.UniformSpace.CompareReals
/-- Type wrapper around ℚ to make sure the absolute value uniform space instance is picked up
instead of the metric space one. We proved in `Rat.uniformSpace_eq` that they are equal,
but they are not definitionaly equal, so it would confuse the type class system (and probably
also human readers).  -/
CompareReals.Q : Type
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearMap.precompUniformConvergenceCLM_apply : ∀ {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_9} {F : Type u_10} (G : Type u_11) [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G] (𝔖 : Set (Set E))
  (𝔗 : Set (Set F)) [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F)
  (hL : Set.MapsTo (fun x => ⇑L '' x) 𝔖 𝔗) (f : UniformConvergenceCLM τ G 𝔗),
  (ContinuousLinearMap.precompUniformConvergenceCLM G 𝔖 𝔗 L hL) f = f ∘SL L
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.right = Y.right
-- Mathlib.LinearAlgebra.Complex.Orientation
/-- The standard orientation on `ℂ`.  -/
Complex.orientation : Orientation ℝ ℂ (Fin 2)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.mono_homologyMap_of_mono_opcyclesMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [CategoryTheory.Mono (CategoryTheory.ShortComplex.opcyclesMap φ)],
  CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.projRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {c₁ c₂ : α × β}
  (p : Path.Homotopic.Quotient c₁ c₂), Path.Homotopic.projRight p = p.map { toFun := Prod.snd, continuous_toFun := ⋯ }
-- Lean.Elab.Term.TermElabM
/-- A name `n` is only eligible to be an auto implicit name if `autoBoundImplicitForbidden n = false`.
We use this predicate to disallow `f` to be considered an auto implicit name in a definition such
as
```
def f : f → Bool := fun _ => true
```
 -/
Lean.Elab.Term.Context.autoBoundImplicitForbidden : Lean.Elab.Term.Context → Lean.Name → Bool
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.coinduct : ∀ (m : Type w → Type w') (β : Type w) [inst : Monad m] [inst_1 : LawfulMonad m]
  (pred : Std.BundledIterM m β → Std.BundledIterM m β → Prop),
  (∀ (ita itb : Std.BundledIterM m β),
      pred ita itb →
        Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk pred)) ita.step =
          Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk pred)) itb.step) →
    ∀ (ita itb : Std.BundledIterM m β), pred ita itb → Std.BundledIterM.Equiv m β ita itb
-- Init.Data.List.Basic
List.of_concat_eq_concat : ∀ {α : Type u} {as bs : List α} {a b : α}, as.concat a = bs.concat b → as = bs ∧ a = b
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_mono : Monotone Nat.primesLE
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- To prove something for an `Lp` function a.e. strongly measurable with respect to a
sub-σ-algebra `m` in a normed space, it suffices to show that
* the property holds for (multiples of) characteristic functions which are measurable w.r.t. `m`;
* is closed under addition;
* the set of functions in `Lp` strongly measurable w.r.t. `m` for which the property holds is
  closed.
 -/
MeasureTheory.Lp.induction_stronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F] (hm : m ≤ m0),
  p ≠ ⊤ →
    ∀ (P : ↥(MeasureTheory.Lp F p μ) → Prop),
      (∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
          P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)) →
        (∀ ⦃f g : α → F⦄ (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
            MeasureTheory.StronglyMeasurable f →
              MeasureTheory.StronglyMeasurable g →
                Disjoint (Function.support f) (Function.support g) →
                  P (MeasureTheory.MemLp.toLp f hf) →
                    P (MeasureTheory.MemLp.toLp g hg) →
                      P (MeasureTheory.MemLp.toLp f hf + MeasureTheory.MemLp.toLp g hg)) →
          IsClosed {f | P ↑f} → ∀ (f : ↥(MeasureTheory.Lp F p μ)), MeasureTheory.AEStronglyMeasurable (↑↑f) μ → P f
-- Mathlib.Data.EReal.Operations
EReal.recENNReal.eq_1 : ∀ {motive : EReal → Sort u_1} (coe : (x : ENNReal) → motive ↑x) (neg_coe : (x : ENNReal) → 0 < x → motive (-↑x))
  (x : EReal),
  EReal.recENNReal coe neg_coe x =
    if hx : 0 ≤ x then ⋯ ▸ coe x.toENNReal
    else Eq.rec (motive := fun x_1 h => 0 < (-x).toENNReal → motive x_1) (neg_coe (-x).toENNReal) ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.nnnorm_up : ∀ {E : Type u_2} [inst : NNNorm E] (x : E), ‖{ down := x }‖₊ = ‖x‖₊
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.cech_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) (n : SimplexCategoryᵒᵖ),
  U.cech.obj n = U.power (CategoryTheory.ToType (Opposite.unop n))
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version in a general ring
with summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
see `hasSum_coe_mul_geometric_of_norm_lt_one`.  -/
hasSum_coe_mul_geometric_of_norm_lt_one' : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] {x : R},
  ‖x‖ < 1 → HasSum (fun n => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)