mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Setup
Lean.instToJsonModuleArtifacts : Lean.ToJson Lean.ModuleArtifacts
-- Mathlib.Order.CompleteLattice.Defs
/-- Any `CompleteSemilatticeSup` is in fact a `CompleteLattice`.

Note that this construction has bad definitional properties:
see the doc-string on `completeLatticeOfSup`.
 -/
completeLatticeOfCompleteSemilatticeSup : (α : Type u_8) → [CompleteSemilatticeSup α] → CompleteLattice α
-- Init.Data.Int.Gcd
Int.ediv_gcd_ne_zero_of_ne_zero_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → a / ↑(a.gcd b) ≠ 0
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.coe_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y}, ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(CategoryTheory.ConcreteCategory.hom g) → f = g
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.toEffectiveImport : Lean.ImportedModule✝ → Lean.EffectiveImport
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.d₂₁ A =
    ModuleCat.ofHom
      ((Finsupp.lsum k) fun g => Finsupp.lsingle g.2 ∘ₗ A.ρ g.1⁻¹ - Finsupp.lsingle (g.1 * g.2) + Finsupp.lsingle g.1)
-- Std.Http.Internal.Char
Std.Http.Internal.Char.not_quotedStringChar_of_not_qdtext_not_dquote_backslash : ∀ c < '',
  ¬Std.Http.Internal.Char.qdtext c = true ∧ ¬(decide (c = '\"') || decide (c = '\\')) = true →
    ¬Std.Http.Internal.Char.quotedStringChar c = true
-- Std.Time.DateTime
Std.Time.instInhabitedDateTime : Inhabited Std.Time.DateTime
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.evalMonoidHom_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (j : ι), (RestrictedProduct.evalMonoidHom R j) x = x j
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) (α : (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X),
  (CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy X F α).inv =
    { app := fun X_1 => AddGrpCat.ofHom ↑{ toEquiv := α.homEquiv.symm, map_add' := ⋯ }, naturality := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.LawfulToForwardSearcherModel.congr_simp : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {σ : String.Slice → Type}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id],
  String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat =
    String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat
-- Mathlib.GroupTheory.Index
Subgroup.IsFiniteRelIndex.mk : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K ≠ 0 → H.IsFiniteRelIndex K
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The unique additive monoid homomorphism `FreeAddMonoid α →+ FreeAddMonoid β`
that sends each `of x` to `of (f x)`.  -/
FreeAddMonoid.map : {α : Type u_1} → {β : Type u_2} → (α → β) → FreeAddMonoid α →+ FreeAddMonoid β
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- For any function `f` tending to infinity, `f ^ exp` is majorized by `f` with exponent `exp`.  -/
Tactic.ComputeAsymptotics.Majorized.self : ∀ {f : ℝ → ℝ} {exp : ℝ},
  Filter.Tendsto f Filter.atTop Filter.atTop → Tactic.ComputeAsymptotics.Majorized (f ^ exp) f exp
-- Mathlib.ModelTheory.Syntax
/-- A bijection sending formulas to sentences with constants.  -/
FirstOrder.Language.Formula.equivSentence : {L : FirstOrder.Language} → {α : Type u'} → L.Formula α ≃ (L.withConstants α).Sentence
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.HomotopyCategory₂.mk.sizeOf_spec : ∀ {A : SSet.Truncated 2}
  (pt : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })),
  sizeOf { pt := pt } = 1 + sizeOf pt
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instCoeSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → Coe (OpenNormalSubgroup G) (Subgroup G)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- When a vector is in `Kᗮ`.  -/
ClosedSubmodule.mem_orthogonal : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) (v : E), v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 u v = 0
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsPGroup.isCyclic_of_isZGroup : ∀ {G : Type u_1} [inst : Group G] [IsZGroup G] {p : ℕ} [Fact (Nat.Prime p)] {P : Subgroup G},
  IsPGroup p ↥P → IsCyclic ↥P
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a commutative additive group object, then `Hom(X, G)` has a commutative
additive group structure.  -/
CategoryTheory.Hom.addCommGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G X : C} →
        [inst_2 : CategoryTheory.AddGrpObj G] →
          [inst_3 : CategoryTheory.BraidedCategory C] → [CategoryTheory.IsCommAddMonObj G] → AddCommGroup (X ⟶ G)
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limitCone_π_app : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J),
  (CategoryTheory.Cat.HasLimits.limitCone F).π.app j =
    {
        obj :=
          ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j)),
        map := fun {X Y} f =>
          (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j))
            f,
        map_id := ⋯, map_comp := ⋯ }.toCatHom
