mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Adds an E-matching equality theorem to the environment.
See `mkEMatchEqTheorem`.
 -/
Lean.Meta.Grind.Extension.addEMatchEqTheorem : Lean.Meta.Grind.Extension → Lean.Name → Lean.MetaM Unit
-- Mathlib.LinearAlgebra.Matrix.Permanent
/-- Permuting the rows does not change the permanent.  -/
Matrix.permanent_permute_rows : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (σ : Equiv.Perm n)
  (M : Matrix n n R), (M.submatrix id ⇑σ).permanent = M.permanent
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality_assoc : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') {Z : D} (h : d' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d').hom h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.keys_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool}, (Std.ExtDTreeMap.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.dist_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_3} [inst_1 : PseudoMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∀ {x y : α}, x ∈ s → y ∈ s → dist (f x) (f y) ≤ (eVariationOn f s).toReal
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!ₘ_eq_getValue! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  [inst_4 : Inhabited β] {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.get!ₘ t k = Std.Internal.List.getValue! k t.toListModel
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.append.eq_1 : ∀ {α : Type u_1} {m n : ℕ} {x : Fin m ↪ α} {y : Fin n ↪ α} (h : Disjoint (Set.range ⇑x) (Set.range ⇑y)),
  Fin.Embedding.append h = { toFun := Fin.append ⇑x ⇑y, inj' := ⋯ }
-- Mathlib.Order.Nucleus
Nucleus.coe_inf : ∀ {X : Type u_1} [inst : SemilatticeInf X] (m n : Nucleus X), ⇑(m ⊓ n) = ⇑m ⊓ ⇑n
-- Std.Do.Triple.Basic
Std.Do.Triple.entails_wp_of_post : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α} {P : Std.Do.Assertion ps}
  {Q Q' : Std.Do.PostCond α ps}, ⦃P⦄ x ⦃Q'⦄ → Q'.entails Q → P ⊢ₛ (Std.Do.wp x).apply Q
-- Lean.Elab.Tactic.LibrarySearch
/-- Implementation of the `exact?` tactic.

* `ref` contains the input syntax and is used for locations in error reporting.
* `config` contains configuration options (e.g., `grind` for using grind as a discharger).
* `required` contains an optional list of terms that should be used in closing the goal.
* `requireClose` indicates if the goal must be closed.
  It is `true` for `exact?` and `false` for `apply?`.
 -/
Lean.Elab.LibrarySearch.exact? : Lean.Syntax →
  Lean.Parser.Tactic.LibrarySearchConfig → Option (Array (Lean.TSyntax `term)) → Bool → Lean.Elab.Tactic.TacticM Unit
-- Std.Sat.AIG.Relabel
_private.Std.Sat.AIG.Relabel.0.Std.Sat.AIG.Decl.relabel.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (decl : Std.Sat.AIG.Decl α) →
      (Unit → motive Std.Sat.AIG.Decl.false) →
        ((a : α) → motive (Std.Sat.AIG.Decl.atom a)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → motive (Std.Sat.AIG.Decl.gate lhs rhs)) → motive decl
-- Mathlib.Algebra.Order.Positive.Ring
Positive.isOrderedMonoid : ∀ {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R],
  IsOrderedMonoid { x // 0 < x }
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If the `affineSpan` of a finite affinely independent family lies
in an affine subspace whose direction has dimension one less than its
cardinality, it equals that subspace.  -/
AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p →
    ∀ {sp : AffineSubspace k P} [FiniteDimensional k ↥sp.direction],
      affineSpan k (Set.range p) ≤ sp →
        Fintype.card ι = Module.finrank k ↥sp.direction + 1 → affineSpan k (Set.range p) = sp
-- Mathlib.FieldTheory.Extension
_private.Mathlib.FieldTheory.Extension.0.IntermediateField.exists_algHom_adjoin_of_splits'' : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E} {L : IntermediateField F E} (f : ↥L →ₐ[F] K),
  (∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits) →
    ∃ φ, AlgHom.domRestrict (↥L) φ = f
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.unfold_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α), a + -b = c → a - b = c
-- Std.Async.Basic
/-- An asynchronous computation that may produce an error of type `IO.Error`..
 -/
Std.Async.Async : Type → Type
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instDistribMulActionOfSMulCommClass : {S : Type u_1} →
  {R : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : Monoid S] →
                    [inst_6 : DistribMulAction S N] → [SMulCommClass S R N] → DistribMulAction S (QuadraticMap R M N)
-- Init.Data.BitVec.Lemmas
/-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`.  -/
BitVec.getMsbD_rotateLeft_of_lt : ∀ {r n w : ℕ} {x : BitVec w}, r < w → (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_has_prop : ∀ {n : ℕ}, n ≠ 1 → Nat.minFacProp✝ n n.minFac
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.instStar : {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → Star (CentroidHom α)
-- Mathlib.Order.Filter.IsBounded
/-- Filters are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic `isBoundedDefault` in the statements,
in the form `(hf : f.IsBounded (≥) := by isBoundedDefault)`.  -/
Filter.tacticIsBoundedDefault : Lean.ParserDescr
-- Mathlib.Data.SetLike.Basic
SetLike.coe_ssubset_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B] {S T : A},
  ↑S ⊂ ↑T ↔ S < T
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C}
  {x y : P.Hom Q}, x.f = y.f → x = y
-- Lean.Message
Lean.AddMessageContext.mk : {m : Type → Type} → (Lean.MessageData → m Lean.MessageData) → Lean.AddMessageContext m
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q),
  (CochainComplex.HomComplex.Cochain.toSingleMk f h).v p q h =
    CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv
-- Mathlib.Data.Rel
SetRel.left_subset_comp : ∀ {α : Type u_1} {β : Type u_2} {S : SetRel β β} {R : SetRel α β} [S.IsRefl], R ⊆ R.comp S
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E),
  ‖A x‖ ^ 2 = RCLike.re (inner 𝕜 x ((ContinuousLinearMap.adjoint A ∘SL A) x))
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_srem : ∀ (a b : BitVec 32), Int32.ofBitVec (a.srem b) = Int32.ofBitVec a % Int32.ofBitVec b
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` is even.  -/
Real.posLog_abs : ∀ (x : ℝ), |x|.posLog = x.posLog
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- Equivalences form a monoid.  -/
RootPairing.Equiv.instMonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → Monoid (P.Equiv P)
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelOpUnop_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.kernelOpUnop f).inv =
    CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯
-- Init.Data.Range.Polymorphic.SInt
Int16.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int16
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent : Type
-- Mathlib.Data.Finset.Pi
Finset.pi_insert : ∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (β a)] {s : Finset α}
  {t : (a : α) → Finset (β a)} {a : α},
  a ∉ s → (insert a s).pi t = (t a).biUnion fun b => Finset.image (Finset.Pi.cons s a b) (s.pi t)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.neg_def : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], (-f).toFun' S = -1 • f.toFun' S
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.symmₗ_apply_of_notMem : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → ∀ (y : F), (Bundle.Pretrivialization.symmₗ R e b) y = 0
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.instQuotientSubmodule : {R : Type u_1} →
  {C : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup C] →
        [inst_2 : Module R C] → [inst_3 : Coalgebra R C] → (I : Submodule R C) → [I.IsCoideal] → Coalgebra R (C ⧸ I)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdx.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : x.Balanced) →
          (x_2 : ℕ) →
            (x_3 : x_2 < x.size) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
                          (n : ℕ) →
                            (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h) →
                motive x x_1 x_2 x_3
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_eq_of_le_of_coeff_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ ↑n → p.coeff n ≠ 0 → p.degree = ↑n
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mvarIdPendingExp : Lean.DelayedMetavarAssignment → Lean.MVarId
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get? (m₁ ∪ m₂) k = Std.DHashMap.Raw.Const.get? m₂ k
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCategory : CategoryTheory.Category.{u, u + 1} GrpCat
-- Mathlib.Algebra.Opposites
AddOpposite.op_injective : ∀ {α : Type u_1}, Function.Injective AddOpposite.op
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isValue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f g : E → F},
  IsBoundedLinearMap 𝕜 f → IsBoundedLinearMap 𝕜 g → IsBoundedLinearMap 𝕜 fun e => f e + g e
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkState : Aesop.MVarClusterRef → Lean.CoreM Unit
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
natCast_pentagonal : ∀ (k : ℤ), ↑(pentagonal k) = k * (3 * k - 1) / 2
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (hr₁ : S₁.RightHomologyData) (hr₂ : S₂.RightHomologyData) (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : hr₁.IsPreservedBy F] [inst_6 : hr₂.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.rightHomologyMap' φ hr₁ hr₂) =
    CategoryTheory.ShortComplex.rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseId : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toList_rco : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m...n).toList.length), (m...n).toList[i] = m + ↑i
-- Mathlib.RingTheory.Nilpotent.Basic
IsIdempotentElem.eq_zero_of_isNilpotent : ∀ {R : Type u_1} [inst : MonoidWithZero R] {e : R}, IsIdempotentElem e → IsNilpotent e → e = 0
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.val_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A], ↑1 = 1
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.edist_approxOn_y0_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ),
  edist y₀ ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ Set.univ = 1 → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Topology.Algebra.Constructions
/-- Put the same topological space structure on the opposite monoid as on the original space.  -/
MulOpposite.instTopologicalSpaceMulOpposite : {M : Type u_1} → [TopologicalSpace M] → TopologicalSpace Mᵐᵒᵖ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.getConst.eq_def : ∀ (x : Int.Internal.Linear.Poly),
  x.getConst =
    match x with
    | Int.Internal.Linear.Poly.num k => k
    | Int.Internal.Linear.Poly.add k v p => p.getConst
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_conductorSet_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {x : ℕ}, x ∈ χ.conductorSet → x ∣ n
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of a singleton is finite-dimensional.  -/
finiteDimensional_direction_affineSpan_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), FiniteDimensional k ↥(affineSpan k {p}).direction
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.natCast_succ : ∀ (n : ℕ), ↑n.succ = Order.succ ↑n
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.lowerCentralSeries_eq_top : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Group.IsPerfect ↥H] (n : ℕ), H.lowerCentralSeries n = H
-- Init.Data.Sum.Lemmas
Sum.elim_comp_inl_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α ⊕ β → γ), Sum.elim (f ∘ Sum.inl) (f ∘ Sum.inr) = f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F) {s t : Set α}, ⇑m '' (s * t) = ⇑m '' s * ⇑m '' t
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYoneda.instSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat},
  CategoryTheory.ObjectProperty.Small.{u, max u v, max u (v + 1)} (PresheafOfModules.freeYoneda R)
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ioi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), UpperSet.Ioi a = { carrier := Set.Ioi a, upper' := ⋯ }
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instIsEquivalenceOppositeSymmUnopFunctor : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V], (HomologicalComplex.unopFunctor V c).IsEquivalence
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.forall_neg_mem : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α} {p : α → Prop}, (∀ (x : α), -x ∈ s → p x) ↔ ∀ x ∈ s, p (-x)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalences_eq_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.weakEquivalences C = (HomotopicalAlgebra.weakEquivalences Cᵒᵖ).unop
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instTransOrdOffset : Std.TransOrd Std.Time.Millisecond.Offset
-- Init.Control.Do
/-- A wrapper around `OptionT` signifying `break` in a loop.  -/
BreakT : (Type u_1 → Type u_2) → Type u_1 → Type u_2
-- Mathlib.Algebra.Lie.Basic
nsmul_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M)
  (n : ℕ), ⁅n • x, m⁆ = n • ⁅x, m⁆
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {a b : α} {fallback : β},
      (a == b) = true → Std.DHashMap.Raw.Const.getD m a fallback = Std.DHashMap.Raw.Const.getD m b fallback
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_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 : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)),
      ↑((s.restrict S hS).touchpoint signs i) = s.touchpoint signs i
-- Init.SimpLemmas
ite_false : ∀ {α : Sort u_1} (a b : α), (if False then a else b) = b
-- Init.Data.Vector.Algebra
/-- Pointwise multiplication of vectors.
This is not a global instance as in some applications different multiplications may be relevant.
 -/
Vector.instMul : {α : Type u_1} → {n : ℕ} → [Mul α] → Mul (Vector α n)
-- Mathlib.Data.Finset.Density
Finset.dens_union_of_disjoint : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α} [inst_1 : DecidableEq α],
  Disjoint s t → (s ∪ t).dens = s.dens + t.dens
-- Mathlib.CategoryTheory.ComposableArrows.One
/-- The functor `ComposableArrows C n ⥤ ComposableArrows C 1`
which sends `S` to `mk₁ (S.map' i j)` when `i`, `j` and `n`
are such that `i ≤ j` and `j ≤ n`.  -/
CategoryTheory.ComposableArrows.functorArrows : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (i j n : ℕ) →
      autoParam (i ≤ j) CategoryTheory.ComposableArrows.functorArrows._auto_1 →
        autoParam (j ≤ n) CategoryTheory.ComposableArrows.functorArrows._auto_3 →
          CategoryTheory.Functor (CategoryTheory.ComposableArrows C n) (CategoryTheory.ComposableArrows C 1)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map_subtype_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (S : AffineSubspace k P) [inst_4 : Nonempty ↥S] (s : Affine.Simplex k (↥S) n),
  (s.map S.subtype ⋯).restrict S ⋯ = s
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_trans : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P ≃ₗ[R] Q)
  (f : N ≃ₗ[R] P), LinearEquiv.rTensor M (f ≪≫ₗ g) = LinearEquiv.rTensor M f ≪≫ₗ LinearEquiv.rTensor M g
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.isOpen_iff_finite : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [IsGalois k K], IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k ↥L
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_div_right : ∀ {M : Type u} [inst : DivInvMonoid M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  edist (a / c) (b / c) = edist a b
-- Init.Data.List.Basic
List.beq.eq_def : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  x.beq x_1 =
    match x, x_1 with
    | [], [] => true
    | a :: as, b :: bs => a == b && as.beq bs
    | x, x_2 => false
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.conjTranspose : ∀ {α : Type u_1} {n : Type u_3} [inst : Star α] {A : Matrix n n α}, A.IsSymm → A.conjTranspose.IsSymm
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.of'_modOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (g : G),
  (AddMonoidAlgebra.of' k G g).modOf g = 0
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N), (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom