mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The isomorphism `X K i ≅ K.X j` when `i = some j`.  -/
HomologicalComplex.extend.XIso : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            (K : HomologicalComplex C c) →
              {i : Option ι} → {j : ι} → i = some j → (HomologicalComplex.extend.X K i ≅ K.X j)
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the antidiagonal is determined by its first coordinate.

See also `Finset.antidiagonal_congr'`.  -/
Finset.HasAntidiagonal.antidiagonal_congr : ∀ {A : Type u_1} [inst : AddCancelMonoid A] [inst_1 : Finset.HasAntidiagonal A] {p q : A × A} {n : A},
  p ∈ Finset.HasAntidiagonal.antidiagonal n → q ∈ Finset.HasAntidiagonal.antidiagonal n → (p = q ↔ p.1 = q.1)
-- Mathlib.GroupTheory.Nilpotent
/-- An additive subgroup is nilpotent iff its lower central series eventually
vanishes.  -/
AddSubgroup.isNilpotent_iff_lowerCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G), AddGroup.IsNilpotent ↥S ↔ ∃ n, S.lowerCentralSeries n = ⊥
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_C : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R),
  (Polynomial.aevalTower g y) (Polynomial.C x) = g x
-- Mathlib.Topology.Order.Rolle
/-- If a function `f` is continuous on an open interval
and tends to the same value at its endpoints,
then it has a local extremum on this open interval.  -/
exists_isLocalExtr_Ioo_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
  a < b →
    ContinuousOn f (Set.Ioo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
        Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, IsLocalExtr f c
-- Mathlib.Data.Matrix.Basic
/-- `piEquiv` as a `LinearEquiv`.  -/
Matrix.piLinearEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {ι : Type u_14} →
      {β : ι → Type u_15} →
        (R : Type u_16) →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (β i)] →
              [inst_2 : (i : ι) → Module R (β i)] → Matrix m n ((i : ι) → β i) ≃ₗ[R] (i : ι) → Matrix m n (β i)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality_left : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (β_ Y Z).hom =
    CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Make `MulArchimedeanClass.subsemigroup` a subgroup by assigning
s = ⊤ with a junk value ⊥.  -/
MulArchimedeanClass.subgroup : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → UpperSet (MulArchimedeanClass M) → Subgroup M
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The short complex `Φ.r ⟶ 𝟭 C ⟶ Φ.quotient` in the functor category associated to a preradical
`Φ`.  -/
CategoryTheory.Abelian.Preradical.shortComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Abelian.Preradical C → CategoryTheory.ShortComplex (CategoryTheory.Functor C C)
-- Init.Data.String.Defs
String.Pos.Raw.isValid_empty_iff : ∀ {p : String.Pos.Raw}, String.Pos.Raw.IsValid "" p ↔ p = 0
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.toAddGroup : {E : Type u_8} → [self : NormedAddGroup E] → AddGroup E
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ext.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Meta.Grind.SplitSource.ext declName = Lean.Meta.Grind.SplitSource.ext declName_1) = (declName = declName_1)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Differentiability of a section on `s` can be determined
using any trivialisation whose `baseSet` contains `s`.  -/
Bundle.Trivialization.mdifferentiableOn_section_iff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] {s : (x : B) → E x} {a : Set B} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [MemTrivializationAtlas e], IsOpen a → a ⊆ e.baseSet → (MDiff[a] (T% s) ↔ MDiff[a] fun x => (↑e ⟨x, s x⟩).2)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.mk.sizeOf_spec : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} [inst_2 : SizeOf C₁] [inst_3 : SizeOf C₂]
  [inst_4 : ⦃X Y : C₁⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)] [inst_5 : ⦃X Y : C₂⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)]
  (functor : CategoryTheory.Functor C₁ C₂) (map : W₁ ≤ W₂.inverseImage functor),
  sizeOf { functor := functor, map := map } = 1 + sizeOf functor
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_eq_zero_iff : ∀ {x : ℝ}, Real.sin x = 0 ↔ ∃ n, ↑n * Real.pi = x
-- Init.Data.String.Defs
String.push_eq_append : ∀ {s : String} (c : Char), s.push c = s ++ String.singleton c
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coconeOfIsSplitEpi_ι_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitEpi f]
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.coconeOfIsSplitEpi f).ι.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.casesOn X_1
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f) f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkLeft_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ η : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.prodMkLeft γ (κ + η) =
    ProbabilityTheory.Kernel.prodMkLeft γ κ + ProbabilityTheory.Kernel.prodMkLeft γ η
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂ : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {Y : CategoryTheory.Abelian.SpectralObject C EInt} [self : Y.IsThirdQuadrant] (i j : EInt) (hij : i ≤ j) (n : ℤ),
  j ≤ WithBotTop.coe n →
    CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprConnection.repr : Std.Http.Header.Connection → ℕ → Std.Format
-- Mathlib.Order.RelClasses
/-- **Alias** of `not_subset_of_ssuperset`.

---

