mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_of_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [hg : HomotopicalAlgebra.WeakEquivalence g]
  [hfg : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)],
  HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.FieldTheory.PrimitiveElement
/-- **Primitive element theorem**: a finite separable field extension `E` of `F` has a
primitive element, i.e. there is an `α ∈ E` such that `F⟮α⟯ = (⊤ : Subalgebra F E)`.  -/
Field.exists_primitive_element : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [Algebra.IsSeparable F E], ∃ α, F⟮α⟯ = ⊤
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.instSupSet : {α : Type u_1} → [LE α] → [SupSet α] → SupSet (WithBot α)
-- Init.Data.Dyadic.Basic
Dyadic.add_mul : ∀ (x y z : Dyadic), (x + y) * z = x * z + y * z
-- Mathlib.Analysis.Convex.Topology
convex_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E}, Convex 𝕜 ((closedConvexHull 𝕜) s)
-- Mathlib.Logic.Encodable.Basic
/-- An encodable type has decidable equality. Not set as an instance because this is usually not the
best way to infer decidability.  -/
Encodable.decidableEqOfEncodable : (α : Type u_3) → [Encodable α] → DecidableEq α
-- Lean.Meta.Tactic.Ext
/-- Key in the discrimination tree,
for the type in which the extensionality theorem holds.
 -/
Lean.Meta.Ext.ExtTheorem.keys : Lean.Meta.Ext.ExtTheorem → Array Lean.Meta.DiscrTree.Key
-- Init.Data.Ord.SInt
Int16.instLawfulEqOrd : Std.LawfulEqOrd Int16
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.transGen_oneStep_of_isDershowitzMannaLT : ∀ {α : Type u_1} [inst : Preorder α] {M N : Multiset α},
  M.IsDershowitzMannaLT N → Relation.TransGen Multiset.OneStep✝ M N
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- For all nonzero `n ∈ S`, there exists a primitive `n`-th root of unity in `B`.  -/
IsCyclotomicExtension.exists_isPrimitiveRoot : ∀ {S : Set ℕ} (A : Type u) (B : Type v) {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B}
  [self : IsCyclotomicExtension S A B] {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformContinuous_ofUniformFun : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  UniformContinuous fun f => (UniformOnFun.ofFun 𝔖) (UniformFun.toFun f)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.cons_left_injective : ∀ {α : Type u} (s : Stream'.Seq α), Function.Injective fun x => Stream'.Seq.cons x s
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.splitCenterBox.eq_1 : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι),
  I.splitCenterBox s =
    { lower := s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower,
      upper := s.piecewise I.upper fun i => (I.lower i + I.upper i) / 2, lower_lt_upper := ⋯ }
-- Lean.DocString.Extension
Lean.ElabBlock.deferred.inj : ∀ {index index_1 : ℕ}, Lean.ElabBlock.deferred index = Lean.ElabBlock.deferred index_1 → index = index_1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Created : Lean.Lsp.FileChangeType
-- Mathlib.Algebra.Lie.SemiDirect
/-- The semi-direct sum of two Lie algebras `K` and `L` over `R`, relative to a Lie algebra homomorphism
`ψ: L → LieDerivation R K K`. As a set, it is just `K × L`, however the Lie bracket is twisted by
`ψ`.
 -/
LieAlgebra.SemiDirectSum : {R : Type u_1} →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          (L : Type u_3) →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ LieDerivation R K K) → Type (max u_2 u_3)
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_sub : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
-- Mathlib.Analysis.Convex.Intrinsic
mem_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P} {x : P},
  x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y ∈ frontier (Subtype.val ⁻¹' s), ↑y = x
-- Mathlib.Order.Hom.BoundedLattice
/-- The function preserves the bottom element. The preferred spelling is `map_bot`.  -/
BoundedLatticeHom.map_bot' : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (self : BoundedLatticeHom α β), self.toFun ⊥ = ⊥
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_iff : ∀ {x y z : ENNReal}, y ≠ 0 → y ≠ ⊤ → (x / y ≤ z ↔ x ≤ z * y)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.neg P 1 = W'.negY P
-- Mathlib.Algebra.DirectSum.Idempotents
DirectSum.isIdempotentElem_idempotent : ∀ {R : Type u_1} {I : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq I] (V : I → Ideal R)
  [inst_2 : DirectSum.Decomposition V] (i : I), IsIdempotentElem (DirectSum.idempotent V i)
-- Mathlib.Algebra.Opposites
AddOpposite.unop_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : αᵃᵒᵖ), AddOpposite.unop a = 0 ↔ a = 0
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_ofBoolListBE : ∀ {bs : List Bool} {i : ℕ}, (BitVec.ofBoolListBE bs).getMsbD i = bs.getD i false
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq : ∀ {A : Type u_4} {B : Type u_5} {inst : CommSemiring A} {inst_1 : CommSemiring B} {inst_2 : Algebra A B} {p : Ideal A}
  {inst_3 : p.IsPrime} {P : Ideal B} {inst_4 : P.IsPrime} {inst_5 : P.LiesOver p}
  {inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)}
  [self : Localization.AtPrime.IsLiesOverAlgebra p P],
  algebraMap (Localization.AtPrime p) (Localization.AtPrime P) = Localization.localRingHom p P (algebraMap A B) ⋯
