mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Basic
/-- Convert a `USize` to `BitVec 32`, assuming that the system bit-width is 32.

This operation is intended for proof purposes.
 -/
USize.toBitVec32 : USize → System.Platform.numBits = 32 → BitVec 32
-- Init.Data.List.Lex
List.lt_iff_exists : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α},
  l₁ < l₂ ↔
    l₁ = List.take l₁.length l₂ ∧ l₁.length < l₂.length ∨
      ∃ i, ∃ (h₁ : i < l₁.length) (h₂ : i < l₂.length), (∀ (j : ℕ) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.triangle : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  [inst_6 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (X₁ X₃ : CategoryTheory.GradedObject I C) [inst_7 : X₁.HasTensor X₃]
  [inst_8 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit).HasTensor X₃]
  [inst_9 :
    X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X₃)]
  [inst_10 : X₁.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.Monoidal.tensorUnit X₃]
  [inst_11 : X₁.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.Monoidal.tensorUnit X₃],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.associator X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit X₃).hom
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁)
        (CategoryTheory.GradedObject.Monoidal.leftUnitor X₃).hom) =
    CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.rightUnitor X₁).hom
      (CategoryTheory.CategoryStruct.id X₃)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
jacobiTheta_T_sq_smul : ∀ (τ : UpperHalfPlane), jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite : ∀ (cond : Bool) {a b c : Bool}, (bif cond then !bif cond then a else b else c) = bif cond then !a else c
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.ofList l cmp).getKey! k' = k
-- Mathlib.Order.Atoms
IsSimpleOrder.instIsCoatomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsCoatomistic α
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.one_antipode : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.HopfObj.antipode =
    CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Horizontal and vertical composition of squares commutes.  -/
CategoryTheory.Bicategory.rightAdjointSquare.comp_hvcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {r₁ : b ⟶ a} {r₂ : c ⟶ b} {r₃ : e ⟶ d} {r₄ : f ⟶ e} {r₅ : y ⟶ x} {r₆ : z ⟶ y}
  (α : CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₃)
  (β : CategoryTheory.CategoryStruct.comp r₂ h₁ ⟶ CategoryTheory.CategoryStruct.comp k₁ r₄)
  (γ : CategoryTheory.CategoryStruct.comp r₃ g₂ ⟶ CategoryTheory.CategoryStruct.comp h₂ r₅)
  (δ : CategoryTheory.CategoryStruct.comp r₄ h₂ ⟶ CategoryTheory.CategoryStruct.comp k₂ r₆),
  CategoryTheory.Bicategory.rightAdjointSquare.comp α β γ δ =
    CategoryTheory.Bicategory.rightAdjointSquare.hcomp (CategoryTheory.Bicategory.rightAdjointSquare.vcomp α γ)
      (CategoryTheory.Bicategory.rightAdjointSquare.vcomp β δ)
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_sub : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a - b) = ISize.ofBitVec a - ISize.ofBitVec b
-- Mathlib.Computability.Primrec.Basic
Primrec₂.swap : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, Primrec₂ f → Primrec₂ (Function.swap f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α},
  Std.DTreeMap.Const.get? (t.erase k) k = none
-- Mathlib.Probability.Kernel.Composition.Comp
/-- Composition of kernels is associative.  -/
ProbabilityTheory.Kernel.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (ξ : ProbabilityTheory.Kernel γ δ)
  (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β), (ξ.comp η).comp κ = ξ.comp (η.comp κ)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ), S.ofUnits = Submonoid.map (Units.coeHom M) S.toSubmonoid
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.IsPath
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.brecOn.go : {motive_1 : Lean.Meta.Match.Pattern → Sort u} →
  {motive_2 : List Lean.Meta.Match.Pattern → Sort u} →
    (t : Lean.Meta.Match.Pattern) →
      ((t : Lean.Meta.Match.Pattern) → t.below → motive_1 t) →
        ((t : List Lean.Meta.Match.Pattern) → Lean.Meta.Match.Pattern.below_1 t → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.Algebra.Group.Action.Defs
AddCommute.vadd_right_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : AddGroup G] {g : G} [inst_1 : Add H] [inst_2 : AddAction G H]
  [VAddCommClass G H H] [VAddAssocClass G H H] {a b : H}, AddCommute a (g +ᵥ b) ↔ AddCommute a b
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.nsmul_index_mem : ∀ {G : Type u_6} [inst : AddGroup G] (H : AddSubgroup G) [H.Normal] (g : G), H.index • g ∈ H
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.bot : ∀ {G : Type u_3} [inst : Group G], ⊥.FG
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.extractBind.extract? : (Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)) →
  Lean.Expr → Lean.MetaM (Option Lean.Elab.Term.ExtractMonadResult)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_le_mul_of_nonpos_right : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a ≤ b → c ≤ 0 → b * c ≤ a * c
