mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Connected.PathConnected
joinedIn_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, JoinedIn Set.univ x y ↔ Joined x y
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` almost
everywhere supported on `s` is `m`-ae-strongly-measurable, then `f` is also
`m₂`-ae-strongly-measurable.  -/
MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m : MeasurableSpace α} {f : α → β}
  {m' m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_1 : Zero β],
  m ≤ m₀ →
    ∀ {s : Set α},
      MeasurableSet s →
        (∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) →
          MeasureTheory.AEStronglyMeasurable f μ → f =ᵐ[μ.restrict sᶜ] 0 → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_lt_add : ∀ {κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}}, κ₁ < κ₂ → μ₁ < μ₂ → κ₁ + μ₁ < κ₂ + μ₂
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.checkTraceOption.go : Std.HashSet Lean.Name → Lean.Options → Lean.Name → Bool
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.sub_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, StrictConcaveOn 𝕜 s f → ConvexOn 𝕜 s g → StrictConcaveOn 𝕜 s (f - g)
-- Mathlib.NumberTheory.Fermat
Nat.fermat_primeFactors_one_lt : ∀ (n p : ℕ), 1 < n → Nat.Prime p → p ∣ n.fermatNumber → ∃ k, p = k * 2 ^ (n + 2) + 1
-- Mathlib.Data.List.Destutter
/-- For an injective function `f`, `destutter' (·≠·)` commutes with `map f`.  -/
List.map_destutter_ne : ∀ {α : Type u_1} {β : Type u_2} (l : List α) {f : α → β},
  Function.Injective f →
    ∀ [inst : DecidableEq α] [inst_1 : DecidableEq β],
      List.map f (List.destutter (fun x1 x2 => x1 ≠ x2) l) = List.destutter (fun x1 x2 => x1 ≠ x2) (List.map f l)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
/-- A morphism of schemes `f : X ⟶ Y` is universally open if the base change `X ×[Y] Y' ⟶ Y'`
along any morphism `Y' ⟶ Y` is (topologically) an open map.
 -/
AlgebraicGeometry.UniversallyOpen : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Lean.Elab.PreDefinition.WF.Preprocess
/-- Transforms non-Prop `have`s to `let`s, so that the values can be used in GuessLex and decreasing-by proofs.
These `have`s may have been introduced by `simp`, which converts `let`s to `have`s.
 -/
_private.Lean.Elab.PreDefinition.WF.Preprocess.0.Lean.Elab.WF.nonPropHaveToLet : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_iff_smul_rearrangement`.

---

Two functions monovary iff the rearrangement inequality holds.  -/
MonovaryOn.smul_add_smul_le_smul_add_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsMulLeftInvariant.comap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] {H : Type u_3} [inst_3 : Group H]
  {mH : MeasurableSpace H} [MeasurableMul H] (μ : MeasureTheory.Measure H) [μ.IsMulLeftInvariant] {f : G →* H},
  MeasurableEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsMulLeftInvariant
-- Init.Data.Vector.Basic
Vector.zipIdx : {α : Type u_1} → {n : ℕ} → Vector α n → optParam ℕ 0 → Vector (α × ℕ) n
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_ite : ∀ {α : Type u_1} [inst : DecidableEq α] (s s' : Finset α) (P : Prop) [inst_1 : Decidable P],
  s ∩ s' ⊆ if P then s else s'
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.NeBot.eq_pure_iff : ∀ {α : Type u} {f : Filter α}, f.NeBot → ∀ {x : α}, f = pure x ↔ {x} ∈ f
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.inv : ∀ {R : Type u_1} [inst : Group R] [inst_1 : StarMul R] {x : R}, IsSelfAdjoint x → IsSelfAdjoint x⁻¹
-- Lean.Parser.Term
/-- `unop% f a` elaborates `f a` as a unary operation using the type propagation protocol in `Lean.Elab.Extra`.  -/
Lean.Parser.Term.unop : Lean.Parser.Parser
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_def : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S),
  p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a_1 : a ⟶ b) (x_1 : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).map a_1).toFunctor.obj x_1 = CategoryTheory.CategoryStruct.comp a_1.unop x_1
-- Mathlib.Data.Nat.Nth
Nat.nth_ne_zero_anti : ∀ {p : ℕ → Prop}, ¬p 0 → ∀ {a b : ℕ}, a ≤ b → Nat.nth p b ≠ 0 → Nat.nth p a ≠ 0
-- Aesop.Forward.SlotIndex
Aesop.instDecidableRelSlotIndexLe : DecidableRel fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.divBy_apply : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : ↥S) (p : LocalizedModule S M),
  (LocalizedModule.divBy s) p = p.liftOn (fun p => LocalizedModule.mk p.1 (p.2 * s)) ⋯
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
-- Lean.Elab.Match
/-- Update `indices` by including any free variable `x` s.t.
- Type of some `discr` depends on `x`.
- Type of `x` depends on some free variable in `indices`.

If we don't include these extra variables in indices, then
`updateMatchType` will generate a type incorrect term.
For example, suppose `discr` contains `h : @HEq α a α b`, and
`indices` is `#[α, b]`, and `matchType` is `@HEq α a α b → B`.
`updateMatchType indices matchType` produces the type
`(α' : Type) → (b : α') → @HEq α' a α' b → B` which is type incorrect
because we have `a : α`.
The method `collectDeps` will include `a` into `indices`.

