mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Ideal
/-- An ideal is maximal if it is maximal in the collection of proper ideals.

Note that `IsCoatom` is less general because ideals only have a top element when `P` is directed
and nonempty.  -/
Order.Ideal.IsMaximal : {P : Type u_1} → [inst : LE P] → Order.Ideal P → Prop
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cone `c : Cone (F ⋙ forget)`
of the underlying functor to types, this is a cone for `F` whose point is
`c.pt` with the infimum of the induced topologies by the maps `c.π.app j`.  -/
TopCat.coneOfConeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat)) → CategoryTheory.Limits.Cone F
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.notMem_setOfIdeal : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] {I : Ideal C(X, R)} {x : X},
  x ∉ ContinuousMap.setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {A B : CommAlgCat R} → (↑A →ₐ[R] ↑B) → A.Hom B
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.instCoalgEquivClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B], CoalgEquivClass (A ≃ₗc[R] B) R A B
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Solve equations for `K⟮X⟯` by applying `RatFunc.induction_on`.  -/
RatFunc.tacticSmul_tac : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f hf).inv.toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h)
-- Init.Data.UInt.Bitwise
UInt8.and_self : ∀ {a : UInt8}, a &&& a = a
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J LightProfinite),
  TotallyDisconnectedSpace ↑(CompHaus.limitCone (F.comp lightProfiniteToCompHaus)).pt.toTop
-- Mathlib.Data.Finset.Lattice.Fold
List.foldr_inf_eq_inf_toFinset : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (l : List α),
  List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l = l.toFinset.inf id
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.differentiableAt : ∀ {𝕜 : 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] {f : E → F}
  {x : E}, IsBoundedLinearMap 𝕜 f → DifferentiableAt 𝕜 f x
-- Lean.Elab.Binders
Lean.Elab.Term.expandMatchAltsIntoMatchTactic : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Init.Data.Range.Polymorphic.Lemmas
Std.PRange.UpwardEnumerable.least.congr_simp : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [hn : Nonempty α],
  Std.PRange.UpwardEnumerable.least = Std.PRange.UpwardEnumerable.least
-- Mathlib.Data.List.Basic
/-- There is only one list of an empty type  -/
List.uniqueOfIsEmpty : {α : Type u} → [IsEmpty α] → Unique (List α)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instBot : {α : Type u_2} → {β : Type u_3} → [inst : SupSet α] → {x : CompleteLattice β} → Bot (sSupHom α β)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsStableUnderPostcompHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPostcomp (HomotopicalAlgebra.CofibrantObject.homRel C)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} (h' : a ∈ m), m[a]? = some m[a]
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofLimitCone_π : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J),
  (CategoryTheory.Limits.Bicone.ofLimitCone ht).π j = t.π.app { as := j }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, k ∉ m₁ → Std.ExtDHashMap.Const.get! (m₁ \ m₂) k = default
-- Init.Data.UInt.Bitwise
UInt8.shiftRight_zero : ∀ {a : UInt8}, a >>> 0 = a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxc.HasSize α]
  [Std.Rxc.LawfulHasSize α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.app : Option Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Option Lean.Grind.AC.Seq
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B), ⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
-- Mathlib.LinearAlgebra.Projection
Submodule.toLinearMap_prodEquivOfIsCompl_symm : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), ↑(p.prodEquivOfIsCompl q hpq).symm = (p.projectionOnto q hpq).prod (q.projectionOnto p ⋯)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeWhile_eq_toSlice_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.takeWhile pat = s.toSlice ↔ s.all pat = true
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.Meta.NormNum.nnreal_rpow_isRat_eq_inv_nnreal_rpow : ∀ (a : NNReal) (b : ℝ) (n d : ℕ), Mathlib.Meta.NormNum.IsRat b (Int.negOfNat n) d → a ^ b = a⁻¹ ^ (↑n / ↑d)
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.mk.sizeOf_spec : ∀ (promise : IO.Promise Unit) (setRef : IO.Ref Bool),
  sizeOf { promise := promise, setRef := setRef } = 1 + sizeOf promise + sizeOf setRef
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  x = 1 →
    (match x with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | x => h_3 x) ≍
      h_2 ()
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.apprSeq_apply_eq_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ)
  {x : X}, x ∈ F → (hF.apprSeq n) x = 1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.bind.eq_1 : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α)
  (f : α → Std.Iterators.HetT m β),
  x.bind f =
    { Property := fun b => ∃ a, x.Property a ∧ (f a).Property b, small := ⋯,
      operation := do
        let a ← x.operation
        (fun b => Std.Internal.USquash.deflate ⟨↑b.inflate, ⋯⟩) <$> (f ↑a.inflate).operation }
