mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.notMem_commonNeighbors_right : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), w ∉ G.commonNeighbors v w
-- Std.Sat.AIG.Basic
_private.Std.Sat.AIG.Basic.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match elem : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 elem) =
    h_3 lhs rhs ⋯
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_one_right : ∀ {R : Type u} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), SemiconjBy a (-1) (-1)
-- Mathlib.Topology.FiberBundle.Basic
/-- Trivialization of a fiber bundle at a point.  -/
FiberBundle.trivializationAt : {B : Type u_2} →
  (F : Type u_3) →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        (E : B → Type u_5) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              [FiberBundle F E] → B → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.ab4OfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.AB4OfSize.{w, v, u} C
-- Std.Time.Format
/-- Parses a `String` in the `ISO8601` format and returns a `DateTime`.
 -/
Std.Time.DateTime.fromISO8601String : String → Except String Std.Time.DateTime
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearExpr : Type
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq_span : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R ↑(Submonoid.closure s)
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Continuous f → Continuous g → Topology.IsEmbedding (g ∘ f) → Topology.IsEmbedding f
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.mk.inj : ∀ {indent : ℕ} {children : Array (Lean.Server.WithRpcRef Lean.MessageData)} {indent_1 : ℕ}
  {children_1 : Array (Lean.Server.WithRpcRef Lean.MessageData)},
  { indent := indent, children := children } = { indent := indent_1, children := children_1 } →
    indent = indent_1 ∧ children = children_1
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing a linear map `P →ₛₗ[σ₃₄] Q` and a bilinear map `M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P` to
form a bilinear map `M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q`.

See `LinearMap.compr₂` for a version of this definition, which does not support semi-linear maps but
which does support towers of scalars.  -/
LinearMap.compr₂ₛₗ : {R : Type u_2} →
  [inst : CommSemiring R] →
    {R₂ : Type u_14} →
      {R₃ : Type u_15} →
        {R₄ : Type u_16} →
          {M : Type u_17} →
            {N : Type u_18} →
              {P : Type u_19} →
                {Q : Type u_20} →
                  [inst_1 : CommSemiring R₂] →
                    [inst_2 : CommSemiring R₃] →
                      [inst_3 : CommSemiring R₄] →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : AddCommMonoid N] →
                            [inst_6 : AddCommMonoid P] →
                              [inst_7 : AddCommMonoid Q] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R₂ N] →
                                    [inst_10 : Module R₃ P] →
                                      [inst_11 : Module R₄ Q] →
                                        {σ₁₃ : R →+* R₃} →
                                          {σ₁₄ : R →+* R₄} →
                                            {σ₂₃ : R₂ →+* R₃} →
                                              {σ₂₄ : R₂ →+* R₄} →
                                                {σ₃₄ : R₃ →+* R₄} →
                                                  [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] →
                                                    [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] →
                                                      (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →
                                                        (P →ₛₗ[σ₃₄] Q) → M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply₀' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → (μ.restrict s) t = μ (t ∩ s)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isRightDescent_inv_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_X_pow : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (n : ℕ), (Polynomial.X ^ n).aroots S = n • {0}
-- Mathlib.Data.Sym.Sym2
Sym2.mem_diagSet : ∀ {α : Type u_1} {z : Sym2 α}, z ∈ Sym2.diagSet ↔ z.IsDiag
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_xor : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (p q : ι → Prop)
  [inst_1 : DecidablePred p] [inst_2 : DecidablePred q],
  ∑ x ∈ s with Xor (p x) (q x), f x = ∑ x ∈ s with p x ∧ ¬q x, f x + ∑ x ∈ s with q x ∧ ¬p x, f x
-- Mathlib.Topology.Homotopy.Path
/-- Two paths `p₀` and `p₁` are `Path.Homotopic` if there exists a `Homotopy` between them.
 -/
Path.Homotopic : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path x₀ x₁ → Path x₀ x₁ → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cosh_sub_pi_mul_I : ∀ (z : ℂ), Complex.cosh (z - ↑Real.pi * Complex.I) = -Complex.cosh z
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instInhabited : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.ExtHashSet α)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'.congr_simp : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {inst : DecidableEq o} [inst_1 : DecidableEq o]
  [inst_2 : Zero α] (M M_1 : (i : o) → Matrix (m' i) (n' i) α),
  M = M_1 →
    ∀ (a a_1 : (i : o) × m' i),
      a = a_1 →
        ∀ (a_2 a_3 : (i : o) × n' i), a_2 = a_3 → Matrix.blockDiagonal' M a a_2 = Matrix.blockDiagonal' M_1 a_1 a_3
-- Mathlib.Analysis.Convex.Segment
lineMap_mem_openSegment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b : E) {t : 𝕜}, t ∈ Set.Ioo 0 1 → (AffineMap.lineMap a b) t ∈ openSegment 𝕜 a b
-- Mathlib.Order.Concept
Concept.intent_ofIsIntent : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) (ht : Order.IsIntent r t),
  (Concept.ofIsIntent r t ht).intent = t
