mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.is3Clique_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)},
  (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 s ↔
    ∃ x ∈ t, SimpleGraph.TripartiteFromTriangles.toTriangle x = s
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNormedRing : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [StarOrderedRing A] → {n : Type u_2} → [Fintype n] → [DecidableEq n] → NormedRing (CStarMatrix n n A)
-- Init.Data.String.Lemmas.Basic
String.slice_startPos : ∀ {s : String} {p : s.Pos}, s.slice s.startPos p ⋯ = s.sliceTo p
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Any function `C → A` lifts to a functor `C ⥤ Codiscrete A`.  -/
CategoryTheory.Codiscrete.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} → (C → A) → CategoryTheory.Functor C (CategoryTheory.Codiscrete A)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A binary convex combination with weight 0 on the first point returns the second point.  -/
Convexity.convexCombPair_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {x y : M}, Convexity.convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y
-- Mathlib.Topology.Homeomorph.Defs
/-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism.  -/
Equiv.toHomeomorphOfContinuousOpen : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (e : X ≃ Y) → Continuous ⇑e → IsOpenMap ⇑e → X ≃ₜ Y
-- Std.Sync.Barrier
Std.Barrier.numThreads : Std.Barrier → ℕ
-- Mathlib.Computability.DFA
DFA.eval_nil : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.eval [] = M.start
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Any category with pullbacks and binary products, has equalizers.  -/
CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasEqualizers C
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.subordinateOrthonormalBasisIndex.congr_simp : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V V_1 : ι → Submodule 𝕜 E} (e_V : V = V_1)
  (hV : DirectSum.IsInternal V) (a a_1 : Fin n),
  a = a_1 →
    ∀ (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
      DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' =
        DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ a_1 ⋯
-- Mathlib.Order.Lattice
le_sup_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
-- Lean.CoreM
Lean.Core.State.mk.inj : ∀ {env : Lean.Environment} {nextMacroScope : Lean.MacroScope} {ngen : Lean.NameGenerator}
  {auxDeclNGen : Lean.DeclNameGenerator} {traceState : Lean.TraceState} {cache : Lean.Core.Cache}
  {messages : Lean.MessageLog} {infoState : Lean.Elab.InfoState}
  {snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)} {env_1 : Lean.Environment}
  {nextMacroScope_1 : Lean.MacroScope} {ngen_1 : Lean.NameGenerator} {auxDeclNGen_1 : Lean.DeclNameGenerator}
  {traceState_1 : Lean.TraceState} {cache_1 : Lean.Core.Cache} {messages_1 : Lean.MessageLog}
  {infoState_1 : Lean.Elab.InfoState} {snapshotTasks_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { env := env, nextMacroScope := nextMacroScope, ngen := ngen, auxDeclNGen := auxDeclNGen, traceState := traceState,
        cache := cache, messages := messages, infoState := infoState, snapshotTasks := snapshotTasks } =
      { env := env_1, nextMacroScope := nextMacroScope_1, ngen := ngen_1, auxDeclNGen := auxDeclNGen_1,
        traceState := traceState_1, cache := cache_1, messages := messages_1, infoState := infoState_1,
        snapshotTasks := snapshotTasks_1 } →
    env = env_1 ∧
      nextMacroScope = nextMacroScope_1 ∧
        ngen = ngen_1 ∧
          auxDeclNGen = auxDeclNGen_1 ∧
            traceState = traceState_1 ∧
              cache = cache_1 ∧ messages = messages_1 ∧ infoState = infoState_1 ∧ snapshotTasks = snapshotTasks_1
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.map_maximalIdeal_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [IsLocalHom f],
  Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The multiplicative homomorphism underlying a `LocalizationMap`.  -/
Submonoid.LocalizationMap.toMulHom : {M : Type u_1} →
  [inst : CommMonoid M] → {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → M →ₙ* N
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.negPolynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R),
  W'.negPolynomial = -Polynomial.X - Polynomial.C (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃)
-- Mathlib.Topology.Sheaves.Module
TopologicalSpace.Opens.sheafRestrictSheafEquivOver.eq_1 : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : TopologicalSpace.Opens ↑X),
  U.sheafRestrictSheafEquivOver = U.overPullbackSheafEquivOver.isoCompInverse.symm