This method does not handle dependencies among non-free variables.
We rely on the type checking method `check` at `updateMatchType`.

Remark: `indices : Array Expr` does not need to be an array anymore.
We should cleanup this code, and use `index : Expr` instead.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.collectDeps : Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.builderParser.go : {α : Type} →
  Std.Time.FormatConfig →
    (format : Std.Time.FormatString) → Std.Time.FormatType (Option α) format → Std.Internal.Parsec.String.Parser α
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.lift_rank_bot_le_lift_rank_of_isScalarTower : ∀ (R : Type u) (R' : Type u') [inst : Semiring R] [inst_1 : Semiring R'] (T : Type w) [inst_2 : Module R R']
  [inst_3 : NonAssocSemiring T] [inst_4 : Module R T] [inst_5 : Module R' T] [IsScalarTower R' T T] [FaithfulSMul R' T]
  [IsScalarTower R R' T], Cardinal.lift.{w, u'} (Module.rank R R') ≤ Cardinal.lift.{u', w} (Module.rank R T)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β], ⇑0 = 0
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.right_triangle : ∀ {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),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft adj.unit)
      (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight adj.counit G)) =
    CategoryTheory.CategoryStruct.comp G.rightUnitor.hom G.leftUnitor.inv
-- Mathlib.Order.CompleteLattice.Basic
eq_singleton_bot_of_sSup_eq_bot_of_nonempty : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⊥ → s.Nonempty → s = {⊥}
-- Init.Data.UInt.Bitwise
UInt32.and_eq_neg_one_iff : ∀ {a b : UInt32}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Equivalence.toIsoCat_inverse : ∀ {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] (e : C ≌ D) (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X)
  (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y)
  (k :
    autoParam (∀ (X : C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Equivalence.toIsoCat._auto_1)
  (k' :
    autoParam (∀ (Y : D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯)
      CategoryTheory.Equivalence.toIsoCat._auto_3),
  (e.toIsoCat h h' k k').inverse = e.inverse
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.listM : {m : Type u → Type u} → MLList.Spec✝ m → Type u → Type u
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.gcd_dvd_const : ∀ {ctx : Int.Internal.Linear.Context} {p : Int.Internal.Linear.Poly} {k : ℤ},
  k ∣ Int.Internal.Linear.Poly.denote ctx p → p.gcdCoeffs k ∣ p.getConst
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_mem_toZFSet_iff : ∀ {a b : Ordinal.{u_1}}, a.toZFSet ∈ b.toZFSet ↔ a < b
-- Lean.Environment
Lean.instOrdOLeanLevel.ord : Lean.OLeanLevel → Lean.OLeanLevel → Ordering
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.isComplete_map_iff : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [inst_6 : RingHomSurjective σ₁₂] {p : Submodule R E},
  IsComplete ↑(Submodule.map f.toLinearMap p) ↔ IsComplete ↑p
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α} {h : a ∈ m},
  Std.ExtDHashMap.Const.get m a h = Std.ExtDHashMap.Const.get! m a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β},
  e = e' ↔ (∀ (x : α), ↑e x = ↑e' x) ∧ (∀ (x : β), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source
-- Std.Time.Date.Unit.Weekday
Std.Time.instInhabitedWeekday.default : Std.Time.Weekday
-- Mathlib.Data.Fintype.Order
Bool.completeLinearOrder : CompleteLinearOrder Bool
-- Lean.Parser.Extension
Lean.Parser.ensureBinaryParserAlias : Lean.Name → IO Unit
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.result : Lean.CollectLevelMVars.State → Array Lean.LMVarId
-- Mathlib.Topology.Sets.Compacts
/-- An open relatively compact neighbourhood of `K` induces a compact neighbourhood by taking
the closure
 -/
TopologicalSpace.Compacts.openRcNhdsToCompactNhds : {α : Type u_1} → [inst : TopologicalSpace α] → (K : TopologicalSpace.Compacts α) → ↑K.openRcNhds → ↑K.compactNhds
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Spec_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.Scheme.Spec.map f = AlgebraicGeometry.Spec.map f.unop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_lt_pow_right' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] {a : M} {n m : ℕ},
  1 < a → n < m → a ^ n < a ^ m
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.orbit_eq_carrier_conjClasses : ∀ {G : Type u_3} [inst : Group G] (g : G), MulAction.orbit (ConjAct G) g = (ConjClasses.mk g).carrier
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.map_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)
  [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T)
  [inst_2 : CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) [CategoryTheory.IsIso i₁]
  [CategoryTheory.IsIso i₂] [CategoryTheory.IsIso i₃],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf : ∀ (R : CommRingCat), (AlgebraicGeometry.Spec.locallyRingedSpaceObj R).sheaf = AlgebraicGeometry.Spec.structureSheaf ↑R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Lean.Parser.Command