-- Mathlib.CategoryTheory.Square
CategoryTheory.NatTrans.mapSquare_app_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C),
  ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₃ = τ.app sq.X₃
-- Lean.Meta.Tactic.Grind.PP
/-- Helper function for pretty printing the state for debugging purposes.  -/
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Goal.ppENodeDecl : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_id : ∀ {X : TopCat}, TopCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = ContinuousMap.id ↑X
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.mk.inj : ∀ {M : Type u_1} {inst : Monoid M} {N : Type u_2} {inst_1 : Monoid N} {φ : M →* N} {A : Type u_4} {inst_2 : Monoid A}
  {inst_3 : MulDistribMulAction M A} {B : Type u_5} {inst_4 : Monoid B} {inst_5 : MulDistribMulAction N B}
  {toMulActionHom : A →ₑ[⇑φ] B} {map_one' : toMulActionHom.toFun 1 = 1}
  {map_mul' : ∀ (x y : A), toMulActionHom.toFun (x * y) = toMulActionHom.toFun x * toMulActionHom.toFun y}
  {toMulActionHom_1 : A →ₑ[⇑φ] B} {map_one'_1 : toMulActionHom_1.toFun 1 = 1}
  {map_mul'_1 : ∀ (x y : A), toMulActionHom_1.toFun (x * y) = toMulActionHom_1.toFun x * toMulActionHom_1.toFun y},
  { toMulActionHom := toMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
      { toMulActionHom := toMulActionHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toMulActionHom = toMulActionHom_1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε G =
    (adj.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Mathlib.Computability.TuringMachine.Config
/-- The `then k` function is a "configuration homomorphism". Its operation on states is to append
`k` to the continuation of a `Cfg.ret` state, and to run `k` on `v` if we are in the `Cfg.halt v`
state.  -/
Turing.ToPartrec.Cfg.then : Turing.ToPartrec.Cfg → Turing.ToPartrec.Cont → Turing.ToPartrec.Cfg
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- `f⁺ g` is the left Kan extension of `g` along `f`.
```
  b
  △ \
  |   \ f⁺ g
f |     \
  |       ◿
  a - - - ▷ c
      g
```
 -/
CategoryTheory.Bicategory.«term_⁺_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_zero : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.condExpL1 hm μ 0 = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The canonical morphism from `G` to its profinite completion.  -/
ProfiniteAddGrp.ProfiniteCompletion.eta : (G : AddGrpCat) → G ⟶ AddGrpCat.of ↑(ProfiniteAddGrp.ProfiniteCompletion.completion G).toProfinite.toTop
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_one_eq_lintegral_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε},
  MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
-- Mathlib.Algebra.Group.AddChar
/-- An additive character maps negatives to inverses (when defined)  -/
AddChar.map_neg_eq_inv : ∀ {A : Type u_1} {M : Type u_2} [inst : AddGroup A] [inst_1 : DivisionMonoid M] (ψ : AddChar A M) (a : A),
  ψ (-a) = (ψ a)⁻¹
-- Mathlib.GroupTheory.Nilpotent
/-- A group `G` is nilpotent if its upper central series is eventually `G`.  -/
Group.IsNilpotent : (G : Type u_2) → [Group G] → Prop
-- Mathlib.Data.Rat.Defs
Rat.mk'_zero : ∀ (d : ℕ) (h : d ≠ 0) (w : (Int.natAbs 0).Coprime d), { num := 0, den := d, den_nz := h, reduced := w } = 0
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.warning.sizeOf_spec : sizeOf Lean.Lsp.MessageType.warning = 1
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.ihom_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{u, u} C] {D E : Type u} [inst_1 : CategoryTheory.Category.{u, u} D]
  [inst_2 : CategoryTheory.Category.{u, u} E] (F : CategoryTheory.Functor D E),
  (CategoryTheory.ihom (CategoryTheory.Cat.of C)).map F.toCatHom =
    ((CategoryTheory.Functor.whiskeringRight C D E).obj F).toCatHom
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.Builder.share1 : Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Topology.Order.OrderClosed
interior_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b : α},
  interior (Set.Ioo a b) = Set.Ioo a b
-- Mathlib.Tactic.FieldSimp.Discharger
/-- Default discharge strategy for `field` and `field_simp`: try to solve the (in)equality `prop`,
of the form `t = 0` or `t > 0`, by one of the following strategies:

* Use an assumption from the context.
* Use the `norm_num` tactic.
* Use the `positivity` tactic.
* Use the `simp` tactic with `discharge` as discharger and lemmas stating:
  * `2 ≠ 0`, `3 ≠ 0`, `4 ≠ 0`
  * `x ≠ 0 → y ≠ 0 → x * y ≠ 0`
  * `a ≠ 0 → a ^ n ≠ 0` (for `n : ℕ` and `n : ℤ`)
  * `↑n + 1 ≠ 0`, if `n : ℕ` and the field has characteristic 0.

If none of the strategies finds a proof for `prop`, the result is `none`.
 -/
Mathlib.Tactic.FieldSimp.tacticField_simp_discharge : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : (CategoryTheory.ObjectProperty.isFinitelyPresentable C).FullSubcategory),
  CategoryTheory.IsFinitelyPresentable ((CategoryTheory.ObjectProperty.isFinitelyPresentable C).ι.obj X)
-- Mathlib.FieldTheory.Perfect
powMulEquiv_symm_pow_p : ∀ (M : Type u_1) (p : ℕ) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (x : M), (powMulEquiv M p).symm x ^ p = x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
/-- Eisenstein series are MDifferentiable (i.e. holomorphic functions from `ℍ → ℂ`).  -/
EisensteinSeries.eisensteinSeriesSIF_mdifferentiable : ∀ {k : ℤ} {N : ℕ}, 3 ≤ k → ∀ (a : Fin 2 → ZMod N), MDiff ⇑(EisensteinSeries.eisensteinSeriesSIF a k)
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.neg_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α : u ⟶ v), (-α).left = -α.left
-- Init.Data.Vector.Lex
/-- `l₁` is *not* lexicographically less than `l₂`
(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂` or
- there exists an index `i` such that
  - for all `j < i`, `l₁[j] == l₂[j]` and
  - `l₂[i] < l₁[i]`

This formulation requires that `==` and `lt` are compatible in the following senses:
- `==` is symmetric
  (we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
- `lt` is irreflexive with respect to `==` (i.e. if `x == y` then `lt x y = false`
- `lt` is asymmetric  (i.e. `lt x y = true → lt y x = false`)
- `lt` is antisymmetric with respect to `==` (i.e. `lt x y = false → lt y x = false → x == y`)
 -/
Vector.lex_eq_false_iff_exists : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [PartialEquivBEq α] (lt : α → α → Bool),
  (∀ (x y : α), (x == y) = true → lt x y = false) →
    (∀ (x y : α), lt x y = true → lt y x = false) →
      (∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true) →
        ∀ {xs ys : Vector α n},
          xs.lex ys lt = false ↔
            (ys.isEqv xs fun x1 x2 => x1 == x2) = true ∨
              ∃ i, ∃ (h : i < n), (∀ (j : ℕ) (hj : j < i), (xs[j] == ys[j]) = true) ∧ lt ys[i] xs[i] = true
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
`Hⁿ(Hom(P, A))`, where `P` is any projective resolution of `k` as a trivial `k`-linear
`G`-representation.  -/
groupCohomologyIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (n : ℕ) →
          (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) →
            groupCohomology A n ≅ HomologicalComplex.homology (P.complex.linearYonedaObj k A) n
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- `Orientation.finOrthonormalBasis` gives a basis with the required orientation.  -/
Orientation.finOrthonormalBasis_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} (hn : 0 < n)
  (h : Module.finrank ℝ E = n) (x : Orientation ℝ E (Fin n)),
  (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.equivOp_apply_coe : ∀ {M : Type u_2} [inst : AddZeroClass M] (H : AddSubmonoid M) (a : ↥H), ↑(H.equivOp a) = AddOpposite.op ↑a
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.rs : Lean.Elab.Command.FinalizeInductiveDecl✝ → Array Lean.Elab.Command.PreElabHeaderResult
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see `charFunDual_pi`
for the Hilbert space version.  -/
MeasureTheory.charFunDual_pi : ∀ {ι : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_5}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (L : StrongDual ℝ ((i : ι) → E i)),
  MeasureTheory.charFunDual (MeasureTheory.Measure.pi μ) L =
    ∏ i, MeasureTheory.charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cot.eq_1 : ∀ (z : ℂ), z.cot = Complex.cos z / Complex.sin z
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_le : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s₁ s₂ : Set α),
  μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- The empty multiseries.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- Composition of partial diffeomorphisms.  -/
PartialDiffeomorph.trans : {𝕜 : 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] →
                {F' : Type u_4} →
                  [inst_5 : NormedAddCommGroup F'] →
                    [inst_6 : NormedSpace 𝕜 F'] →
                      {H₁ : Type u_5} →
                        [inst_7 : TopologicalSpace H₁] →
                          {H₂ : Type u_6} →
                            [inst_8 : TopologicalSpace H₂] →
                              {H₃ : Type u_7} →
                                [inst_9 : TopologicalSpace H₃] →
                                  {I : ModelWithCorners 𝕜 E H₁} →
                                    {J : ModelWithCorners 𝕜 F H₂} →
                                      {K : ModelWithCorners 𝕜 F' H₃} →
                                        {M : Type u_8} →
                                          [inst_10 : TopologicalSpace M] →
                                            [inst_11 : ChartedSpace H₁ M] →
                                              {N : Type u_9} →
                                                [inst_12 : TopologicalSpace N] →
                                                  [inst_13 : ChartedSpace H₂ N] →
                                                    {P : Type u_10} →
                                                      [inst_14 : TopologicalSpace P] →
                                                        [inst_15 : ChartedSpace H₃ P] →
                                                          {n : WithTop ℕ∞} →
                                                            PartialDiffeomorph I J M N n →
                                                              PartialDiffeomorph J K N P n →
                                                                PartialDiffeomorph I K M P n
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.zero_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2],
  AffineMap.linear 0 = 0
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_eq : ∀ {α : Type u_4} {β : Type u_5} [_F : Fintype α] [_G : Fintype β], Fintype.card α = Fintype.card β ↔ Nonempty (α ≃ β)
-- Mathlib.Data.Opposite
Opposite.instSubsingleton : ∀ {α : Sort u} [Subsingleton α], Subsingleton αᵒᵖ
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.rightLim_eq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [OrderTopology R] (f : StieltjesFunction R)
  (x : R), Function.rightLim (↑f) x = ↑f x
-- Init.Conv
/-- `args` traverses into all arguments. Synonym for `congr`.  -/
Lean.Parser.Tactic.Conv.convArgs : Lean.ParserDescr
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.inv_sub_inv_eq_inv : ∀ (p q : ENNReal) {r : ENNReal} [p.HolderTriple q r], r ≠ 0 → r⁻¹ - q⁻¹ = p⁻¹
-- Init.Data.String.Basic
/-- Given a position in `s.sliceFrom p₀`, obtain the corresponding position in `s`.  -/
String.Pos.ofSliceFrom : {s : String} → {p₀ : s.Pos} → (s.sliceFrom p₀).Pos → s.Pos
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.restrict_compl : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), M.restrict (M.E \ D) = M.delete D