mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.RightLift.IsKan.fac_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.RightLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.RightLift f g) {Z : c ⟶ a}
  (h : g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (H.desc s) f)
      (CategoryTheory.CategoryStruct.comp t.counit h) =
    CategoryTheory.CategoryStruct.comp s.counit h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.leftUnitor_hom_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).hom
      Y.hom
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.η_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {X Y : C}
  (f : X ⟶ Y) [inst_3 : F.OplaxMonoidal] {Z : C}
  (h : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).map f) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Separation.Basic
Homeomorph.t1Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y),
  T1Space Y
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
/-- A multivariate power series is not a zero divisor
when its constant coefficient is not a zero divisor  -/
MvPowerSeries.mem_nonZeroDivisors_of_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ : MvPowerSeries σ R},
  MvPowerSeries.constantCoeff φ ∈ nonZeroDivisors R → φ ∈ nonZeroDivisors (MvPowerSeries σ R)
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
/-- If `x ↦ ∑' i, log (f i x)` is uniformly convergent on `𝔖`, its sum has bounded-above real part
on each set in `𝔖`, and the functions `f i x` have no zeroes, then  `∏' i, f i x` is uniformly
convergent on `𝔖`.

Note that the non-vanishing assumption is really needed here: if this assumption is dropped then
one obtains a counterexample if `ι = α = ℕ` and `f i x` is `0` if `i = x` and `1` otherwise.  -/
hasProdUniformlyOn_of_clog : ∀ {α : Type u_1} {ι : Type u_2} {s : Set α} {f : ι → α → ℂ},
  SummableUniformlyOn (fun i x => Complex.log (f i x)) s →
    (∀ x ∈ s, ∀ (i : ι), f i x ≠ 0) →
      BddAbove ((fun x => (∑' (i : ι), Complex.log (f i x)).re) '' s) →
        HasProdUniformlyOn f (fun x => ∏' (i : ι), f i x) s
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul₂_iterateMulAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, MeasurableSMul₂ (IterateMulAct f) α ↔ Measurable f
-- Lean.Meta.Tactic.Grind.Types
/-- We use this auxiliary constant to mark delayed congruence proofs.  -/
Lean.Meta.Grind.congrPlaceholderProof : Lean.Expr
-- Mathlib.Data.Nat.Digits.Lemmas
/-- Any non-zero natural number `m` is greater than
b^((number of digits in the base b representation of m) - 1)
 -/
Nat.base_pow_length_digits_le : ∀ (b m : ℕ), 1 < b → m ≠ 0 → b ^ (b.digits m).length ≤ b * m
-- Std.Time.Format.DateFormat
/-- The first day of the week for this locale (e.g., `Weekday.sunday` for US, `Weekday.monday` for ISO 8601).
 -/
Std.Time.DateFormat.firstDayOfWeek : Std.Time.DateFormat → Std.Time.Weekday
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.toMeasure_apply₀ : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α},
  MeasureTheory.NullMeasurableSet s (m.toMeasure h) → (m.toMeasure h) s = m s
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- `S` is the localization of `T` away from `S`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.instAwayTGbar : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  IsLocalization.Away (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D) S
-- Init.Tactics
/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`.  -/
Lean.Parser.Tactic.runTac : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.differentiableAt_log : ∀ {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ Real.log x
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- `A.nonunits` agrees with the maximal ideal of `A`, after taking its image in `K`.  -/
ValuationSubring.image_maximalIdeal : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K}, Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) = ↑A.nonunits
-- Mathlib.ModelTheory.Basic
Equiv.inducedStructure_RelMap : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] (e : M ≃ N) {n : ℕ} (r : L.Relations n)
  (x : Fin n → N), FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r (⇑e.symm ∘ x)
-- Mathlib.Probability.Kernel.WithDensity
/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0∞` which is everywhere finite,
`withDensity κ f` is s-finite.  -/
ProbabilityTheory.Kernel.IsSFiniteKernel.withDensity : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ],
  (∀ (a : α) (b : β), f a b ≠ ⊤) → ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)
-- Mathlib.Order.GaloisConnection.Basic
isGLB_image2_of_isGLB_isGLB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (u₂ a) (u a)) → IsGLB s a₀ → IsGLB t b₀ → IsGLB (Set.image2 u s t) (u a₀ b₀)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q
          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
        h_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_swap_add_of_covariant_add : ∀ (N : Type u_2) (r : N → N → Prop) [inst : AddCommSemigroup N] [CovariantClass N N (fun x1 x2 => x1 + x2) r],
  CovariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