Set notation form of `not_le_of_gt` -/
not_subset_of_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊆ a
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_coe_nonneg : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]}, 0 ≤ (↑x).valuation
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.ctor.inj : ∀ {ctorName : Lean.Name} {us : List Lean.Level} {params : List Lean.Expr} {fields : List Lean.Meta.Match.Pattern}
  {ctorName_1 : Lean.Name} {us_1 : List Lean.Level} {params_1 : List Lean.Expr}
  {fields_1 : List Lean.Meta.Match.Pattern},
  Lean.Meta.Match.Pattern.ctor ctorName us params fields =
      Lean.Meta.Match.Pattern.ctor ctorName_1 us_1 params_1 fields_1 →
    ctorName = ctorName_1 ∧ us = us_1 ∧ params = params_1 ∧ fields = fields_1
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `MonCat`.  -/
CategoryTheory.Iso.monCatIsoToMulEquiv : {X Y : MonCat} → (X ≅ Y) → ↑X ≃* ↑Y
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
/-- This is really an auxiliary result en route to `blimsup_cthickening_mul_ae_eq`.

NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932.  -/
blimsup_cthickening_ae_le_of_eventually_mul_le : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  {s : ℕ → Set α} {M : ℝ},
  0 < M →
    ∀ {r₁ r₂ : ℕ → ℝ},
      Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) →
        (∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) →
          Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ]
            Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p
-- Mathlib.Analysis.PSeries
summable_pow_div_add : ∀ {α : Type u_1} (x : α) [inst : RCLike α] (q k : ℕ), 1 < q → Summable fun n => ‖x / (↑n + ↑k) ^ q‖
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.logUnassignedAndAbort : Array Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.toPMF_dirac : ∀ {α : Type u_1} (a : α) [inst : MeasurableSpace α] [inst_1 : Countable α] [h : MeasurableSingletonClass α],
  (MeasureTheory.Measure.dirac a).toPMF = PMF.pure a
-- Init.Data.Iterators.Basic
/-- Makes a single step with the given iterator `it`, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
Std.IterM.step : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [inst : Std.Iterator α m β] → (it : Std.IterM m β) → m (Std.Shrink it.Step)
-- Std.Data.DTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DTreeMap.Const.insertMany : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      {ρ : Type u_1} → [ForIn Id ρ (α × β)] → Std.DTreeMap α (fun x => β) cmp → ρ → Std.DTreeMap α (fun x => β) cmp
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.mk : {α : Type} → Std.Mutex (Std.CloseableChannel.Bounded.State✝ α) → Std.CloseableChannel.Bounded✝ α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The type of objects for the diagram indexing reflexive (co)equalizers  -/
CategoryTheory.Limits.WalkingReflexivePair : Type
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.normedAddCommGroup : {E : Type u_1} → [inst : NormedAddCommGroup E] → {s : AddSubgroup E} → NormedAddCommGroup ↥s
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (φ : G ≃ₜ* G), 0 < MeasureTheory.mulEquivHaarChar φ
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousInvULift : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G], ContinuousInv (ULift.{u_1, w} G)
-- Mathlib.Algebra.Group.Action.Defs
/-- Commutativity of additive actions is a symmetric relation. This lemma can't be an instance
because this would cause a loop in the instance search graph.  -/
VAddCommClass.symm : ∀ (M : Type u_9) (N : Type u_10) (α : Type u_11) [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass N M α
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_top_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.relIndex ⊤ = H.index
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.annIdealGenerator_aeval_eq_zero : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  (Polynomial.aeval a) (Polynomial.annIdealGenerator 𝕜 a) = 0
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.subset' : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (self : T.CompleteType α),
  (L.lhomWithConstants α).onTheory T ⊆ ↑self
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The property satisfied by the circumsphere.  -/
Affine.Simplex.circumsphere_unique_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  (s.circumsphere.center ∈ affineSpan ℝ (Set.range s.points) ∧
      Set.range s.points ⊆ Metric.sphere s.circumsphere.center s.circumsphere.radius) ∧
    ∀ (cs : EuclideanGeometry.Sphere P),
      cs.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere cs.center cs.radius →
        cs = s.circumsphere
-- Mathlib.Order.CompleteLattice.Basic
iSup_sup_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f g : ι → α}, ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of the identity in a topological group, as a subgroup.  -/
Subgroup.pathComponentOne : (G : Type u_4) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → Subgroup G
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instInvValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → Inv (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instVAdd : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd β αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Presentation
/-- A colimit presentation of `X` over `J` is a diagram `{Dᵢ}` in `C` and natural maps
`sᵢ : Dᵢ ⟶ X` making `X` into the colimit of the `Dᵢ`.  -/
CategoryTheory.Limits.ColimitPresentation : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    (J : Type w) → [CategoryTheory.Category.{t, w} J] → C → Type (max (max (max t u) v) w)
-- Mathlib.Data.Analysis.Topology
Ctop.inter_mem : ∀ {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b),
  x ∈ self.f (self.inter a b x h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_t : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A), (C.map φ).t = φ C.t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig → Std.Tactic.BVDecide.BVExpr.Return aig w
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.mk : {G : Type u_6} →
  [inst : AddGroup G] →
    (toAddGroupSeminorm : AddGroupSeminorm G) → (∀ (x : G), toAddGroupSeminorm.toFun x = 0 → x = 0) → AddGroupNorm G
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- **Alias** of `zero_mem_tangentConeAt`.

---

The tangent cone at a non-isolated point contains `0`.  -/
zero_mem_tangentCone : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E}, x ∈ closure s → 0 ∈ tangentConeAt 𝕜 s x
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_biSup_of_directedOn : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Type u_4} {p : ι → Prop},
  (∃ i, p i) →
    ∀ {S : ι → AddSubmonoid M},
      DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) S) {i | p i} →
        ∀ {x : M}, x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i
