mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.inducedMeasure.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B],
  H.inducedMeasure μA μC = RealRMK.rieszMeasure { toLinearMap := H.integrate μA μC, monotone' := ⋯ }
-- Mathlib.Data.Stream.Defs
/-- Interpret a nonempty list as a cyclic stream.  -/
Stream'.cycle : {α : Type u} → (l : List α) → l ≠ [] → Stream' α
-- Lean.Elab.Tactic.Grind.Anchor
Lean.Elab.Tactic.Grind.elabAnchorRef : Lean.TSyntax `hexnum → Lean.CoreM Lean.Meta.Grind.AnchorRef
-- Init.Data.Vector.Lemmas
Vector.forall_zero_iff : ∀ {α : Type u_1} {P : Vector α 0 → Prop}, (∀ (xs : Vector α 0), P xs) ↔ P #v[]
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi (Std.Slice.size xs) - lo
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- The stabilizer of a set acts on that set.  -/
instAddActionSubtypeMemAddSubgroupStabilizerSetElem : (G : Type u_1) →
  [inst : AddGroup G] →
    (α : Type u_2) → [inst_1 : AddAction G α] → (s : Set α) → AddAction ↥(AddAction.stabilizer G s) ↑s
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_inv_hom_id_eval_assoc : ∀ {C : Type u_1} {D : Type u_2} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C D) (j : J) {Z : D} (h : F.obj (Y j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (e.inv j)) (CategoryTheory.CategoryStruct.comp (F.map (e.hom j)) h) = h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side, version subtracting vectors.  -/
Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (toEquiv : A ≃ B) →
                  (∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y) →
                    (∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) →
                      (∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r) → A ≃ₐ[R] B
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.toAlgHom : {R : Type u_3} →
  [inst : CommSemiring R] →
    {A : Type u_4} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_5} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A →A[R] B) → A →ₐ[R] B
-- Mathlib.Data.ENat.Basic
ENat.le_sub_of_add_le_right : ∀ {a b c : ℕ∞}, b ≠ ⊤ → a + b ≤ c → a ≤ c - b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
ModuleCat.restrictScalarsId'.congr_simp : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R),
  ModuleCat.restrictScalarsId' f hf = ModuleCat.restrictScalarsId' f hf
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [Inhabited α] {k fallback : α} {f : β → β},
  (Std.DTreeMap.Const.modify t k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (j : ↑J.obj), J.PropSetWithTop κ' {↑j, ⊤}
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α Id β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β},
  it₁.IsPlausibleStep Std.IterStep.done → (Std.Iter.flatMapAfterM f it₁ none).IsPlausibleStep Std.IterStep.done
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.ofLoogleJson? : Lean.Json → Option LeanSearchClient.SearchResult
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.mono_pre : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal) {r r' : ENNReal},
  r ≤ r' → MeasureTheory.OuterMeasure.mkMetric'.pre m r' ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r
-- Mathlib.Algebra.Order.Ring.Abs
abs_mul : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a b : α), |a * b| = |a| * |b|
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_nonempty : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, (G.neighborSet v).Nonempty ↔ ¬G.IsIsolated v
-- Mathlib.Order.Height
Set.chainHeight_of_isEmpty : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop) [IsEmpty α], s.chainHeight r = 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.MutuallySingular.eq_1 : ∀ {α : Type u_1} {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  μ.MutuallySingular ν = ∃ s, MeasurableSet s ∧ μ s = 0 ∧ ν sᶜ = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.head.congr_simp : ∀ {m a a_1 : ℕ} (e_a : a = a_1) {L L_1 : List ℕ} (e_L : L = L_1) (hl : SimplexCategoryGenRel.IsAdmissible m (a :: L)),
  hl.head = ⋯.head
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.hasLimits' : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasLimits (ModuleCat R)
-- Mathlib.RingTheory.Etale.Basic
/-- Étale is stable under base change.  -/
Algebra.Etale.baseChange : ∀ (R : Type u) (A : Type v) (B : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Etale R A], Algebra.Etale B (TensorProduct R B A)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_neg' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp (-a) b = p - toIocMod hp a (-b)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_pow : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] E)
  (n : ℕ), ContinuousLinearMap.rTensor G (f ^ n) = ContinuousLinearMap.rTensor G f ^ n
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.MonoidalClosed.linearHomEquiv.eq_1 : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G),
  Rep.MonoidalClosed.linearHomEquiv A B C =
    { toFun := ((CategoryTheory.ihom.adjunction A).homEquiv B C).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := ((CategoryTheory.ihom.adjunction A).homEquiv B C).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Measure.AddContent
/-- An additive content obtained from another one on the same semiring of sets by setting the value
of each set not in the semiring at `∞`.  -/
MeasureTheory.AddContent.extend : {α : Type u_1} →
  {C : Set (Set α)} →
    MeasureTheory.IsSetSemiring C → MeasureTheory.AddContent ENNReal C → MeasureTheory.AddContent ENNReal C
-- Mathlib.Algebra.Order.Pi
Function.const_nonneg_of_nonneg : ∀ {α : Type u_2} (β : Type u_3) [inst : Zero α] [inst_1 : Preorder α] {a : α}, 0 ≤ a → 0 ≤ Function.const β a
-- Mathlib.Order.Max
/-- `a : α` is a top element of `α` if it is greater than or equal to any other element of `α`.
This predicate is roughly an unbundled version of `OrderBot`, except that a preorder may have
several top elements. When `α` is linear, this is useful to make a case disjunction on
`NoMaxOrder α` within a proof.  -/
IsTop : {α : Type u_1} → [LE α] → α → Prop
-- Mathlib.NumberTheory.Divisors
Nat.pairwise_divisorsAntidiagonalList_snd : ∀ {n : ℕ}, List.Pairwise (fun x1 x2 => x1.2 > x2.2) n.divisorsAntidiagonalList
-- Init.Data.List.Lemmas
List.eraseDupsBy.loop.eq_2 : ∀ {α : Type u_1} (r : α → α → Bool) (a : List α) (a_1 : α) (l : List α),
  List.eraseDupsBy.loop r (a_1 :: l) a =
    match a.any (r a_1) with
    | true => List.eraseDupsBy.loop r l a
    | false => List.eraseDupsBy.loop r l (a_1 :: a)
-- Mathlib.Analysis.Distribution.Distribution
/-- The Dirac delta distribution. This is zero if `x` does not belong to `Ω`.  -/
Distribution.delta : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → {Ω : TopologicalSpace.Opens E} → {n : ℕ∞} → E → Distribution Ω ℝ n
-- Mathlib.Data.Set.Finite.Basic
Finset.mem_range_coe_iff : ∀ {α : Type u} {s : Set α}, s ∈ Set.range SetLike.coe ↔ s.Finite
-- Mathlib.Dynamics.Flow
/-- A set `s ⊆ α` is forward-invariant under `ϕ : τ → α → α` if `ϕ t s ⊆ s` for all `t ≥ 0`.  -/
IsForwardInvariant : {τ : Type u_1} → {α : Type u_2} → [Preorder τ] → [Zero τ] → (τ → α → α) → Set α → Prop
-- Aesop.Search.SearchM
Aesop.NormSimpContext.mk.injEq : ∀ (toContext : Lean.Meta.Simp.Context) (enabled useHyps : Bool) (configStx? : Option Lean.Term)
  (simprocs : Lean.Meta.Simp.SimprocsArray) (toContext_1 : Lean.Meta.Simp.Context) (enabled_1 useHyps_1 : Bool)
  (configStx?_1 : Option Lean.Term) (simprocs_1 : Lean.Meta.Simp.SimprocsArray),
  ({ toContext := toContext, enabled := enabled, useHyps := useHyps, configStx? := configStx?, simprocs := simprocs } =
      { toContext := toContext_1, enabled := enabled_1, useHyps := useHyps_1, configStx? := configStx?_1,
        simprocs := simprocs_1 }) =
    (toContext = toContext_1 ∧
      enabled = enabled_1 ∧ useHyps = useHyps_1 ∧ configStx? = configStx?_1 ∧ simprocs = simprocs_1)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_of_mul_le_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [MulPosMono α],
  a * b ≤ c → d ≤ a → 0 ≤ b → d * b ≤ c
-- Mathlib.Analysis.Analytic.Order
/-- A function vanishes at a point if its analytic order is nonzero when converted to ℕ.  -/
apply_eq_zero_of_analyticOrderNatAt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderNatAt f z₀ ≠ 0 → f z₀ = 0
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.exists_rename_eq_of_vars_subset_range : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R) (f : τ → σ),
  Function.Injective f → ↑p.vars ⊆ Set.range f → ∃ q, (MvPolynomial.rename f) q = p
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.decomposeAux_eq_decompose : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : CommSemiring R] (f : M →+ ι),
  ⇑(AddMonoidAlgebra.decomposeAux f) = ⇑(DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f))
-- Init.Data.List.Lex
List.left_le_left_of_cons_le_cons : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {a b : α} {l₁ l₂ : List α},
  a :: l₁ ≤ b :: l₂ → a ≤ b
-- Mathlib.FieldTheory.SeparableClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then `separableClosure F E` and
`separableClosure F K` are also isomorphic as `F`-algebras.  -/
separableClosure.algEquivOfAlgEquiv : {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] → (E ≃ₐ[F] K) → ↥(separableClosure F E) ≃ₐ[F] ↥(separableClosure F K)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.desc_extend : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F)
  {X : C} (f : c.pt ⟶ X),
  CategoryTheory.Limits.colimit.desc F (c.extend f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F c) f
-- Mathlib.Probability.Independence.Process.Basic
/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.iIndepFun.iIndepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4}
  {𝓧 : (i : S) → T i → Type u_5} [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)]
  {X : (i : S) → (j : T i) → Ω → 𝓧 i j},
  (∀ (i : S) (j : T i), AEMeasurable (X i j) P) →
    (∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), ProbabilityTheory.iIndepFun (fun i ω j => X (↑i) (↑j) ω) P) →
      ProbabilityTheory.iIndepFun (fun i ω j => X i j ω) P
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.prodMap : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {n : WithTop ℕ∞} {g : N → N'},
  ContMDiff I I' n f → ContMDiff J J' n g → ContMDiff (I.prod J) (I'.prod J') n (Prod.map f g)
-- Mathlib.Tactic.Linarith.Parsing
/-- `linearFormOfExpr red map e` computes the linear form of `e`.

`map` is a lookup map from atomic expressions to variable numbers.
If a new atomic expression is encountered, it is added to the map with a new number.
It matches atomic expressions up to reducibility given by `red`.

Because it matches up to definitional equality, this function must be in the `MetaM` monad,
and forces some functions that call it into `MetaM` as well.
 -/
Mathlib.Tactic.Linarith.linearFormOfExpr : Lean.Meta.TransparencyMode →
  Mathlib.Tactic.Linarith.ExprMap →
    Lean.Expr → Lean.MetaM (Mathlib.Tactic.Linarith.ExprMap × Mathlib.Tactic.Linarith.Sum)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def'_norm : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (e : Int.Internal.Linear.Expr)
  (ePoly ePoly' p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def'_norm_cert x e ePoly ePoly' p = true →
    Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Expr.denote ctx e →
      Int.Internal.Linear.Poly.denote' ctx ePoly = Int.Internal.Linear.Poly.denote' ctx ePoly' →
        Int.Internal.Linear.Poly.denote' ctx p = 0
-- Std.Time.DateTime.WallTime
/-- Adds a `Day.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addDays : Std.Time.WallTime → Std.Time.Day.Offset → Std.Time.WallTime
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream'.Seq α),
  Stream'.Seq1.map f (a, s) = (f a, Stream'.Seq.map f s)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.bot_lt_toWithBotNat_iff : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x : R),
  ⊥ < IsDiscreteValuationRing.toWithBotNat x ↔ x ≠ 0
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_two` for a version with the type implicit.  -/
zero_lt_two' : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 2
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The algebraic closure of `F` in `E` is equal to `E` if and only if `E / F` is
algebraic.  -/
algebraicClosure.eq_top_iff : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  algebraicClosure F E = ⊤ ↔ Algebra.IsAlgebraic F E
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An equality of subobjects gives an isomorphism of the corresponding objects.  -/
CategoryTheory.Subobject.isoOfMkEq : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A : C} →
      (f : A ⟶ B) →
        [inst_1 : CategoryTheory.Mono f] →
          (X : CategoryTheory.Subobject B) →
            CategoryTheory.Subobject.mk f = X → (A ≅ CategoryTheory.Subobject.underlying.obj X)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Combine two initial results.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.append : {α : Type} →
  Lean.Meta.RefinedDiscrTree.InitResults✝ α →
    Lean.Meta.RefinedDiscrTree.InitResults✝ α → Lean.Meta.RefinedDiscrTree.InitResults✝ α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp k ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_4 : ∀ (coeff k : ℕ) (a : Nat.Internal.Linear.Expr),
  Nat.Internal.Linear.Expr.toPoly.go coeff (Nat.Internal.Linear.Expr.mulL k a) =
    bif k == 0 then id else Nat.Internal.Linear.Expr.toPoly.go (coeff * k) a