-- Mathlib.Topology.Separation.Basic
t1Space_iff_disjoint_nhds_pure : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsQF
-- Mathlib.Algebra.Homology.QuasiIso
/-- A morphism of homological complexes `f : K ⟶ L` is a quasi-isomorphism when it
is so in every degree, i.e. when the induced maps `homologyMap f i : K.homology i ⟶ L.homology i`
are all isomorphisms (see `quasiIso_iff` and `quasiIsoAt_iff_isIso_homologyMap`).  -/
QuasiIso : {ι : Type u_1} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} → (K ⟶ L) → [∀ (i : ι), K.HasHomology i] → [∀ (i : ι), L.HasHomology i] → Prop
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], Int.fract (OfNat.ofNat n) = 0
-- Mathlib.Data.List.Sublists
List.sublistsLen_sublist_sublists' : ∀ {α : Type u} (n : ℕ) (l : List α), (List.sublistsLen n l).Sublist l.sublists'
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_sign : ∀ (a b : ℤ), a.tdiv b.sign = a * b.sign
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.map_of : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : Add β] (f : α →ₙ+ β) (x : α),
  (AddMagma.FreeAddSemigroup.map f) (AddMagma.FreeAddSemigroup.of x) = AddMagma.FreeAddSemigroup.of (f x)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_rng_of_principal_iff_forall : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι}
  {X : Type u_3} [inst_1 : TopologicalSpace X]
  {f : X → RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S)},
  Continuous f ↔ ∀ (i : ι), Continuous ((fun x => x i) ∘ f)
-- Batteries.Control.LawfulMonadState
/-- If the underlying monad `m` has a lawful state instance, then the induced state instance on
`ReaderT ρ m` will also be lawful.  -/
LawfulMonadStateOf.instReaderTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ ρ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadStateOf σ m]
  [LawfulMonadStateOf σ m], LawfulMonadStateOf σ (ReaderT ρ m)
-- Mathlib.Topology.Sets.Compacts
/-- The image of a nonempty compact set under a continuous function.  -/
TopologicalSpace.NonemptyCompacts.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : α → β) → Continuous f → TopologicalSpace.NonemptyCompacts α → TopologicalSpace.NonemptyCompacts β
-- Mathlib.Topology.SeparatedMap
isSeparatedMap_iff_isClosedEmbedding : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsSeparatedMap f ↔ Topology.IsClosedEmbedding (toPullbackDiag f)
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_sInf : ∀ {M : Type u_3} [inst : Add M] {ts : Set (TopologicalSpace M)}, (∀ t ∈ ts, ContinuousAdd M) → ContinuousAdd M
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.smulCommClass : ∀ (G : Type u_10) (A : Type u_11) (B : Type u_12) (K : Type u_13) (L : Type u_14) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [inst_5 : Field K] [inst_6 : Field L]
  [inst_7 : Algebra K L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : Algebra A L] [IsFractionRing A K]
  [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [SMulCommClass G A B], SMulCommClass G K L
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
AffineSubspace.shift_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (c : P) (r : k), ⊤.shift c r = ⊤
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The continuous linear equivalence between a vector space over `𝕜` with a finite basis and
functions from its basis indexing type to `𝕜`.  -/
Module.Basis.equivFunL : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                [CompleteSpace 𝕜] → {ι : Type u_1} → [Finite ι] → [T2Space E] → Module.Basis ι 𝕜 E → E ≃L[𝕜] ι → 𝕜
-- Lean.Environment
_private.Lean.Environment.0.Lean.getIRExtraConstNames : Lean.Environment → Lean.OLeanLevel → optParam Bool false → Array Lean.Name
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `multiplicative_of_total`.

---

If a binary function from a type equipped with a total relation `r` to a monoid is
anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
(i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
We allow restricting to a subset specified by a predicate `p`.  -/
multiplicative_of_isTotal : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (r : α → α → Prop) [Std.Total r] (f : α → α → β) (p : α → Prop),
  (∀ {a b : α}, p a → p b → f a b * f b a = 1) →
    (∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) →
      ∀ {a b c : α}, p a → p b → p c → f a c = f a b * f b c
-- Init.Notation
/-- Parentheses are used for grouping priority expressions.  -/
«prio(_)» : Lean.ParserDescr
-- Mathlib.Order.SemiconjSup
IsOrderRightAdjoint.right_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {g : β → α},
  IsOrderRightAdjoint f g → Monotone g
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] [G.IsEquivalence],
  Φ.IsLocalizedEquivalence
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_isColimit : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i],
  (SSet.relativeCellComplexOfMono i).isColimit =
    (CategoryTheory.Limits.isColimitOfPreserves SSet.Subcomplex.toSSetFunctor
          (CategoryTheory.Limits.CompleteLattice.colimitCocone ⋯.functor).isColimit).ofIsoColimit
      (CategoryTheory.Limits.Cocone.ext (SSet.Subcomplex.eqToIso ⋯ ≪≫ SSet.Subcomplex.topIso Y) ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.darts_dropUntil_subset_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).darts ⊆ p.darts
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R),
  CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i) =
    CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_inf_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
  Filter.Tendsto f x₁ y → Filter.Tendsto f (x₁ ⊓ x₂) y
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_coeff_eq_prod_coeff_of_le : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  {k : ℕ}, Fintype.card n - 1 ≤ k → M.charpoly.coeff k = (∏ i, (Polynomial.X - Polynomial.C (M i i))).coeff k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a k : α}
  {v : β}, (t.insert k v)[a]? = if cmp k a = Ordering.eq then some v else t[a]?
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_one_of_mul_lt_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightReflectLT α] {a b : α}, a * b < b → a < 1
-- Mathlib.Topology.SeparatedMap
/-- A function from a topological space `X` is locally injective if every point of `X`
has a neighborhood on which `f` is injective.  -/
IsLocallyInjective : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → (X → Y) → Prop
-- Mathlib.Order.CompactlyGenerated.Intervals
Set.Iic.instIsCompactlyGenerated : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α}, IsCompactlyGenerated ↑(Set.Iic a)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_sInf : ∀ {M : Type u_2} [inst : Mul M] (S : Set (Subsemigroup M)), (sInf S).op = sInf (Subsemigroup.unop ⁻¹' S)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
/-- Given a `n`-simplex `x` in `Δ[p] ⊗ Δ[q]`, this is the order preserving
map `Fin (n + 1) →o Fin (m + 1)` (with `p + q = m`) which corresponds to the
sum of the two components of `objEquiv x : Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)`.  -/
SSet.prodStdSimplex.orderHomOfSimplex : {p q n : ℕ} →
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }) →
    {m : ℕ} → p + q = m → Fin (n + 1) →o Fin (m + 1)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquivOfRightInverse_symm_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N]
  {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) (x : N),
  (Module.Invertible.linearEquivOfRightInverse hfg).symm x = g x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionParams : Lean.FromJson Lean.Lsp.CompletionParams
