mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.comap_embedding_atBot : ∀ {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {e : β → γ},
  (∀ (b₁ b₂ : β), e b₂ ≤ e b₁ ↔ b₂ ≤ b₁) → (∀ (c : γ), ∃ b, e b ≤ c) → Filter.comap e Filter.atBot = Filter.atBot
-- Init.Data.NeZero
/-- A type-class version of `n ≠ 0`.   -/
NeZero : {R : Type u_1} → [Zero R] → R → Prop
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.mk.injEq : ∀ {M N : SemiNormedGrp} (hom' hom'_1 : NormedAddGroupHom M.carrier N.carrier),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Data.Vector.Range
Vector.snd_lt_add_of_mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {k : ℕ} {xs : Vector α n}, x ∈ xs.zipIdx k → x.2 < k + n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.p₂ r = r.g₂
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_int_ge_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, x ≤ ↑n
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.mk : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              [inst_3 : Ring A] →
                [inst_4 : Algebra R A] →
                  (bilin : M →ₗ[R] M →ₗ[R] A) →
                    (∀ (m : M), (bilin m) m = (algebraMap R A) (Q m)) →
                      (∀ (m₁ m₂ m₃ : M), (bilin m₁) m₂ * (bilin m₂) m₃ = Q m₂ • (bilin m₁) m₃) →
                        CliffordAlgebra.EvenHom Q A
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_comp_orderHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ) (g : α →+o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_5.eq_2 : ∀ {α : Type u_1} {P : α → Prop}
  (motive :
    (r : Option α) →
      (match r with
        | some a => P a
        | none => True) →
        Sort u_2)
  (x :
    match none with
    | some a => P a
    | none => True)
  (h_1 :
    (a : α) →
      (hp :
          match some a with
          | some a => P a
          | none => True) →
        motive (some a) hp)
  (h_2 :
    (x :
        match none with
        | some a => P a
        | none => True) →
      motive none x),
  (match none, x with
    | some a, hp => h_1 a hp
    | none, x => h_2 x) =
    h_2 x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.get?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] {k : α}
  (c : Std.DTreeMap.Internal.Cell α β (compare k)),
  c.get? =
    match h : c.inner with
    | none => none
    | some p => some (cast ⋯ p.snd)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instCanonicallyOrderedAddOfAddLeftMono : ∀ {ι : Type u_1} (α : ι → Type u_2) [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)]
  [∀ (i : ι), AddLeftMono (α i)], CanonicallyOrderedAdd (Π₀ (i : ι), α i)
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwise_iUnion₂_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → ((⋃ a ∈ s, a).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.false : Lean.Expr → Nat.EqResult✝
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams : Type
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableOn 𝕜 (A i) s) → DifferentiableOn 𝕜 (∑ i ∈ u, A i) s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piCongrLeft.eq_1 : ∀ {δ : Type u_4} {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] (f : δ ≃ δ'),
  MeasurableEquiv.piCongrLeft π f = { toEquiv := Equiv.piCongrLeft π f, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Lean.Meta.Basic
/-- This function is similar to `forallMetaTelescopeReducing`: Given `e` of the
form `forall ..xs, A`, this combinator will create a new metavariable for
each `x` in `xs` until it reaches an `x` whose type is defeq to `t`,
and instantiate `A` with these, while also reducing `A` if needed.
It uses `forallMetaTelescopeReducing`.

This function returns a triple `(mvs, bis, out)` where
- `mvs` is an array containing the new metavariables.
- `bis` is an array containing the binder infos for the `mvs`.
- `out` is `e` but instantiated with the `mvs`.
 -/
Lean.Meta.forallMetaTelescopeReducingUntilDefEq : Lean.Expr →
  Lean.Expr →
    optParam Lean.MetavarKind Lean.MetavarKind.natural →
      Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.of.injEq : ∀ (carrier : Type u_1) [str : PartialOrder carrier] (carrier_1 : Type u_1) (str_1 : PartialOrder carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_5 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_6 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_7 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6)
      [inst_8 : (r : ↑s) → AddCommMonoid (Nₚ r)] [inst_9 : (r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r)
      [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Surjective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) →
        Function.Surjective ⇑F
-- Batteries.CodeAction.Attr
Batteries.CodeAction.instInhabitedTacticCodeActionEntry.default : Batteries.CodeAction.TacticCodeActionEntry
-- Init.Data.NeZero
neZero_iff : ∀ {R : Type u_1} [inst : Zero R] {n : R}, NeZero n ↔ n ≠ 0
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.coeq_condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [inst_1 : CategoryTheory.IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : HasCardinalLT K κ)
  (k : K),
  CategoryTheory.CategoryStruct.comp (f k) (CategoryTheory.IsCardinalFiltered.coeqHom f hK) =
    CategoryTheory.IsCardinalFiltered.toCoeq f hK
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
sends `i : CostructuredArrow P.ι X` to `i.left.obj : C`. The coproduct
of this family is the source of the morphism `P.coproductFrom X`.  -/
CategoryTheory.ObjectProperty.coproductFromFamily : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) → (X : C) → CategoryTheory.CostructuredArrow P.ι X → C
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mk.inj : ∀ {R : Type u_1} {inst : LinearOrder R} {inst_1 : TopologicalSpace R} {toFun : R → ℝ} {mono' : Monotone toFun}
  {right_continuous' : ∀ (x : R), ContinuousWithinAt toFun (Set.Ici x) x} {toFun_1 : R → ℝ} {mono'_1 : Monotone toFun_1}
  {right_continuous'_1 : ∀ (x : R), ContinuousWithinAt toFun_1 (Set.Ici x) x},
  { toFun := toFun, mono' := mono', right_continuous' := right_continuous' } =
      { toFun := toFun_1, mono' := mono'_1, right_continuous' := right_continuous'_1 } →
    toFun = toFun_1
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a top element.  -/
BooleanSubalgebra.instTopCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → Top ↥L
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.instEpiAppOppositeNatπAsLimitCone : ∀ (S : LightProfinite) (i : ℕᵒᵖ), CategoryTheory.Epi (S.asLimitCone.π.app i)
-- Mathlib.MeasureTheory.Constructions.Pi
/-- A product of measures in `tprod α l`.  -/
MeasureTheory.Measure.tprod : {δ : Type u_4} →
  {X : δ → Type u_5} →
    [inst : (i : δ) → MeasurableSpace (X i)] →
      (l : List δ) → ((i : δ) → MeasureTheory.Measure (X i)) → MeasureTheory.Measure (List.TProd X l)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_add_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R (n + 2) = Polynomial.X * Polynomial.Chebyshev.C R (n + 1) - Polynomial.Chebyshev.C R n
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_ext : ∀ {A B : ProfiniteAddGrp.{u}} {f g : A ⟶ B}, ProfiniteAddGrp.Hom.hom f = ProfiniteAddGrp.Hom.hom g → f = g
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
notMem_nonZeroDivisorsLeft_iff : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] {x : M₀}, x ∉ nonZeroDivisorsLeft M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.id_apply : ∀ (X : CommGrpCat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.toArray_drop : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.drop n it).toArray = it.toArray.extract n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfToPiQuotient.eq_1 : ∀ {R : Type u} [inst : Ring R] {ι : Type u_1} (I : ι → Ideal R) [inst_1 : ∀ (i : ι), (I i).IsTwoSided],
  Ideal.quotientInfToPiQuotient I = Ideal.Quotient.lift (⨅ i, I i) (RingHom.pi fun i => Ideal.Quotient.mk (I i)) ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.mul_isCompl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousMul α] {s t : Set β},
  IsCompl s t → HasProd (f ∘ Subtype.val) a → HasProd (f ∘ Subtype.val) b → HasProd f (a * b)
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.dvd_map_of_isScalarTower : ∀ (A : Type u_3) (K : Type u_4) {R : Type u_5} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Ring R]
  [inst_3 : Algebra A K] [inst_4 : Algebra A R] [inst_5 : Algebra K R] [IsScalarTower A K R] (x : R),
  minpoly K x ∣ Polynomial.map (algebraMap A K) (minpoly A x)
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_2.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)))
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_3 t (Lean.Doc.Block.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_smul_of_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {r : R},
  r ∈ nonZeroDivisors R → ∀ {f : MvPolynomial σ R}, m.degree (r • f) = m.degree f
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.out : ∀ {R : Type uR} {A : Type uA} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : Algebra.FiniteType R A], ⊤.FG
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_laurent : ∀ {R : Type u} [inst : CommRing R] (r s : R) (f : RatFunc R) [inst_1 : IsDomain R],
  (RatFunc.laurent r) ((RatFunc.laurent s) f) = (RatFunc.laurent (r + s)) f
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app._auto_1)
  {Z : C} (h : (CategoryTheory.unopUnop C).obj ((CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso C n).inv.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop h)
-- Mathlib.MeasureTheory.Group.LIntegral
MeasurableEquiv.mulLeft.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g g_1 : G),
  g = g_1 → MeasurableEquiv.mulLeft g = MeasurableEquiv.mulLeft g_1