Lean.Parser.Command.optionValue : Lean.Parser.Parser
-- Init.Data.List.Impl
List.findSomeRev?.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → Option β) (a : α) (as : List α),
  List.findSomeRev? f (a :: as) =
    match List.findSomeRev? f as with
    | some b => some b
    | none => f a
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_div_eq_nnnorm_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E) {y : E}, ‖y‖₊ = 0 → ‖x / y‖₊ = ‖x‖₊
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7}
  [inst_1 : NormedAddCommGroup G] [inst_2 : PartialOrder G] {f : ↥(MeasureTheory.Lp.simpleFunc G p μ)},
  0 ≤ f → ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ⇑f'
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.lt : Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {fallback : α},
  (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (a : E.I₀),
  (CategoryTheory.PreOneHypercover.Hom.id E).s₀ a = a
-- Mathlib.Topology.Order.CountableSeparating
Filter.EventuallyEq.of_forall_eventually_lt_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X},
  (∀ (x : X), ∀ᶠ (a : α) in l, f a < x ↔ g a < x) → f =ᶠ[l] g
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The canonical bilinear map `M → N → M ⊗[R] N`.  -/
TensorProduct.mk : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → M →ₗ[R] N →ₗ[R] TensorProduct R M N
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.trans : ∀ {n a b c : ℕ}, a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n]
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_rfl_rfl : ∀ {U : Type u_1} [inst : Quiver U] {u v : U} (p : Quiver.Path u v), Quiver.Path.cast ⋯ ⋯ p = p
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  IsSymmetricAlgebra f = Function.Bijective ⇑(SymmetricAlgebra.lift f)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The diagram
```
ℤ_[p]  -------->  (primesEquiv.symm p).adicCompletionIntegers ℚ
   |                          |
   |                          |
   v                          v
ℚ_[p]  -------->  (primesEquiv.symm p).adicCompletion ℚ
```
commutes.  -/
PadicInt.coe_adicCompletionIntegersEquiv_apply : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  [inst_4 : IsIntegralClosure R ℤ ℚ] (p : Nat.Primes) (x : ℤ_[↑p]),
  ↑((PadicInt.adicCompletionIntegersEquiv R p) x) = (Padic.adicCompletionEquiv R p) ↑x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddGroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : AddGroup G],
  Filter.Germ.instAddGroup = { toSubNegMonoid := Filter.Germ.subNegMonoid, neg_add_cancel := ⋯ }
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isBounded_of_image2_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] {f : α → β → γ} {K₂ : NNReal},
  (∀ (a : α), AntilipschitzWith K₂ (f a)) →
    ∀ {s : Set α} {t : Set β}, Bornology.IsBounded (Set.image2 f s t) → Bornology.IsBounded s ∨ Bornology.IsBounded t
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.tuple.injEq : ∀ (ref : Lean.Syntax) (a : List Lean.Elab.Tactic.RCases.RCasesPatt) (ref_1 : Lean.Syntax)
  (a_1 : List Lean.Elab.Tactic.RCases.RCasesPatt),
  (Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref a = Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref_1 a_1) =
    (ref = ref_1 ∧ a = a_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a left homology data for `S₂` induces a left homology data for `S₁` with
the same `K` and `H` fields. The inverse construction is `ofEpiOfIsIsoOfMono`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₂.LeftHomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₁.LeftHomologyData
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) {Z : C}
  (h : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) h) =
    h
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isBigOTVS_iff_isBigO`. -/
Asymptotics.IsBigOTVS.isBigO : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =O[𝕜; l] g → f =O[l] g
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_mem_mul_rev : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {M N : Submodule R A} {m n : A}, m ∈ M → n ∈ N → n * m ∈ M * N
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.counit_comul_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.ComonObj M] {Z : C} (f : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.ae_covers : ∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1},
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The natural isomorphism `F(A ⨯ -) ≅ FA ⨯ F-`, provided each `prodComparison F A B` is an
isomorphism (as `B` changes).
 -/
CategoryTheory.Limits.prodComparisonNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] →
            [inst_3 : CategoryTheory.Limits.HasBinaryProducts D] →
              (A : C) →
                [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] →
                  (CategoryTheory.Limits.prod.functor.obj A).comp F ≅
                    F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- A partial Hahn embedding always extends `baseEmbedding`.  -/
HahnEmbedding.IsPartial.baseEmbedding_le : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)}, HahnEmbedding.IsPartial seed f → seed.baseEmbedding ≤ f
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {p r : α}, (∀ {m : α}, m ∈ UniqueFactorizationMonoid.normalizedFactors r → m = p) → r ≠ 0 → ∃ i, Associated (p ^ i) r
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  ((Matrix.toLinearMap₂' R) M).SeparatingLeft ↔ ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingLeft
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.child : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    (x : P.last.M) →
      (a : P.A) →
        (f : P.last.B a → P.last.M) →
          x.dest = ⟨a, f⟩ → (j : P.last.B a) → (i : Fin2 n) → MvPFunctor.M.Path P (f j) i → MvPFunctor.M.Path P x i
-- Init.Core
/-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic.  -/
LawfulBEq.eq_of_beq : ∀ {α : Type u} {inst : BEq α} [self : LawfulBEq α] {a b : α}, (a == b) = true → a = b
-- Mathlib.Data.NNRat.Lemmas
NNRat.mul_num : ∀ (q₁ q₂ : ℚ≥0), (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGE? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option (α × β)