-- Mathlib.Algebra.CharP.Lemmas
exists_add_pow_prime_pow_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p → ∀ (x y : R) (n : ℕ), ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * x * y * r
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- Given a finite set of monic polynomials, construct an algebra homomorphism
to the splitting field of the product of the polynomials
sending indeterminates $X_{f_i}$ to the distinct roots of `f`.  -/
AlgebraicClosure.toSplittingField : {k : Type u} →
  [inst : Field k] →
    (s : Finset (AlgebraicClosure.Monics k)) →
      MvPolynomial (AlgebraicClosure.Vars k) k →ₐ[k] (∏ f ∈ s, ↑f).SplittingField
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, panicking if no such element exists.
 -/
Std.ExtTreeSet.getGE! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsDTopologyCompatible.mk : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : DiffeologicalSpace X],
  Diffeology.dTopology = t → Diffeology.IsDTopologyCompatible X
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R), (PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_map : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ},
  (Std.Iter.map f it).toArray = Array.map f it.toArray
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_ofColex : ∀ {α : Type u_1} [inst : Monoid α] {a : Colex α}, IsRegular (ofColex a) ↔ IsRegular a
-- Mathlib.Data.Num.Basic
PosNum.bit1.inj : ∀ {a a_1 : PosNum}, a.bit1 = a_1.bit1 → a = a_1
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.refl_apply : ∀ {R : Type u_1} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  (LinearEquiv.refl R M) x = x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] [inst_6 : W.IsCompatibleWithShift M]
  {m : M} (α : CategoryTheory.Localization.SmallShiftedHom W X Y m) (m₀ : M) (hm₀ : m₀ = 0),
  (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ (CategoryTheory.CategoryStruct.id X)).comp α ⋯ = α
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) =
    h_1 ()
-- Mathlib.Analysis.Complex.Trigonometric
Real.one_add_tan_sq_mul_cos_sq_eq_one : ∀ {x : ℝ}, Real.cos x ≠ 0 → (1 + Real.tan x ^ 2) * Real.cos x ^ 2 = 1
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.eraseEMatch : Lean.Meta.Grind.Params → Lean.Name → Lean.MetaM Lean.Meta.Grind.Params
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32.congr_simp : ∀ (a a_1 : USize), a = a_1 → ∀ (h : System.Platform.numBits = 32), a.toBitVec32 h = a_1.toBitVec32 h
-- Mathlib.Data.Fin.Tuple.Basic
/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.cons`.  -/
Fin.consInduction : {α : Sort u_1} →
  {motive : {n : ℕ} → (Fin n → α) → Sort v} →
    motive Fin.elim0 →
      ({n : ℕ} → (x₀ : α) → (x : Fin n → α) → motive x → motive (Fin.cons x₀ x)) → {n : ℕ} → (x : Fin n → α) → motive x