-- Mathlib.Analysis.Convex.Star
/-- Alternative definition of star-convexity, using division.  -/
starConvex_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x : E} {s : Set E},
  StarConvex 𝕜 x s ↔
    ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.unbounded.injEq : ∀ {α : Type} (ch ch_1 : Std.CloseableChannel.Unbounded✝ α),
  (Std.CloseableChannel.Flavors.unbounded✝ ch = Std.CloseableChannel.Flavors.unbounded✝ ch_1) = (ch = ch_1)
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int16
-- Mathlib.Topology.Neighborhoods
nhds_bind_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, (nhds x).bind nhds = nhds x
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile : Type
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendMiddle.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length),
  c.extendMiddle k =
    { length := c.length, partSize := Function.update c.partSize k (c.partSize k + 1), partSize_pos := ⋯,
      emb := fun m =>
        if h : m = k then
          have this := ⋯;
          (fun i => Fin.cases 0 (Fin.succ ∘ c.emb k) i) ∘ Fin.cast this
        else
          have this := ⋯;
          Fin.succ ∘ c.emb m ∘ Fin.cast this,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_zsmul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℤ) (x : WittVector p R) (n : ℕ),
  WittVector.init n (m • x) = WittVector.init n (m • WittVector.init n x)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mk : {R : Type u_1} →
  [inst : LinearOrder R] →
    [inst_1 : TopologicalSpace R] →
      (toFun : R → ℝ) → Monotone toFun → (∀ (x : R), ContinuousWithinAt toFun (Set.Ici x) x) → StieltjesFunction R
-- Mathlib.Analysis.InnerProductSpace.SingularValues
/-- 7.68(a) from [axler2024]. Note that we have countably infinitely many singular values whereas there
are only dim(domain(T)) singular values in [axler2024], so we modify the statement to account for
this.
 -/
LinearMap.injective_iff_forall_lt_finrank_singularValues_pos : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F),
  Function.Injective ⇑T ↔ ∀ i < Module.finrank 𝕜 E, 0 < T.singularValues i