-- Init.System.IO
/-- Returns the current thread's standard error stream.

Use `IO.setStderr` to replace the current thread's standard error stream.
 -/
IO.getStderr : BaseIO IO.FS.Stream
-- Mathlib.Topology.Neighborhoods
Filter.EventuallyEq.eq_of_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α}, f =ᶠ[nhds x] g → f x = g x
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_add_eq_left_of_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p q : Polynomial R}, q.natDegree < n → (p + q).coeff n = p.coeff n
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_id_id : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M), B.comp LinearMap.id LinearMap.id = B
-- Init.Data.List.Lemmas
List.concat_append : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.concat a ++ l₂ = l₁ ++ a :: l₂
-- Lean.Data.LBool
Lean.instBEqLBool : BEq Lean.LBool
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] (f : γ →CO δ) (g : β →CO γ) (h : α →CO β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.of_f : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {i j : ι} (hij : i ≤ j)
  (x : G i), (DirectLimit.Algebra.of G f j) ((f i j hij) x) = (DirectLimit.Algebra.of G f i) x
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivWithinAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → ∀ (n : ℕ), HasDerivWithinAt (f ^ n) (↑n * f x ^ (n - 1) * f') s x
-- Mathlib.Analysis.Normed.MulAction
IsBoundedSMul.of_norm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β],
  (∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) → IsBoundedSMul α β
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instCommSemiring : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → {S : Submonoid R} → CommSemiring (LocalizedModule S A)
-- Mathlib.Data.Set.Function
Set.prod_surjOn_fst_iff : ∀ {β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂}, Set.SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ↔ t₁ = ∅ ∨ t₂.Nonempty
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- The tensor product of `R`-bialgebras is commutative, up to bialgebra isomorphism.  -/
Bialgebra.TensorProduct.comm : (R : Type u_1) →
  (A : Type u_3) →
    (B : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Bialgebra R A] → [inst_4 : Bialgebra R B] → TensorProduct R A B ≃ₐc[R] TensorProduct R B A
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_inv : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` is differentiable on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
mdifferentiableOn_localFrameCoeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  IsOpen t →
    t ⊆ e.baseSet →
      MDiff[t] (T% s) → ∀ (i : ι), MDiff[t] ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
-- Init.GrindInstances.ToInt
Lean.Grind.instMulNatCiOfNatInt : Lean.Grind.ToInt.Mul ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.toEven_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  ↑((CliffordAlgebra.toEven Q) ((CliffordAlgebra.ι Q) m)) =
    CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m
-- Batteries.Tactic.Lint.Frontend
/-- The `in foo` config argument allows running the linter on a specified project.  -/
Batteries.Tactic.Lint.inProject : Lean.ParserDescr
-- Mathlib.Order.Interval.Set.Monotone
antitone_Ioi : ∀ {α : Type u_1} [inst : Preorder α], Antitone Set.Ioi
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The identity embedding from a graph to itself.  -/
SimpleGraph.Embedding.refl : {V : Type u_1} → {G : SimpleGraph V} → G ↪g G
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.inl_strictMono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero M₀] [inst_1 : GroupWithZero N₀]
  [inst_2 : PartialOrder N₀] [inst_3 : DecidablePred fun x => x = 0], StrictMono ⇑(MonoidWithZeroHom.inl M₀ N₀)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ici_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ici a)), Subtype.val '' Set.Iio b = Set.Ico a ↑b
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits a subtraction.  -/
AddSubgroup.sub : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → Sub ↥H
-- Init.GetElem
GetElem?.toGetElem : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} → [self : GetElem? coll idx elem valid] → GetElem coll idx elem valid
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f g : ℕ → β},
  IsCauSeq abv f → IsCauSeq abv g → IsCauSeq abv (f * g)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk.injEq : ∀ {M : Type u_3} [inst : Mul M] (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
  (carrier_1 : Set M) (mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1),
  ({ carrier := carrier, mul_mem' := mul_mem' } = { carrier := carrier_1, mul_mem' := mul_mem'_1 }) =
    (carrier = carrier_1)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.warning.simp.otherHead : Lean.Option Bool