-- Mathlib.GroupTheory.Perm.Cycle.Basic
zpowersEquivZPowers.congr_simp : ∀ {G : Type u_1} [inst : Group G] {x y : G} [inst_1 : Finite G] (h : orderOf x = orderOf y),
  zpowersEquivZPowers h = zpowersEquivZPowers h
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δ₀Functor_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1))
  (X : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.obj F).obj X = F.obj X.succ
-- Mathlib.Order.RelIso.Basic
/-- See Note [custom simps projection].  -/
RelIso.Simps.symm_apply : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → β → α
-- Init.Data.SInt.Bitwise
Int32.toInt64_or : ∀ (a b : Int32), (a ||| b).toInt64 = a.toInt64 ||| b.toInt64
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_vadd : ∀ (x : ℝ) (z : UpperHalfPlane), ↑(x +ᵥ z) = ↑x + ↑z
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g • x) ∂μ
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {θ : Δ ⟶ Δ'} {Δ'' : SimplexCategory}
  {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [inst_3 : CategoryTheory.Epi e]
  [inst_4 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
    ∀ {Z : C} (h : AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ' ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A)
          (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) h) =
        CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ')
              (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e))
            h)
-- Mathlib.Order.Extension.Well
IsWellFounded.wellOrderExtension.isWellOrder_lt : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r], IsWellOrder α LT.lt
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightId_inv_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapRightId R L).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Init.SimpLemmas
bne_self_eq_false' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (a != a) = false
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.mk.inj : ∀ {expr relevantArgs expr_1 relevantArgs_1 : Lean.Expr},
  { expr := expr, relevantArgs := relevantArgs } = { expr := expr_1, relevantArgs := relevantArgs_1 } →
    expr = expr_1 ∧ relevantArgs = relevantArgs_1
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.snd` as a linear map.  -/
WithLp.sndₗ : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [inst : Semiring 𝕜] →
          [inst_1 : AddCommGroup α] →
            [inst_2 : AddCommGroup β] → [inst_3 : Module 𝕜 α] → [inst_4 : Module 𝕜 β] → WithLp p (α × β) →ₗ[𝕜] β
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.of_subsingleton : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : Fintype I] [Subsingleton R],
  CompleteOrthogonalIdempotents e
-- Lean.Structure
Lean.instInhabitedStructureState.default : Lean.StructureState✝
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.whiskerRight_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {y z : B} {g g' : y ⟶ z} (h : g = g') {x : B} {f f' : x ⟶ y}
  (η : f ⟶ f'),
  CategoryTheory.Bicategory.whiskerRight η g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η g') (CategoryTheory.eqToHom ⋯))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey! k = m.getKey! k
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePoint_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), ↑(s.restrict S hS).mongePoint = s.mongePoint
-- Init.Grind.Norm
Lean.Grind.ite_false_true : ∀ {p : Prop} {x : Decidable p}, (if p then False else True) = ¬p
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] [inst_2 : NonAssocRing T]
  (s : Subring R) (g : S →+* T) (f : R →+* S), Subring.map g (Subring.map f s) = Subring.map (g.comp f) s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.exists_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Y : C}
  (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S),
  CategoryTheory.CategoryStruct.comp g₁ f₁ = b →
    CategoryTheory.CategoryStruct.comp g₂ f₂ = b →
      CategoryTheory.CategoryStruct.comp g₃ f₃ = b →
        ∃ φ,
          CategoryTheory.CategoryStruct.comp φ h.p₁ = g₁ ∧
            CategoryTheory.CategoryStruct.comp φ h.p₂ = g₂ ∧ CategoryTheory.CategoryStruct.comp φ h.p₃ = g₃
-- Mathlib.Data.Int.Init
Int.succ_neg_succ : ∀ (a : ℤ), (-a.succ).succ = -a
-- Mathlib.Logic.Basic
not_iff_comm : ∀ {a b : Prop}, (¬a ↔ b) ↔ (¬b ↔ a)
-- Init.Data.Array.Basic
Array.getElem?_toList : ∀ {α : Type u} {xs : Array α} {i : ℕ}, xs.toList[i]? = xs[i]?
-- Mathlib.Order.Grade
/-- An `𝕆`-graded order where minimal elements have minimal grades and maximal elements have maximal
grades.  -/
GradeBoundedOrder : (𝕆 : Type u_5) → (α : Type u_6) → [Preorder 𝕆] → [Preorder α] → Type (max u_5 u_6)
-- Mathlib.Order.RelClasses
/-- The lexicographical order of well-founded relations is well-founded.  -/
WellFounded.psigma_lex : ∀ {α : Sort u_1} {β : α → Sort u_2} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop},
  WellFounded r → (∀ (x : α), WellFounded (s x)) → WellFounded (PSigma.Lex r s)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isoMk_inv : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N)
  (hφ :
    ∀ (r : R),
      CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom),
  (ModuleCat.isoMk φ hφ).inv = ModuleCat.homMk φ.inv ⋯
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has limits of shape `J` if there exists a limit for every functor `F : J ⥤ C`.  -/
CategoryTheory.Limits.HasLimitsOfShape : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkNoNatZeroDivInst? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Init.Data.SInt.Basic
/-- Signed 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value.
 -/
Int16 : Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.mk.inj : ∀ {startLine endLine : ℕ} {kind? : Option Lean.Lsp.FoldingRangeKind} {startLine_1 endLine_1 : ℕ}
  {kind?_1 : Option Lean.Lsp.FoldingRangeKind},
  { startLine := startLine, endLine := endLine, kind? := kind? } =
      { startLine := startLine_1, endLine := endLine_1, kind? := kind?_1 } →
    startLine = startLine_1 ∧ endLine = endLine_1 ∧ kind? = kind?_1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₀₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₀ a) (Sum3.in₂ c)
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isDenseEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → IsDenseEmbedding f
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_div₀' : ∀ {α : Type u_10} {β : Type u_11} [inst : Group α] [inst_1 : GroupWithZero β] [inst_2 : MulDistribMulAction α β] (g : α)
  (x y : β), g • (x / y) = g • x / g • y
-- Mathlib.GroupTheory.Congruence.Defs
Con.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : SizeOf M] (toSetoid : Setoid M)
  (mul' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)),
  sizeOf { toSetoid := toSetoid, mul' := mul' } = 1 + sizeOf toSetoid
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.rel_of_left : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it it' : Std.IterM m β},
  it'.internalState.it₁.finitelyManySteps.Rel it.internalState.it₁.finitelyManySteps →
    Std.Iterators.Types.Flatten.Rel✝ α β m it' it
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomial =
    P 1 ^ 2 * P 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 2 -
      (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 + W'.a₄ * P 0 * P 2 ^ 2 + W'.a₆ * P 2 ^ 3)
-- Aesop.Forward.State
/-- Partial matches associated with a particular slot instantiation. An entry
`s ↦ e ↦ (ms, hs)` indicates that for the instantiation `e` of slot `s`, we have
partial matches `ms` and hypotheses `hs`.  -/
Aesop.InstMap : Type
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.extraction_of_frequently_atTop : ∀ {P : ℕ → Prop}, (∃ᶠ (n : ℕ) in Filter.atTop, P n) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
-- Mathlib.Data.Multiset.Sym
Multiset.dedup_sym2 : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.sym2.dedup = m.dedup.sym2
-- Mathlib.Analysis.Normed.Group.Ultra
/-- **Alias** of `IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty`.

---

Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find `i ∈ t` such that
`‖∏ j in t, f j‖ ≤ ‖f i‖`.
 -/
IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {t : Finset ι},
  t.Nonempty → ∀ (f : ι → M), ∃ i ∈ t, ‖∏ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.Data.Finset.Density
Finset.dens_union_le : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s ∪ t).dens ≤ s.dens + t.dens
-- Std.Time.Zoned.TimeZone
/-- A zero `Offset` representing UTC (no offset).
 -/
Std.Time.TimeZone.Offset.zero : Std.Time.TimeZone.Offset
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.pathGraph_preconnected : ∀ (n : ℕ), (SimpleGraph.pathGraph n).Preconnected
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_μ_δ : ∀ {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] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') (X Y : C),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
      (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) =
    CategoryTheory.CategoryStruct.id (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The model of `S` over a `R₀` that contains the coefficients of `P` is `R₀[X]` quotiented by the
same relations.  -/
Algebra.Presentation.ModelOfHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {P : Algebra.Presentation R S ι σ} →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] → [P.HasCoeffs R₀] → Type (max (max u_3 u_5) u_5 u_3)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Lebesgue dominated convergence theorem for filters with a countable basis  -/
MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} {l : Filter ι}
  [l.IsCountablyGenerated] {fs : ι → α → E} {f : α → E} (bound : α → ℝ),
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (fs n) μ) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) l (nhds (f a))) →
          Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) l (nhds (MeasureTheory.setToFun μ T hT f))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.isStarNormal : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → IsStarNormal A
-- Mathlib.Topology.Algebra.Algebra
/-- The identity map as a continuous algebra homomorphism.  -/
ContinuousAlgHom.id : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → A →A[R] A
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.restrictScalars : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.IsIntegral R S]
  {p : Ideal T}, Algebra.ZariskisMainProperty S p → Algebra.ZariskisMainProperty R p
-- Mathlib.Tactic.Order
/-- Finds a contradictory `≠`-fact whose `.lhs` and `.rhs` belong to the same strongly connected
component in the `≤`-graph, implying they must be equal, and then uses it to derive `False`.  -/
Mathlib.Tactic.Order.findContradictionWithNe : Mathlib.Tactic.Order.Graph → Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM (Option Lean.Expr)