-- Init.Data.String.TakeDrop
String.Internal.trimImpl : String → String
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insert'.eq_def : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α) (x_1 : Ordnode α),
  Ordnode.insert' x x_1 =
    match x_1 with
    | Ordnode.nil => Ordnode.singleton x
    | t@h:(Ordnode.node size l y r) =>
      match cmpLE x y with
      | Ordering.lt => (Ordnode.insert' x l).balanceL y r
      | Ordering.eq => t
      | Ordering.gt => l.balanceR y (Ordnode.insert' x r)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_self_add_compl : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f : α → M), s.indicator f + sᶜ.indicator f = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxEntry!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)], t₁.Equiv t₂ → t₁.maxEntry! = t₂.maxEntry!
-- Mathlib.Algebra.Free
FreeMagma.traverse_eq : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeMagma α),
  FreeMagma.traverse F x = traverse F x
-- Lean.Parser.Term
/-- `unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
the compiler is unable to guarantee the safety of the operation.

For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
 -/
Lean.Parser.Term.unsafe : Lean.Parser.Parser
-- Mathlib.RingTheory.Coalgebra.Basic
/-- A coalgebra over a commutative (semi)ring `R` is an `R`-module equipped with a coassociative
comultiplication `Δ` and a counit `ε` obeying the left and right counitality laws.  -/
Coalgebra : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Type (max u v)
-- Mathlib.CategoryTheory.IsoCat
_private.Mathlib.CategoryTheory.IsoCat.0.CategoryTheory.Functor.strictInv.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [inst_2 : F.IsIso],
  F.strictInv =
    { obj := ⇑F.objEquiv.symm,
      map := fun {X Y} f =>
        F.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))),
      map_id := ⋯, map_comp := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.getTermRingId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SSameSide (t.points i₁) (Affine.Simplex.excenter t {i₂})
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_tail : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (t : Fin (n + 1) →₀ M), Finsupp.cons (t 0) t.tail = t
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGEFunctor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c') (e_e : e = e_1)
  [inst : e.IsTruncGE] (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.CategoryWithHomology C], e.truncGEFunctor C = e_1.truncGEFunctor C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- the series `sqrtTwoAddSeries x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrtTwoAddSeries 0 n / 2`
 -/
Real.sqrtTwoAddSeries : ℝ → ℕ → ℝ
-- Init.Data.SInt.Lemmas
Int16.ofInt_lt_iff_lt : ∀ {a b : ℤ},
  Int16.minValue.toInt ≤ a →
    a ≤ Int16.maxValue.toInt →
      Int16.minValue.toInt ≤ b → b ≤ Int16.maxValue.toInt → (Int16.ofInt a < Int16.ofInt b ↔ a < b)
-- Mathlib.Probability.IdentDistrib
MeasureTheory.AEMeasurable.identDistrib_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α}
  {f : α → γ} (hf : AEMeasurable f μ), ProbabilityTheory.IdentDistrib f (AEMeasurable.mk f hf) μ μ
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_mapRange : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : α ↪ β) (g : M → N)
  (p : α →₀ M) (hg : g 0 = 0),
  Finsupp.embDomain f (Finsupp.mapRange g hg p) = Finsupp.mapRange g hg (Finsupp.embDomain f p)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodAssoc_toLinearEquiv : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : TopologicalSpace M₁] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃],
  ↑(ContinuousLinearEquiv.prodAssoc R M₁ M₂ M₃) = LinearEquiv.prodAssoc R M₁ M₂ M₃
-- Init.Data.UInt.Lemmas
UInt64.toFin_div : ∀ (a b : UInt64), (a / b).toFin = a.toFin / b.toFin
-- Init.System.IO
IO.FS.Stream.Buffer.mk.inj : ∀ {data : ByteArray} {pos : ℕ} {data_1 : ByteArray} {pos_1 : ℕ},
  { data := data, pos := pos } = { data := data_1, pos := pos_1 } → data = data_1 ∧ pos = pos_1
-- Mathlib.Data.List.Perm.Basic
List.Perm.foldr_op_eq : ∀ {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ l₂ : List α} {a : α},
  l₁.Perm l₂ → List.foldr op a l₁ = List.foldr op a l₂
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.alternatingMapToDual_apply_ιMulti : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (f : Fin n → Module.Dual R M) (v : Fin n → M),
  ((exteriorPower.alternatingMapToDual R M n) f) ((exteriorPower.ιMulti R n) v) = (Matrix.of fun i j => (f j) (v i)).det
-- Mathlib.GroupTheory.Nilpotent
AddGroup.isNilpotent_congr : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (e : G ≃+ H),
  AddGroup.IsNilpotent G ↔ AddGroup.IsNilpotent H
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_comp_add_right : ∀ {𝕜 : 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} {s : Set E} (a : E),
  DifferentiableWithinAt 𝕜 (fun x => f (x + a)) s x ↔ DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)
-- Init.Data.UInt.Bitwise
UInt16.xor_not : ∀ {a b : UInt16}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Mathlib.Data.List.Map2
List.map₂Right.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β),
  List.map₂Right f as bs = List.map₂Left (flip f) bs as
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_toDual : ∀ {α : Type u_1} [inst : Lattice α] (a b : α),
  Set.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIcc a b
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.opEquiv.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G],
  AddSubgroup.opEquiv =
    { toFun := AddSubgroup.op, invFun := AddSubgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.map_circulant : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_3} [inst : Sub n] (v : n → α) (f : α → β),
  (Matrix.circulant v).map f = Matrix.circulant fun i => f (v i)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
modelWithCornersSelf_coe : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ↑(modelWithCornersSelf 𝕜 E) = id
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have r := ⟨(↑r).insertIfNew a (), ⋯⟩;
            pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {a : α} {b : Unit}, P m'' → P (m''.insertIfNew a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Data.Nat.Find
/-- If a predicate `p` holds at some `x` and agrees with `q` up to that `x`, then
their `Nat.find` agree. The stronger version of `Nat.find_congr'`, since this one needs
agreement only up to `Nat.find _` while the other requires `p = q`.
Usage of this lemma will likely be via `obtain ⟨x, hx⟩ := hp; apply Nat.find_congr hx` to unify `q`,
or provide it explicitly with `rw [Nat.find_congr (q := q) hx]`.
 -/
Nat.find_congr : ∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {x : ℕ} (hx : p x) (hpq : ∀ n ≤ x, p n ↔ q n),
  Nat.find ⋯ = Nat.find ⋯
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.dual : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α}, t.Valid → t.dual.Valid
-- Mathlib.RingTheory.LocalRing.LocalSubring
Subring.copy.congr_simp : ∀ {R : Type u} [inst : NonAssocRing R] (S S_1 : Subring R) (e_S : S = S_1) (s s_1 : Set R) (e_s : s = s_1)
  (hs : s = ↑S), S.copy s hs = S_1.copy s_1 ⋯
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.dense_preimage_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G}
  {s : Set (G ⧸ N)}, Dense (QuotientGroup.mk ⁻¹' s) ↔ Dense s
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Right identity of the `L^p` product as an isometric equivalence.  -/
IsometryEquiv.withLpProdUnique : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] →
        [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → [Unique β] → WithLp p (α × β) ≃ᵢ α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km → t.contains km = true
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatDvd : ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.oneLE_toSubmonoid : ∀ {H : Type u_1} [inst : CommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedMonoid H],
  (GroupCone.oneLE H).toSubmonoid = Submonoid.oneLE H
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_congr : ∀ {α β : Type u} (e : α ≃ β), Cardinal.mk α = Cardinal.mk β
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_unone : ∀ {α : Type u} {x : WithOne α} (hx : x ≠ 1), ↑(WithOne.unone hx) = x
-- Mathlib.Data.Vector.MapLemmas
/-- If there is a set of states that is closed under `f`, and such that `f` produces that same output
for all states in this set, then the state is not actually needed.
Hence, then we can rewrite `mapAccumr₂` into just `map₂`.
 -/
List.Vector.mapAccumr₂_eq_map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} {ys : List.Vector β n}
  {f : α → β → σ → σ × γ} {s₀ : σ} (S : Set σ),
  s₀ ∈ S →
    (∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S) →
      (∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) →
        (List.Vector.mapAccumr₂ f xs ys s₀).2 = List.Vector.map₂ (fun x1 x2 => (f x1 x2 s₀).2) xs ys
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.prod_eq_zero : ∀ {ι : Type u_1} (f : ι → Cardinal.{u}), Cardinal.prod f = 0 ↔ ∃ i, f i = 0
-- Init.Data.Float.Float
Float.ofModel.injEq : ∀ (toModel toModel_1 : Float.Model), ({ toModel := toModel } = { toModel := toModel_1 }) = (toModel = toModel_1)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_div_natCast : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] (a : k) (n : ℕ),
  ⌊a / ↑n⌋ = ⌊a⌋ / ↑n
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_roo : ∀ {a b : ℕ}, (a<...b).toArray.size = b - a - 1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
ChainComplex.isoHomologyι₀_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : ChainComplex C ℕ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0] {Z : C} (h : HomologicalComplex.homology L 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp K.isoHomologyι₀.inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0)
      (CategoryTheory.CategoryStruct.comp L.isoHomologyι₀.inv h)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, subtracting vectors, if-and-if vector inner product form using square