-- Mathlib.CategoryTheory.Filtered.Small
/-- All steps of building the abstract filtered closure together with the realization function,
as a function of `ℕ`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {α : Type w} → (α → C) → ℕ → (t : Type (max v w)) × (t → C)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsUnit.multisetProd_iff : ∀ {M : Type u_4} [inst : CommMonoid M] {s : Multiset M}, IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs s c₁ c₂) = 1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_push : ∀ {m n : ℤ}, m < n → (m...n).toArray = (m...n - 1).toArray.push (n - 1)
-- Mathlib.CategoryTheory.CatCommSq
/-- `CatCommSq T L R B` expresses that there is a 2-commutative square of functors, where
the functors `T`, `L`, `R` and `B` are respectively the left, top, right and bottom functors
of the square.  -/
CategoryTheory.CatCommSq : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                CategoryTheory.Functor C₁ C₂ →
                  CategoryTheory.Functor C₁ C₃ →
                    CategoryTheory.Functor C₂ C₄ → CategoryTheory.Functor C₃ C₄ → Type (max u_1 v_4)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The `f` and `h` in Weierstrass preparation theorem are equal
to `PowerSeries.weierstrassDistinguished` and `PowerSeries.weierstrassUnit`.  -/
PowerSeries.IsWeierstrassFactorization.unique : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A},
  g.IsWeierstrassFactorization f h →
    ∀ (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0),
      f = g.weierstrassDistinguished hg ∧ h = g.weierstrassUnit hg
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.monoidAlgebraFree_map : ∀ (R : Type u) [inst : Ring R] {X Y : Type u} (f : X ⟶ Y),
  (ModuleCat.monoidAlgebraFree R).map f =
    ModuleCat.ofHom (MonoidAlgebra.mapDomainLinearMap R R ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Lean.Util.ParamMinimizer
/-- The final parameter bitmask.  -/
Lean.Util.ParamMinimizer.Result.paramMask : Lean.Util.ParamMinimizer.Result → Array Bool
-- Aesop.Search.Queue
Aesop.BestFirstQueue.init : Aesop.BestFirstQueue
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.tsum_mul_le_mul_norm' : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
  p.toReal.HolderConjugate q.toReal → ∀ (f : ↥(lp E p)) (g : ↥(lp E q)), ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddMonoid.toAddMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedAddMonoid E] → AddMonoid E
-- Mathlib.Tactic.Positivity.Finset
/-- Extension for `Fintype.card`. `Fintype.card α` is positive if `α` is nonempty.  -/
Mathlib.Meta.Positivity.evalFintypeCard : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a function `f`, the smallest congruence relation containing the binary relation on `f`'s
image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)`
by a congruence relation `c`.'  -/
Con.mapGen : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → {c : Con M} → (M → N) → Con N
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicative_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] (f : α →+ β) (a : Multiplicative α),
  (AddMonoidHom.toMultiplicative f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addCommMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCommMonoid α] → AddCommMonoid (Matrix m n α)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_zero_of_not_linearIndependent_rows : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] [IsDomain R]
  {A : Matrix m m R}, (¬LinearIndependent R fun i => A i) → A.det = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_id : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.map (RingHom.id R) = W
-- Aesop.Util.Basic
Aesop.setThe : (σ : Type u_1) → {m : Type u_1 → Type u_2} → [MonadStateOf σ m] → σ → m PUnit.{u_1 + 1}
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.const : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (x : β), IsCauSeq abv fun x_1 => x
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- Suppose `f : S →ₐ[R] T` is an `R`-algebra homomorphism with `S` integral and `T` of finite type,
such that the induced map `S[1/g] → T[1/g]` is surjective for some `g : S`.
Then for any prime `p` of `R` such that `1 ⊗ₜ g` is invertible in `κ(p) ⊗ S`,
there exists `r ∉ p` such that `T[1/r]` is finite over `R[1/r]`.  -/
Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ : ∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.FiniteType R T] [Algebra.IsIntegral R S] (f : S →ₐ[R] T)
  (g : S),
  Function.Surjective ⇑(Localization.awayMapₐ f g) →
    ∀ (p : Ideal R) [inst_7 : p.IsPrime],
      IsUnit (1 ⊗ₜ[R] g) → ∃ r ∉ p, (Localization.awayMapₐ (Algebra.ofId R T) r).Finite
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_inv_app : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (X : C₀),
  (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv.app X =
    CategoryTheory.CategoryStruct.comp (F₀₂.map (adj₀₁.unit.app X))
      (CategoryTheory.CategoryStruct.comp (F₀₂.map (G₁₀.map (adj₁₂.unit.app (F₀₁.obj X))))
        (CategoryTheory.CategoryStruct.comp (F₀₂.map (e₀₁₂.hom.app (F₁₂.obj (F₀₁.obj X))))
          (adj₀₂.counit.app (F₁₂.obj (F₀₁.obj X)))))
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- **Alias** of `ProperCone.hyperplane_separation'`.

---

Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones.  -/
ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [CompleteSpace E] {x₀ : E}
  (C : ProperCone ℝ E), x₀ ∉ C → ∃ y, (∀ x ∈ C, 0 ≤ inner ℝ x y) ∧ inner ℝ x₀ y < 0