-- Init.Data.SInt.Bitwise
Int8.toBitVec_not : ∀ {a : Int8}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial Cᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).inverse.obj x =
    match x with
    | CategoryTheory.WithInitial.of x => Opposite.op (CategoryTheory.WithTerminal.of (Opposite.unop x))
    | CategoryTheory.WithInitial.star => Opposite.op CategoryTheory.WithTerminal.star
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- An element of the fundamental group as a quotient of homotopic paths.  -/
FundamentalGroup.toPath : {X : Type u_1} → [inst : TopologicalSpace X] → {x : X} → FundamentalGroup X x → Path.Homotopic.Quotient x x
-- Init.SimpLemmas
eq_false_of_decide : ∀ {p : Prop} {x : Decidable p}, decide p = false → p = False
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_slice_iff : ∀ {pat s : String.Slice}, s.endsWith pat = true ↔ pat.copy.toList <:+ s.copy.toList
-- Mathlib.Data.Complex.Basic
Complex.normSq_mul : ∀ (z w : ℂ), Complex.normSq (z * w) = Complex.normSq z * Complex.normSq w
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.mk.inj : ∀ {α : Type} {roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ}
  {tries : Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))} {roots_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ}
  {tries_1 : Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))},
  { roots := roots, tries := tries } = { roots := roots_1, tries := tries_1 } → roots = roots_1 ∧ tries = tries_1
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.mk : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry → Bool → Aesop.RulePatternIndex
-- Mathlib.Analysis.Convex.StdSimplex
/-- The barycenter of a standard simplex has coordinates `(Fintype.card X)⁻¹` at each index.  -/
stdSimplex.barycenter_apply : ∀ {X : Type u_2} [inst : Fintype X] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : IsStrictOrderedRing 𝕜] [inst_4 : Nonempty X] (x : X), ↑stdSimplex.barycenter x = (↑(Fintype.card X))⁻¹
-- Mathlib.Tactic.Translate.ToAdditive
/-- An attribute that tells that certain arguments of this definition are not
involved when translating.
This helps the translation heuristic by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments.  -/
Mathlib.Tactic.ToAdditive.ignoreArgsAttr : Lean.NameMapExtension (List ℕ)
-- Mathlib.Topology.Clopen
isClopen_iff_frontier_eq_empty : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s ↔ frontier s = ∅
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁_supportsStmt_mono : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {S : Finset Λ} {q₁ q₂ : Turing.TM1.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM1.stmts₁ q₂ → Turing.TM1.SupportsStmt S q₂ → Turing.TM1.SupportsStmt S q₁
-- Mathlib.Probability.Moments.CovarianceBilin
/-- The covariance operator of the measure `μ`. This is the bounded operator `F : E →L[ℝ] E`
associated to the continuous bilinear form `B : E →L[ℝ] E →L[ℝ] ℝ` such that
`B x y = ∫ z, ⟪x, z⟫ * ⟪y, z⟫ ∂μ` (see `covarianceOperator_inner`). Namely we have
`B x y = ⟪F x, y⟫`.

Note that the bilinear form `B` is the _uncentered_ covariance bilinear form associated to the
measure `µ`, which is not to be confused with the covariance bilinear form defined earlier in this
file as `covarianceBilin μ`.  -/
ProbabilityTheory.covarianceOperator : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [inst_2 : MeasurableSpace E] → [BorelSpace E] → [CompleteSpace E] → MeasureTheory.Measure E → E →L[ℝ] E
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_pair_of_ne : ∀ {x y : ZFSet.{u}}, x ≠ y → {x, y}.card = 2
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkProofs : Lean.Meta.Grind.GoalM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.ι.eq_1 : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i), SSet.horn.ι i j hij = SSet.yonedaEquiv.symm (SSet.horn.face i j hij)
-- Mathlib.Topology.Order.OrderClosed
Dense.Iio_eq_biUnion : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α]
  {s : Set α}, Dense s → ∀ (x : α), Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y
-- Std.Time.Format.Modifier
Std.Time.Modifier.Y.inj : ∀ {presentation presentation_1 : Std.Time.Year},
  Std.Time.Modifier.Y presentation = Std.Time.Modifier.Y presentation_1 → presentation = presentation_1
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.Option.instDecidableEq.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (b : Option α) → (Unit → motive none) → ((val : α) → motive (some val)) → motive b
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- Twisting by a Dirichlet character `χ` distributes over convolution.  -/
DirichletCharacter.mul_convolution_distrib : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ} (χ : DirichletCharacter R n) (f g : ℕ → R),
  LSeries.convolution ((fun x => χ ↑x) * f) ((fun x => χ ↑x) * g) = (fun x => χ ↑x) * LSeries.convolution f g
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_le_right : ∀ {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R), (A * B).rank ≤ B.rank
-- Mathlib.Topology.Basic
isOpen_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen ∅
-- Mathlib.Topology.Separation.Basic
R1Space.inf : ∀ {X : Type u_3} {t₁ t₂ : TopologicalSpace X}, R1Space X → R1Space X → R1Space X
-- Aesop.Rule.Name
Aesop.DisplayRuleName.instToJson : Lean.ToJson Aesop.DisplayRuleName
-- Init.Data.Array.Lemmas
Array.mem_empty_iff : ∀ {α : Type u_1} (a : α), a ∈ #[] ↔ False
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_hom_comp_descQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom (h.descQ k hk) = S.descOpcycles k hk
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_nonempty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P},
  (asymptoticCone k s).Nonempty ↔ s.Nonempty