roots.  -/
norm_sub_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ inner ℝ x y = 0
-- Std.Internal.UV.Timer
Std.Internal.UV.instNonemptyTimer : Nonempty Std.Internal.UV.Timer
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mkRBSet_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering}, RBTree.mkRBSet α cmp = ∅
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteAddMonoid.mk : ∀ {M : Type u_2} [inst : AddZero M], (∀ {a b : M}, a + b = 0 → b + a = 0) → IsDedekindFiniteAddMonoid M
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Serialize `proof` into the binary LRAT format as a `ByteArray`.
 -/
Std.Tactic.BVDecide.LRAT.lratProofToBinary : Array Std.Tactic.BVDecide.LRAT.IntAction → ByteArray
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_inv : ∀ {G : Type u_2} [inst : Group G] (S : Submonoid G), ↑S⁻¹ = (↑S)⁻¹
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.restrict_eigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), LinearMap.restrict f ⋯ = μ • LinearMap.id
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α], Function.Injective TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.IsIrreducible.nontrivial' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} (P : RootPairing ι R M N)
  [self : P.IsIrreducible], Nontrivial N
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize₀ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{0, 0, v, u} C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Data.Nat.ModEq
/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq`  -/
Nat.ModEq.cancel_left_of_coprime : ∀ {m a b c : ℕ}, m.gcd c = 1 → c * a ≡ c * b [MOD m] → a ≡ b [MOD m]
-- Mathlib.Tactic.Linter.OldObtain
/-- The `oldObtain` linter: see docstring above  -/
_private.Mathlib.Tactic.Linter.OldObtain.0.Mathlib.Linter.Style.oldObtainLinter : Lean.Linter
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The zeroth index  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀ : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} →
          CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ →
            (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_1 → ι
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Constructs a simple continued fraction without fractional part.  -/
SimpContFract.ofInteger : {α : Type u_1} → [inst : One α] → α → SimpContFract α
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_append_of_containsKey_left_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = false →
    Std.Internal.List.replaceEntry k v (l ++ l') = l ++ Std.Internal.List.replaceEntry k v l'