-- Mathlib.Order.Filter.Lift
Filter.lift_lift_same_le_lift : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set α → Filter β},
  (f.lift fun s => f.lift (g s)) ≤ f.lift fun s => g s s
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_toReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    ∀ (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤), (μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure
-- Mathlib.Order.BooleanSubalgebra
/-- Copy of a Boolean subalgebra with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
BooleanSubalgebra.copy : {α : Type u_2} → [inst : BooleanAlgebra α] → (L : BooleanSubalgebra α) → (s : Set α) → s = ↑L → BooleanSubalgebra α
-- Mathlib.ModelTheory.Order
FirstOrder.Language.partialOrderTheory.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.partialOrderTheory = insert FirstOrder.Language.leSymb.antisymmetric L.preorderTheory
-- Lean.ErrorExplanation
Lean.ErrorExplanation.mk.injEq : ∀ (doc : String) (metadata : Lean.ErrorExplanation.Metadata) (declLoc? : Option Lean.DeclarationLocation)
  (doc_1 : String) (metadata_1 : Lean.ErrorExplanation.Metadata) (declLoc?_1 : Option Lean.DeclarationLocation),
  ({ doc := doc, metadata := metadata, declLoc? := declLoc? } =
      { doc := doc_1, metadata := metadata_1, declLoc? := declLoc?_1 }) =
    (doc = doc_1 ∧ metadata = metadata_1 ∧ declLoc? = declLoc?_1)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_sum_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {α : Type u_3} {s : Finset α}
  {f : α → MvPolynomial σ R},
  m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x => m.toWithBotSyn (m.withBotDegree (f x))
-- Mathlib.Order.Category.DistLat
_private.Mathlib.Order.Category.DistLat.0.DistLat.Hom.mk.inj : ∀ {X Y : DistLat} {hom' hom'_1 : LatticeHom ↑X ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Topology.Algebra.Valued.WithVal
IsIntegralClosure.equiv.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (A' : Type u_4)
  [inst_6 : CommRing A'] [inst_7 : Algebra A' B] [inst_8 : IsIntegralClosure A' R B] [inst_9 : Algebra R A]
  [inst_10 : Algebra R A'] [inst_11 : IsScalarTower R A B] [inst_12 : IsScalarTower R A' B],
  IsIntegralClosure.equiv R A B A' = IsIntegralClosure.equiv R A B A'
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- If `q` is a prime of `R'` lying over `p`, a prime of `R`, such that `κ(q) = κ(p)`, then
the fiber of `R' → R' ⊗[R] S` over `q` is in bijection with the fiber of `R → S` over `p`.  -/
Ideal.fiberIsoOfBijectiveResidueField : {R : Type u_1} →
  {R' : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing R'] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R R'] →
              [inst_4 : Algebra R S] →
                {p : Ideal R} →
                  {q : Ideal R'} →
                    [inst_5 : p.IsPrime] →
                      [inst_6 : q.IsPrime] →
                        [inst_7 : q.LiesOver p] →
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) →
                            ↑(q.primesOver (TensorProduct R R' S)) ≃o ↑(p.primesOver S)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.add_iInf_le_iInf_add : ∀ {α : Type u_2} {u v : α → EReal}, (⨅ x, u x) + ⨅ x, v x ≤ ⨅ x, (u + v) x
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Real.fromBinary_surjective : Function.Surjective Real.fromBinary
-- Mathlib.ModelTheory.Definability
/-- The preimage of a constant under a definable function is definable.  -/
Set.DefinableFun.ofPred_eq_const : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M},
  Set.DefinableFun L A f → ∀ {a : M}, a ∈ A → A.Definable L {v | f v = a}
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instDecidableMem : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → {m : Std.ExtDTreeMap α β cmp} → {a : α} → Decidable (a ∈ m)
-- Std.Data.DHashMap.RawDef
/-- Dependent hash maps without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `DHashMap`
over `DHashMap.Raw`. Lemmas about the operations on `Std.Data.DHashMap.Raw` are available in the
module `Std.Data.DHashMap.RawLemmas`.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.
 -/
Std.DHashMap.Raw : (α : Type u) → (α → Type v) → Type (max u v)
-- Mathlib.Algebra.Ring.ULift
ULift.distrib : {R : Type u} → [Distrib R] → Distrib (ULift.{u_1, u} R)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insertNew_eq_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α} {v : α},
  RBTree.RBNode.zoom (cmp v) t = (RBTree.RBNode.nil, path) → path.insertNew v = (RBTree.RBNode.insert cmp t v).setBlack
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.GroupTheory.Torsion
/-- Torsion additive monoids are really additive groups.  -/
IsAddTorsion.addGroup : {G : Type u_1} → [inst : AddMonoid G] → IsAddTorsion G → AddGroup G
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂),
  (CategoryTheory.Monad.algebraEquivOfIsoMonads h).unitIso =
    CategoryTheory.Monad.algebraFunctorOfMonadHomId.symm ≪≫
      CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.hom h.inv
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Icc' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  c ≤ b → a ≤ d → Set.Icc a b ∪ Set.Icc c d = Set.Icc (min a c) (max b d)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey! t.minKey! = t.minKey!
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_sub_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g - h) μ μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_apply_of_contains_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF)
  (h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true),
  (f (t.getKey k ⋯) (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)).isSome = true
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- Upgrade a bialgebra to a Hopf algebra by specifying a convolution inverse of the identity.  -/
HopfAlgebra.ofConvInverse : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Bialgebra R A] →
          (antipode : A →ₗ[R] A) →
            WithConv.toConv antipode * WithConv.toConv LinearMap.id = 1 →
              WithConv.toConv LinearMap.id * WithConv.toConv antipode = 1 → HopfAlgebra R A
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_left' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.measure_condCDF_univ : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  (ProbabilityTheory.condCDF ρ a).measure Set.univ = 1
-- Mathlib.Data.Tree.Get
/-- Retrieves an element from the tree, or the provided default value
if the index is invalid. See `BinaryTree.get`.  -/
BinaryTree.getOrElse : {α : Type u_1} → PosNum → BinaryTree α → α → α
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_lt : ∀ (x : Int8), x.toNatClampNeg < 2 ^ 7