-- Mathlib.Algebra.Quaternion
Quaternion.coe_commutes : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (a : Quaternion R), ↑r * a = a * ↑r
-- Mathlib.Data.PNat.Basic
instAddLeftReflectLEPNat : AddLeftReflectLE ℕ+
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : TopologicalSpace N]
  {M : Type u_6} [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [inst_4 : IsTopologicalAddGroup M]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.AbsolutelyContinuous w → (-v).AbsolutelyContinuous w
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_def : ∀ {R : Type u_1} [inst : Semiring R] (k m n : ℕ) (u v w : R),
  Polynomial.trinomial k m n u v w =
    Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mkAlgHom_C : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  (RingCon.mkₐ R (DividedPowerAlgebra.ringCon R M)) (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- To construct an isomorphism of cocones over the walking span,
it suffices to construct an isomorphism
of the cocone points and check it commutes with the legs from `left` and `right`.  -/
CategoryTheory.Limits.WalkingSpan.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      {s t : CategoryTheory.Limits.Cocone F} →
        (i : s.pt ≅ t.pt) →
          CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingCospan.left) i.hom =
              t.ι.app CategoryTheory.Limits.WalkingCospan.left →
            CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingCospan.right) i.hom =
                t.ι.app CategoryTheory.Limits.WalkingCospan.right →
              (s ≅ t)
-- Aesop.Index.RulePattern
/-- A rule pattern index. Maps expressions `e` to rule patterns that likely
unify with `e`.  -/
Aesop.RulePatternIndex : Type
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.NormalizedMooreComplex.objX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C), AlgebraicTopology.NormalizedMooreComplex.objX X 0 = ⊤
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- To prove something for an arbitrary `MemLp` function in a second countable
Borel normed group, it suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in the `Lᵖ` space for which the property holds is closed.
* the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`).
 -/
MeasureTheory.MemLp.induction : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ (motive : (α → E) → Prop),
      (∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → motive (s.indicator fun x => c)) →
        (∀ ⦃f g : α → E⦄,
            Disjoint (Function.support f) (Function.support g) →
              MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → motive f → motive g → motive (f + g)) →
          IsClosed {f | motive ↑↑f} →
            (∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MeasureTheory.MemLp f p μ → motive f → motive g) →
              ∀ ⦃f : α → E⦄, MeasureTheory.MemLp f p μ → motive f
-- Mathlib.Control.Monad.Cont
MonadCont.callCC : {m : Type u → Type v} → [self : MonadCont m] → {α β : Type u} → (MonadCont.Label α m β → m α) → m α
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.coeFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [inst_12 : ContMDiffRing I (↑⊤) R] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              CoeFun ↑((smoothSheafCommRing IM I M R).presheaf.obj U) fun x =>
                                                ↥(Opposite.unop U) → R
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.intersecting_iff_eq_empty_of_subsingleton : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [Subsingleton α] (s : Set α), s.Intersecting ↔ s = ∅
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The natural transformation `τ`, seen as a natural transformation from `OppositeShift.functor F A`
to `OppositeShift.functor G A`..
 -/
CategoryTheory.OppositeShift.natTrans : {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] →
        (A : Type u_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                {F G : CategoryTheory.Functor C D} →
                  (F ⟶ G) → (CategoryTheory.OppositeShift.functor A G ⟶ CategoryTheory.OppositeShift.functor A F)
-- Lean.Server.Completion.CompletionCollectors
/-- Truncate the given identifier and make sure it has length `≤ newLength`.
This function assumes `id` does not contain `Name.num` constructors.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.truncate : Lean.Name → ℕ → Lean.Name
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_eq_iSup_biInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  Filter.bliminf u f p = ⨆ s ∈ f, ⨅ b, ⨅ (_ : p b ∧ b ∈ s), u b
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.horn.spineId_arrow_coe : ∀ {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) (j : Fin (n + 2)),
  ↑((SSet.horn.spineId i h₀ hₙ).arrow j) = (SSet.stdSimplex.spineId (n + 2)).arrow j
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The packing number of a set `A` for radius `2 * ε` is at most the external covering number
of `A` for radius `ε`.  -/
Metric.packingNumber_two_mul_le_externalCoveringNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.packingNumber (2 * ε) A ≤ Metric.externalCoveringNumber ε A
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  Function.Injective ⇑e
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.collectArgs : {pu : Lean.Compiler.LCNF.Purity} → Array (Lean.Compiler.LCNF.Arg pu) → Lean.FVarIdHashSet → Lean.FVarIdHashSet
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_update_stack : ∀ {a b c d d' : List Turing.PartrecToTM2.Γ'},
  Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.stack d' =
    Turing.PartrecToTM2.K'.elim a b c d'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.δ_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.mappingCone.inl φ) =
    CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ (CochainComplex.mappingCone.inr φ))
-- Mathlib.Control.Applicative
Functor.Comp.applicative_comp_id : ∀ {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F], Functor.Comp.instApplicativeComp = AF
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_mul : ∀ (a b : BitVec 16), { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₁_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  CategoryTheory.Pretriangulated.Triangle.π₁.map f = f.hom₁
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- Families at which power series can be consistently evaluated  -/
MvPowerSeries.HasEval : {σ : Type u_1} → {S : Type u_3} → [CommRing S] → [TopologicalSpace S] → (σ → S) → Prop