-- Mathlib.Algebra.DirectSum.Internal
/-- The semiring `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instSemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] → [AddSubmonoidClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → Semiring ↥(A 0)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_zero_mul : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : AddZeroClass ι]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] (a b : A 0),
  (DirectSum.of A 0) (a * b) = (DirectSum.of A 0) a * (DirectSum.of A 0) b
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_map_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.map α).map f).fiber =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((α.app Y.base).toFunctor.map f.fiber)
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  a ∈ m.insert k → (k == a) = false → a ∈ m
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.move p k₁ k₂ q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_1 p k₁ k₂ q
-- Mathlib.Topology.Algebra.Constructions
AddUnits.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [T2Space M], T2Space (AddUnits M)
-- Mathlib.Tactic.FunProp.Types
/-- theorem name  -/
Mathlib.Meta.FunProp.GeneralTheorem.thmName : Mathlib.Meta.FunProp.GeneralTheorem → Lean.Name
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {f : α ⊕ β → M} {a b : M}, HasSum (f ∘ Sum.inl) a → HasSum (f ∘ Sum.inr) b → HasSum f (a + b)
-- Init.MetaTypes
/-- If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded.
 -/
Lean.Meta.DSimp.Config.unfoldPartialApp : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication from the right between graded components distributes with respect to
addition.  -/
DirectSum.GNonUnitalNonAssocSemiring.mul_add : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : Add ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b c : A j),
  GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- The Stone-Weierstrass approximation theorem, `RCLike` version, that a star subalgebra `A` of
`C(X, 𝕜)`, where `X` is a compact topological space and `RCLike 𝕜`, is dense if it separates
points.  -/
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  (A : StarSubalgebra 𝕜 C(X, 𝕜)), A.SeparatesPoints → A.topologicalClosure = ⊤
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
CategoryTheory.isSheaf_coherent : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C]
  (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      CategoryTheory.EffectiveEpiFamily X π →
        CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π)
-- Init.Data.List.Basic
/-- List membership, typically accessed via the `∈` operator.

`a ∈ l` means that `a` is an element of the list `l`. Elements are compared according to Lean's
logical equality.

The related function `List.elem` is a Boolean membership test that uses a `BEq α` instance.

Examples:
* `a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z`
 -/
List.Mem : {α : Type u} → α → List α → Prop
-- Mathlib.Order.ModularLattice
Disjoint.disjoint_sup_left_of_disjoint_sup_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderBot α] [IsModularLattice α],
  Disjoint b c → Disjoint a (b ⊔ c) → Disjoint (a ⊔ b) c
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} [CompactSpace ↥(D.obj i)]
  (s : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (c.π.app i))) s = 0 →
    ∃ j f, (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (D.map f))) s = 0
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The underlying morphism associated to a morphism of algebras.  -/
CategoryTheory.Monad.Algebra.Hom.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → {A B : T.Algebra} → A.Hom B → (A.A ⟶ B.A)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_nsmul : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (n : ℕ) (f : BoundedContinuousFunction α R), ⇑(n • f) = n • ⇑f
-- Mathlib.Data.Set.Function
Set.InjOn.leftInvOn_invFunOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Nonempty α],
  Set.InjOn f s → Set.LeftInvOn (Function.invFunOn f s) f s
-- Mathlib.Data.ENat.Basic
/-- Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
`ℕ → ℕ∞` is `Nat.cast`.  -/
ENat.some_eq_natCast : WithTop.some = Nat.cast
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_eval_add_inv : ∀ {R : Type u_1} [inst : CommRing R] (x y : R),
  x * y = 1 → ∀ (n : ℕ), Polynomial.eval (x + y) (Polynomial.dickson 1 1 n) = x ^ n + y ^ n
-- Mathlib.Algebra.Lie.Basis.Basic
_private.Mathlib.Algebra.Lie.Basis.Basic.0.LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top_aux : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) {y z : L},
  y ∈ LieSubalgebra.lieSpan R L (Set.range b.e) →
    z ∈ LieSubalgebra.lieSpan R L (Set.range b.f) → ⁅y, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_id : ∀ (α : Type u_2) [inst : Lattice α] [inst_1 : BoundedOrder α], ⇑(BoundedLatticeHom.id α) = id
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (i j : ℕ),
  (HomologicalComplex.alternatingConst A hOdd hEven hc).d i j = if c.Rel i j then if Even i then φ else ψ else 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.toLinearMap_congr : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] {σ₂₁ : R₂ →+* R} [inst_10 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_11 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂),
  ↑(TensorProduct.congr f g) = TensorProduct.map ↑f ↑g
-- Init.Data.Array.Lemmas
Array.mem_iff_getElem? : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs ↔ ∃ i, xs[i]? = some a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getKeyGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.Logic.Equiv.Option
Equiv.optionEquivSumPUnit_coe : ∀ {α : Type u_4} (a : α), (Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.cospanOp.match_1.splitter : (motive : CategoryTheory.Limits.WalkingCospan → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingCospan) →
    (Unit → motive none) →
      (Unit → motive (some CategoryTheory.Limits.WalkingPair.left)) →
        (Unit → motive (some CategoryTheory.Limits.WalkingPair.right)) → motive x
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.error : Lean.Lsp.MessageType
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?ₘ'.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α]
  (motive : (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun x => Ordering.lt) → Sort u_3) (a : List ((a : α) × β a))
  (a_1 : Std.DTreeMap.Internal.Cell α β fun x => Ordering.lt) (r : List ((a : α) × β a))
  (h_1 :
    (ky : α) →
      (a : Ordering.lt = Ordering.lt) →
        (y : β ky) → (a_2 : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_2))
  (h_2 :
    (a : List ((a : α) × β a)) →
      (a_2 : Std.DTreeMap.Internal.Cell α β fun x => Ordering.lt) →
        (r : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r)),
  (match Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r with
    | Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_2 => h_1 ky a y a_2
    | Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r => h_2 a a_2 r) =
    h_2 a a_1 r
-- Mathlib.Data.Part
/-- `unwrap o` gets the value at `o`, ignoring the condition. This function is unsound.  -/
Part.unwrap : {α : Type u_1} → Part α → α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instToStringMVarErrorKind : ToString Lean.Elab.Term.MVarErrorKind
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_mul_X_pow' : ∀ {R : Type u_1} [inst : Semiring R] (p : PowerSeries R) (n d : ℕ),
  (PowerSeries.coeff d) (p * PowerSeries.X ^ n) = if n ≤ d then (PowerSeries.coeff (d - n)) p else 0
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whisker_counit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.RightLift f g) {x : B} (h : x ⟶ c),
  (t.whisker h).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator h t.lift f).hom
      (CategoryTheory.Bicategory.whiskerLeft h t.counit)
-- Mathlib.Computability.Primrec.List
Primrec.list_foldl : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → σ} {h : α → σ × β → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_mul_iff_of_pos_right : ∀ {a b c : ℤ}, 0 < a → (b * a ≤ c * a ↔ b ≤ c)
-- Init.Data.List.Lemmas
/-- `simp` unfolds `headD` in terms of `head?` and `Option.getD`.  -/
List.headD_eq_head?_getD : ∀ {α : Type u_1} {a : α} {l : List α}, l.headD a = l.head?.getD a
-- Mathlib.Geometry.Polygon.Basic
/-- Converting a 3-polygon to a triangle and back yields the original polygon.  -/
Polygon.toTriangle_toPolygon : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (poly : Polygon P 3) (h : Polygon.HasNondegenerateVertices R poly),
  Affine.Triangle.toPolygon (Polygon.toTriangle R poly h) = poly
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.exists_finset_coe : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ s', ↑s' = s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨j, ⋯⟩ = c.pt
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.closure_eq_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α},
  closure s = ↑(lowerClosure s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
Complex.measurableSpace : MeasurableSpace ℂ
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- In a Galois category, every object is the sum of connected objects.  -/
CategoryTheory.PreGaloisCategory.has_decomp_connected_components : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (X : C),
  ∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticSeverity.beq : Lean.Lsp.DiagnosticSeverity → Lean.Lsp.DiagnosticSeverity → Bool
-- Mathlib.Analysis.Convex.Cone.Extension
/-- Induction step in M. Riesz extension theorem. Given a convex cone `s` in a vector space `E`,
a partially defined linear map `f : f.domain → ℝ`, assume that `f` is nonnegative on `f.domain ∩ p`
and `p + s = E`. If `f` is not defined on the whole `E`, then we can extend it to a larger
submodule without breaking the non-negativity condition.  -/
RieszExtension.step : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : PointedCone ℝ E) (f : E →ₗ.[ℝ] ℝ),
  (∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x) →
    (∀ (y : E), ∃ x, ↑x + y ∈ s) → f.domain ≠ ⊤ → ∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ico_union_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  Finset.Ico a c ⊆ Finset.Ico a b ∪ Finset.Ico b c
-- Mathlib.GroupTheory.Rank
Group.rank_congr : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [inst_2 : Group.FG G] [inst_3 : Group.FG H]
  (e : G ≃* H), Group.rank G = Group.rank H
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- If `f : α → β` is `K`-antilipschitz and `α` is nontrivial, `K` is positive.  -/
AntilipschitzWith.pos : ∀ {β : Type u_2} [inst : PseudoEMetricSpace β] {K : NNReal} {α : Type u_4} [inst_1 : EMetricSpace α] [Nontrivial α]
  {f : α → β}, AntilipschitzWith K f → 0 < K
-- Init.Data.Range.Polymorphic.Basic
Std.Rcc.le_upper_of_mem : ∀ {α : Type u} {r : Std.Rcc α} {a : α} [inst : LE α], a ∈ r → a ≤ r.upper