-- Mathlib.Algebra.Exact.Basic
/-- The maps `f` and `g` form an exact pair:
`g y = 0` iff `y` belongs to the image of `f`.  -/
Function.Exact : {M : Type u_2} → {N : Type u_4} → {P : Type u_6} → (M → N) → (N → P) → [Zero P] → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If a subspace is less than another, there is a point only in the second.  -/
AffineSubspace.exists_of_lt : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁ < s₂ → ∃ p ∈ s₂, p ∉ s₁
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] (t : Set β) (b : β), {b} /ₛ t = (fun x => b /ₛ x) '' t
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.biUnion_star_subset_nonuniformWitness : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts) (V : Finset α),
  (SzemerediRegularity.star hP G ε hU V).biUnion id ⊆ G.nonuniformWitness ε U V
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Composing with an injective homomorphism on the codomain does not change the kernel.  -/
MonoidHom.ker_comp_of_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {P : Type u_8} [inst_2 : MulOneClass P] (f : G →* N)
  (g : N →* P), Function.Injective ⇑g → (g.comp f).ker = f.ker
-- Mathlib.Order.Category.BddLat
/-- The underlying `BoundedLatticeHom`.  -/
BddLat.Hom.hom' : {X Y : BddLat} → X.Hom Y → BoundedLatticeHom ↑X.toLat ↑Y.toLat
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Evidence that the arbitrary choice of cocone is a colimit cocone.  -/
CategoryTheory.Limits.colimit.isColimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.colimit.cocone F)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.restrict.eq_1 : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0),
  w.restrict s hs =
    {
      weights :=
        ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun x k => k)⁻¹ • Finsupp.filter (fun x => x ∈ s) w.weights,
      nonneg := ⋯, total := ⋯ }
-- Mathlib.RingTheory.Ideal.Maximal
/-- The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring,
and there are no other proper ideals strictly containing it.  -/
Ideal.IsMaximal.out : ∀ {α : Type u} {inst : Semiring α} {I : Ideal α} [self : I.IsMaximal], IsCoatom I
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.del.injEq : ∀ (x : Lean.IR.VarId) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.del x b = Lean.IR.FnBody.del x_1 b_1) = (x = x_1 ∧ b = b_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.toList_perm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey! = k
-- Init.Data.Fin.Lemmas
Fin.exists_castSucc_eq : ∀ {n : ℕ} {i : Fin (n + 1)}, (∃ j, j.castSucc = i) ↔ i ≠ Fin.last n
-- Mathlib.RingTheory.WittVector.Basic
/-- The bijection between `𝕎 R` and `ℕ → R`, under the assumption that `p` is invertible in `R`.
In `WittVector.ghostEquiv` we upgrade this to an isomorphism of rings.  -/
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostEquiv' : (p : ℕ) → (R : Type u_1) → [inst : CommRing R] → [Invertible ↑p] → WittVector p R ≃ (ℕ → R)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.toSubsemigroup'_closure : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Additive M)),
  AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Additive.ofMul ⁻¹' S)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.comp h i) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom h_1)
-- Mathlib.RingTheory.FinitePresentation
/-- The quotient of a finitely presented algebra by a finitely generated ideal is finitely
presented.  -/
Algebra.FinitePresentation.quotient : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I : Ideal A},
  I.FG → ∀ [Algebra.FinitePresentation R A], Algebra.FinitePresentation R (A ⧸ I)