mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Defs
/-- `Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  -/
Fintype : Type u_4 → Type u_4
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_one : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.extend 1 = f₁
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- If `sᵢ` is a countable family of (null) measurable pairwise `μ`-a.e. disjoint sets, then there
exists a subordinate family `tᵢ ⊆ sᵢ` of measurable pairwise disjoint sets such that
`tᵢ =ᵐ[μ] sᵢ`.  -/
MeasureTheory.exists_subordinate_pairwise_disjoint : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
      ∃ t,
        (∀ (i : ι), t i ⊆ s i) ∧
          (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Function.onFun Disjoint t)
-- Mathlib.Analysis.Normed.Field.Lemmas
Rat.instNormedField : NormedField ℚ
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `orderOf_eq_card_powers`.  -/
RightCancelMonoid.Nat.card_submonoidPowers : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {a : G}, Nat.card ↥(Submonoid.powers a) = orderOf a
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SimplexCategory.toTopHomeo_symm_naturality_apply : ∀ {n m : SimplexCategory} (f : n ⟶ m) (x : ↑(stdSimplex ℝ (Fin (n.len + 1)))),
  m.toTopHomeo.symm (stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) x) =
    (CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) (n.toTopHomeo.symm x)
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
sqrt_one_add_norm_sq_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (x : E), √(1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖
-- Init.Data.UInt.BasicAux
instAddUInt32 : Add UInt32
-- Mathlib.Analysis.Convex.Topology
IsOpen.convexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [ZeroLEOneClass 𝕜] {s : Set E}, IsOpen s → IsOpen ((convexHull 𝕜) s)
-- Mathlib.CategoryTheory.Sites.Point.Over
/-- Given a point `Φ` of a site `(C, J)`, an object `X : C`, and `x : Φ.fiber.obj X`,
this is the point of the site `(Over X, J.over X)` such that the fiber of
an object of `Over X` corresponding to a morphism `f : Y ⟶ X` identifies
to subtype of `Φ.fiber.obj Y` consisting of elements `y` such
that `Φ.fiber.map f y = x`.  -/
CategoryTheory.GrothendieckTopology.Point.over : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [CategoryTheory.LocallySmall.{w, v, u} C] → (Φ : J.Point) → {X : C} → Φ.fiber.obj X → (J.over X).Point
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- **Alias** of `CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom`. -/
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A}
  (f : Φ.presheafFiber.obj F.obj ⟶ M),
  ((Φ.skyscraperSheafAdjunction.homEquiv F M) f).hom = Φ.skyscraperPresheafHomEquiv f
-- Mathlib.Algebra.Group.Basic
div_right_injective : ∀ {G : Type u_3} [inst : Group G] {b : G}, Function.Injective fun a => b / a
-- Init.Data.UInt.Lemmas
USize.lt_of_le_of_lt : ∀ {a b c : USize}, a ≤ b → b < c → a < c
-- Lean.Data.Position
/-- Returns the position of the start of (1-based) line `line`.
This gives the same result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
 -/
Lean.FileMap.lineStart : Lean.FileMap → ℕ → String.Pos.Raw
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNIndepSet_iff : ∀ {α : Type u_1} (G : SimpleGraph α) (n : ℕ) (s : Finset α), G.IsNIndepSet n s ↔ G.IsIndepSet ↑s ∧ s.card = n
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
          (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) h)))
-- Init.Data.Nat.Gcd
Nat.gcd_sub_right_right_of_dvd : ∀ {m k : ℕ} (n : ℕ), k ≤ m → n ∣ k → n.gcd (m - k) = n.gcd m
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.instIsEmpty : ∀ (X : Type u_3) [IsEmpty X], IsEmpty (FundamentalGroupoid X)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_eq_self : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] {b : Module.Basis ι K E} [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] {x : E}, ZSpan.fract b x = x ↔ x ∈ ZSpan.fundamentalDomain b
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vadd_right_swap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p q : P), ((signedDist v) p) (w +ᵥ q) = ((signedDist v) (-w +ᵥ p)) q
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasFDerivAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜},
  x ≠ 0 → HasFDerivAt (fun x => x⁻¹) (ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) x
-- Init.Data.String.Basic
instDecidableIsValidUTF8 : {b : ByteArray} → Decidable b.IsValidUTF8
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis'.eRk_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → M.eRk X = I.encard
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.coe_symm_opAddEquiv : ∀ {M : Type u_1} [inst : AddCommMonoid M], ⇑AddOpposite.opAddEquiv.symm = AddOpposite.unop
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 00IA](https://stacks.math.columbia.edu/tag/00IA) -/
LocalSubring.exists_le_valuationSubring : ∀ {K : Type u_3} [inst : Field K] (A : LocalSubring K), ∃ B, A ≤ B.toLocalSubring
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex tangent function, defined as `sin z / cos z`  -/
Complex.tan : ℂ → ℂ
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonpositive on
`Iio b` and nonnegative on `Ioo b c`. Then `f` attains its minimum on `Iic c` at `b`.  -/
isMinOn_Iic_of_deriv : ∀ {f : ℝ → ℝ} {b c : ℝ},
  ContinuousAt f b →
    ContinuousAt f c →
      DifferentiableOn ℝ f (Set.Iio b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Iio b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Iic c) b
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.AtomIso.mk.sizeOf_spec : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf { e := e, src := src, tgt := tgt } = 1 + sizeOf e + sizeOf src + sizeOf tgt
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a right lift from a 1-morphism and a 2-morphism.  -/
CategoryTheory.Bicategory.RightLift.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (h : c ⟶ b) → (CategoryTheory.CategoryStruct.comp h f ⟶ g) → CategoryTheory.Bicategory.RightLift f g
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
Submodule.mem_adjoint_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (g : Submodule 𝕜 (E × F)) (x : F × E),
  x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → inner 𝕜 b x.1 - inner 𝕜 a x.2 = 0
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Postcomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNorm_linearIsometryEquiv_comp : ∀ {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜₁] [inst_4 : NormedSpace 𝕜₁ E] [inst_5 : NontriviallyNormedField 𝕜₂]
  [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : NontriviallyNormedField 𝕜₃] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [inst_9 : RingHomInvPair σ₂₃ σ₃₂] [inst_10 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂]
  (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F), ‖↑↑e ∘SL f‖ = ‖f‖
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] (a : A),
  CategoryTheory.CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a)
      ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) =
    G.map ((L.pointwiseLeftKanExtensionUnit F).app a)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- `Proj` as a locally ringed space  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.termProj : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic.0.tacticEval_simp : Lean.ParserDescr
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_bot_of_isEmpty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [IsEmpty β] (f : β → α) (S : Finset β),
  S.sup f = ⊥
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconcaveOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r < f x}
-- Mathlib.NumberTheory.Divisors
Nat.prod_divisors_prime_pow : ∀ {α : Type u_1} [inst : CommMonoid α] {k p : ℕ} {f : ℕ → α},
  Nat.Prime p → ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ Finset.range (k + 1), f (p ^ x)
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
IsPrimitiveRoot.idealQuotient_mk : ∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [inst_1 : NumberField K] {n : ℕ} [NeZero n]
  {ζ : NumberField.RingOfIntegers K},
  IsPrimitiveRoot ζ n → Ideal.absNorm I ≠ 1 → (Ideal.absNorm I).Coprime n → IsPrimitiveRoot ((Ideal.Quotient.mk I) ζ) n
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.ofList_cons : ∀ {α : Type u} (a : α) (l : List α), ↑(a :: l) = Stream'.WSeq.cons a ↑l
-- Mathlib.Topology.UniformSpace.CompareReals
/-- The uniform bijection between Bourbaki and Cauchy reals.  -/
CompareReals.compareEquiv : CompareReals.Bourbakiℝ ≃ᵤ ℝ
-- Mathlib.Order.Lattice
/-- Transfer `SemilatticeInf` across an `Equiv`.  -/
Equiv.semilatticeInf : {α : Type u} → {β : Type v} → α ≃ β → [SemilatticeInf β] → SemilatticeInf α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two strictly monotone functions is strictly monotone.  -/
StrictMonoOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftStrictMono α] [AddRightStrictMono α],
  StrictMonoOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x + g x) s
-- Lean.Data.Options
Lean.Options.getInPattern : Lean.Options → Bool
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses `Finsupp.sum`.  -/
Submodule.mem_span_set : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M}
  {s : Set M}, m ∈ Submodule.span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelCommMonoid α],
  MulOpposite.instCancelCommMonoid = { toCommMonoid := MulOpposite.instCommMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.instEtaleRing : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R), Algebra.Etale R P.Ring
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.counitInv = e.counitIso.inv
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves multiplication  -/
MulSemiringActionHom.map_mul' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (self : R →ₑ+*[φ] S) (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.RingTheory.DualNumber
TrivSqZeroExt.isNilpotent_inr : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : M), IsNilpotent (TrivSqZeroExt.inr x)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.tsum_of_nat_of_neg : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {f : ℤ → G},
  (Summable fun n => f ↑n) →
    (Summable fun n => f (-↑n)) → ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-↑n) - f 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.CtorView.modifiers : Lean.Elab.Command.CtorView → Lean.Elab.Modifiers
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom map in the right unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp
                F ⟶
              F
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.mk : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] →
                  [inst_6 : Star B] →
                    (toNonUnitalAlgHom : A →ₙₐ[R] B) →
                      (∀ (a : A), toNonUnitalAlgHom.toFun (star a) = star (toNonUnitalAlgHom.toFun a)) → A →⋆ₙₐ[R] B
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.simplex.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (e_x : x = x_1) (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d), hx.simplex hd = ⋯.simplex ⋯
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roi_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rco.Sliceable.mkSlice xs (lo + 1)...Std.Slice.size xs
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.cast_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_14} {M : ι → Type u_15} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {i j : ι} (h : i = j) (a : M j), (LinearEquiv.cast h).symm a = cast ⋯ a
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_enorm_pow : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} {p : ℕ},
  MeasureTheory.MemLp f (↑p) μ → p ≠ 0 → MeasureTheory.Integrable (fun x => ‖f x‖ₑ ^ p) μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_le_arith_mean3_weighted : ∀ {w₁ w₂ w₃ p₁ p₂ p₃ : ℝ},
  0 ≤ w₁ →
    0 ≤ w₂ →
      0 ≤ w₃ → 0 ≤ p₁ → 0 ≤ p₂ → 0 ≤ p₃ → w₁ + w₂ + w₃ = 1 → p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.comp_eqToHom_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y'),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom p) = g ↔
    f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.foundLine : Std.Format.SpaceResult✝ → Bool
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.mk_surjective : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (R : Φ.RightResolution X₂), ∃ X₁ w, ∃ (hw : W₂ w), R = { X₁ := X₁, w := w, hw := hw }
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineMap.map_midpoint : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : Invertible 2]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] (f : P →ᵃ[R] P') (a b : P),
  f (midpoint R a b) = midpoint R (f a) (f b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey? k = m₁.getKey? k
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.isNormal_veblen_zero : Order.IsNormal fun x => Ordinal.veblen x 0
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instContinuousSMulTangentSpace : ∀ {𝕜 : 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] (_x : M), ContinuousSMul 𝕜 (TangentSpace I _x)
-- Mathlib.SetTheory.Cardinal.Basic
/-- The lift of a supremum is the supremum of the lifts.  -/
Cardinal.lift_sSup : ∀ {s : Set Cardinal.{u_1}}, BddAbove s → Cardinal.lift.{u, u_1} (sSup s) = sSup (Cardinal.lift.{u, u_1} '' s)
-- Batteries.Data.List.Scan
_private.Batteries.Data.List.Scan.0.List.take_flatten : {α : Type u_1} →
  (L : List (List α)) →
    (i : ℕ) →
      ProofWanted
        (have j := List.findIdx (fun x => decide (x > i)) (List.map List.length L).partialSums - 1;
        have k := i - (List.take j L).flatten.length;
        List.take i L.flatten = (List.take j L).flatten ++ List.take k (L[j]?.getD []))
-- Lean.Parser.Term
Lean.Parser.Term.letOpts.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Lie.SemiDirect
/-- The canonical inclusion of K into the semi-direct sum K ⋊⁅ψ⁆ G.  -/
LieAlgebra.SemiDirectSum.inl : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → K →ₗ⁅R⁆ K ⋊⁅ψ⁆ L
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- Inductively construct preimage of Cauchy sequence.  -/
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage : {R : Type u} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type w} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {f : M →ₗ[R] N} →
                    Function.Surjective ⇑f → (x : AdicCompletion.AdicCauchySequence I N) → (n : ℕ) → ↑(⇑f ⁻¹' {↑x n})
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.finsetSum_iSup : ∀ {ι : Type u_1} {α : Type u_2} {s : Finset α} {f : α → ι → ENNReal},
  (∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) → ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
-- Lean.SubExpr
Lean.SubExpr.Pos.pushAppArg : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_sub : ∀ {α : Type u_1} {G : Type u_8} [inst : AddGroup G] {p : α → Prop} {v v' : α →₀ G},
  Finsupp.subtypeDomain p (v - v') = Finsupp.subtypeDomain p v - Finsupp.subtypeDomain p v'
-- Std.Data.HashMap.AdditionalOperations
Std.HashMap.Raw.WF.filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  {f : α → β → Option γ}, m.WF → (Std.HashMap.Raw.filterMap f m).WF
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toOneHom_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), ⇑↑f = ⇑f
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_right_cancel : ∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit b → a + b = c + b → a = c
-- Mathlib.Order.OrderDual
OrderDual.ofDual_le_ofDual : ∀ {α : Type u_1} [inst : LE α] {a b : αᵒᵈ}, OrderDual.ofDual a ≤ OrderDual.ofDual b ↔ b ≤ a
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.of_add_eq_zero_right : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {b : M} (a : M), a + b = 0 → IsAddUnit b
-- Init.Data.List.Basic
List.append_eq : ∀ {α : Type u} {as bs : List α}, as.append bs = as ++ bs
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E}, s ∈ nhds x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x