mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.comp_lift : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] {N : Type u_5} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M),
  g.comp (FreeAddMonoid.lift f) = FreeAddMonoid.lift (⇑g ∘ f)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Sets `mat[i, j]`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.setElem : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommRing.toGRing : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddCommMonoid ι} →
      {inst_1 : (i : ι) → AddCommGroup (A i)} → [self : DirectSum.GCommRing A] → DirectSum.GRing A
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.summable_norm_sub_inv_pow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L] (n : ℕ), Module.finrank ℤ ↥L < n → ∀ (x : E), Summable fun z => ‖↑z - x‖⁻¹ ^ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext : Type
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.eq_1 : ∀ {α : Type u} (s : Stream'.WSeq α), s.drop 0 = s
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.coe_ofContinuousOpenRestrict : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)),
  ↑(PartialHomeomorph.ofContinuousOpenRestrict e hc ho) = ↑e
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [inst_1 : SizeOf α]
  (rank : ↑P.II → α) (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y),
  sizeOf { rank := rank, lt := lt } = 1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_ofRingCon : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {x : R} {c : RingCon R}, x ∈ { ringCon := c } ↔ c x 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁ β).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ ((β.hom.app X₂).app X₃)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The "homology class" map `S.cycles ⟶ S.leftHomology`.  -/
CategoryTheory.ShortComplex.leftHomologyπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.cycles ⟶ S.leftHomology
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
          k ∈ List.map Prod.fst toInsert →
            ∀ {h : Std.Internal.List.containsKey k' (Std.Internal.List.insertListConst l toInsert) = true},
              Std.Internal.List.getKey k' (Std.Internal.List.insertListConst l toInsert) h = k
-- Init.Data.Array.Basic
/-- Low-level indexing operator which is as fast as a C array read.

This avoids overhead due to unboxing a `Nat` used as an index.
 -/
Array.uget : {α : Type u} → (xs : Array α) → (i : USize) → i.toNat < xs.size → α
-- Lean.Meta.Tactic.Grind.Beta
/-- Returns all lambda expressions in the equivalence class with root `root`.  -/
Lean.Meta.Grind.getEqcLambdas : Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM (Array Lean.Expr)
-- Init.Meta.Defs
Lean.Meta.instReprConfig.repr : Lean.Meta.DSimp.Config → ℕ → Std.Format
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s)
-- Init.Sym.Lemmas
Lean.Sym.Int.eq_eq_true : ∀ (a b : ℤ), decide (a = b) = true → (a = b) = True
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.minKey? = none
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.one_le_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, 1 ≤ a⁻¹ ↔ a ≤ 1
-- Init.Data.SInt.Bitwise
Int32.not_not : ∀ {a : Int32}, ~~~~~~a = a
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.vec_add_const_isTheta : ∀ (a b : ℤ), (fun m => ‖![m 0 + a, m 1 + b]‖⁻¹) =Θ[Filter.cofinite] fun m => ‖m‖⁻¹
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mk.sizeOf_spec : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C] [inst_3 : SizeOf C]
  [inst_4 : SizeOf ι] (H : ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C)
  (δ' :
    (n₀ n₁ : ℤ) →
      n₀ + 1 = n₁ →
        ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_2
                CategoryTheory.Abelian.SpectralObject._proof_4).comp
            (H n₀) ⟶
          (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Abelian.SpectralObject._proof_6
                CategoryTheory.Abelian.SpectralObject._proof_2).comp
            (H n₁)))
  (exact₁' :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂ ((δ' n₀ n₁ h).app D)
          ((H n₁).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₂' :
    ∀ (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8
                  CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((H n).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))).Exact)
  (exact₃' :
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2),
      (CategoryTheory.ComposableArrows.mk₂
          ((H n₀).map
            ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                  CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2
                  CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4
                  CategoryTheory.Abelian.SpectralObject._proof_4).app
              D))
          ((δ' n₀ n₁ h).app D)).Exact),
  sizeOf { H := H, δ' := δ', exact₁' := exact₁', exact₂' := exact₂', exact₃' := exact₃' } = 1
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_image_equiv : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (e : α ≃ β), Nat.card ↑(⇑e '' s) = Nat.card ↑s
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a frame with possibly different definitional
equalities.  -/
Frame.copy : {α : Type u} →
  (c : Order.Frame α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (himp : α → α → α) →
                          himp = HImp.himp →
                            (compl : α → α) →
                              compl = Compl.compl →
                                (sSup : Set α → α) →
                                  sSup = SupSet.sSup → (sInf : Set α → α) → sInf = InfSet.sInf → Order.Frame α
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f (-g) = -CategoryTheory.CategoryStruct.comp f g
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R), ↑(Matrix.SpecialLinearGroup.toLin' A).symm = Matrix.toLin' ↑A⁻¹
-- Mathlib.Data.Prod.TProd
List.TProd.elim.eq_1 : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] (x i : ι) (is : List ι) (v : List.TProd α (i :: is))
  (x_1 : x ∈ i :: is),
  v.elim x_1 =
    if hji : x = i then
      Eq.ndrec (motive := fun i => List.TProd α (i :: is) → x ∈ i :: is → α x) (fun v hj => v.1) hji v x_1
    else List.TProd.elim v.2 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abLeftHomologyData_i : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.abLeftHomologyData.i = AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom S.g).ker.subtype
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Rci.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Rci.HasRcoIntersection α] → Std.Rci α → Std.Rco α → Std.Rco α
-- Mathlib.Analysis.Fourier.AddCircle
fourier_zero' : ∀ {T : ℝ}, ↑(AddCircle.toCircle 0) = 1
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.isEligible : Lean.Name → Lean.Meta.Try.Collector.M Bool
-- Init.Data.Fin.Lemmas
Fin.val_cast : ∀ {n m : ℕ} (h : n = m) (i : Fin n), ↑(Fin.cast h i) = ↑i
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaN_iff : ∀ {x : Float.Model.UnpackedFloat}, x.isNaN = true ↔ x = Float.Model.UnpackedFloat.notANumber
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLECancellable_of_lt_top : ∀ {α : Type u} [inst : Add α] {x : WithTop α} [inst_1 : Preorder α] [AddLeftReflectLE α], x < ⊤ → AddLECancellable x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_mul : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : MulZeroClass β]
  [inst_3 : ContinuousMul β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f * g) = ⇑f * ⇑g
-- Init.Core
beq_of_eq : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a b : α}, a = b → (a == b) = true
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.instSemiring : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → Semiring (LinearAlgebra.FreeProduct R A)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_succ : ∀ {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}) (o : Ordinal.{u_2}),
  Ordinal.derivFamily f (Order.succ o) = Ordinal.nfpFamily f (Order.succ (Ordinal.derivFamily f o))
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_monotone : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → ∀ (F : CategoryTheory.Functor C D), P.strictMap F ≤ Q.strictMap F
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)} {h : k ∈ m.alter k f}, (m.alter k f).get k h = (f (m.get? k)).get ⋯
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.commute_inlₗ_inrₗ : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (m : α) (n : β), Commute ((OrderMonoidHom.inlₗ α β) m) ((OrderMonoidHom.inrₗ α β) n)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.w_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j') {F_1 : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F_1] (x : carrier c.pt),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x) =
    (CategoryTheory.ConcreteCategory.hom (c.π.app j')) x
-- Init.Sym.Lemmas
Lean.Sym.String.le_eq_true : ∀ (a b : String), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coeff_mul_prod_one_sub_of_lt_order : ∀ {R : Type u_2} {ι : Type u_3} [inst : CommRing R] (k : ℕ) (s : Finset ι) (φ : PowerSeries R) (f : ι → PowerSeries R),
  (∀ i ∈ s, ↑k < (f i).order) → (PowerSeries.coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (PowerSeries.coeff k) φ
-- Init.GetElem
/-- The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]` in identifiers is `getElem`. -/
«term__[_]» : Lean.TrailingParserDescr
-- Init.Data.String.Basic
String.Slice.Pos.le_nextn : ∀ {s : String.Slice} {p : s.Pos} {n : ℕ}, p ≤ p.nextn n
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_comp_descOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j)
  (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K ⟶ L) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (L.descOpcycles k j hj hk) h) =
    CategoryTheory.CategoryStruct.comp (K.descOpcycles (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj ⋯) h
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.f_open : ∀ (self : AlgebraicGeometry.Scheme.GlueData) (i j : self.J), AlgebraicGeometry.IsOpenImmersion (self.f i j)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
instHasDetOneAdjoinNegOneOfFactEvenNatCard : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_3} [inst_2 : CommRing R]
  {𝒢 : Subgroup (GL n R)} [𝒢.HasDetOne] [Fact (Even (Fintype.card n))], 𝒢.adjoinNegOne.HasDetOne
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.ofBaseChange_toBaseChange : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (x : CliffordAlgebra (QuadraticForm.baseChange A Q)),
  (CliffordAlgebra.ofBaseChange A Q) ((CliffordAlgebra.toBaseChange A Q) x) = x
-- Mathlib.Algebra.Torsor.Defs
/-- Subtracting two points produces 0 if and only if they are
equal.  -/
vsub_eq_zero_iff_eq : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P}, p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.mk : IO.Promise Unit → IO.Ref Bool → IO.CancelToken
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.Pattern.Model.find?_eq_some_iff.match_1_2.splitter : {s : String.Slice} →
  (motive : String.Slice.Pattern.SearchStep s → Sort u_1) →
    (x : String.Slice.Pattern.SearchStep s) →
      ((s_1 endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched s_1 endPos)) →
        ((startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.left_unitality_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} (self : F.CoreMonoidal) (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X))
      (CategoryTheory.CategoryStruct.comp (self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) h))
-- Mathlib.Topology.Category.CompactlyGenerated
/-- Typecheck a `ContinuousMap` as a morphism in `CompactlyGenerated`.  -/
CompactlyGenerated.ofHom : {X : Type w} →
  [inst : TopologicalSpace X] →
    [inst_1 : UCompactlyGeneratedSpace X] →
      {Y : Type w} →
        [inst_2 : TopologicalSpace Y] →
          [inst_3 : UCompactlyGeneratedSpace Y] → C(X, Y) → (CompactlyGenerated.of X ⟶ CompactlyGenerated.of Y)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.refl_symm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], (ContinuousAlgEquiv.refl R A).symm = ContinuousAlgEquiv.refl R A
-- Mathlib.Order.SupClosed
image_latticeClosure' : ∀ {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] (s : Set α) (f : α → β),
  (∀ (a b : α), f (a ⊔ b) = f a ⊓ f b) →
    (∀ (a b : α), f (a ⊓ b) = f a ⊔ f b) → f '' latticeClosure s = latticeClosure (f '' s)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx.congr_simp : ∀ {α : Type u} {β : Type v} (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (hl : t.Balanced)
  (n n_1 : ℕ) (e_n : n = n_1) (h : n < t.size),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx t hl n h = Std.DTreeMap.Internal.Impl.Const.entryAtIdx t_1 ⋯ n_1 ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ._auto_1) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀)
      (CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) h) =
    CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.node_lt : ∀ {n i j : ℕ}, j ≤ n → i < j → Polynomial.Chebyshev.node n j < Polynomial.Chebyshev.node n i
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_1.eq_1 : ∀ {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ Id β₁] {it₁ : Std.Iter β₁} (motive : it₁.Step → Sort u_2)
  (it₁' : Std.Iter β₁) (out : β₁) (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.Iter β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.Iter β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.yield it₁' out, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_1 it₁' out hp
-- Mathlib.GroupTheory.Rank
AddGroup.rank_spec : ∀ (G : Type u_1) [inst : AddGroup G] [h : AddGroup.FG G], ∃ S, S.card = AddGroup.rank G ∧ AddSubgroup.closure ↑S = ⊤
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_rpow_of_exponent_lt : ∀ {x : ENNReal} {y z : ℝ}, 1 < x → x ≠ ⊤ → y < z → x ^ y < x ^ z
-- Mathlib.Topology.Connected.PathConnected
/-- If `f : X → Y` is an inducing map, `f(F)` is path-connected iff `F` is.  -/
Topology.IsInducing.isPathConnected_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X} {f : X → Y},
  Topology.IsInducing f → (IsPathConnected F ↔ IsPathConnected (f '' F))
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The conductor of χ⁻¹ equals the conductor of χ.  -/
DirichletCharacter.conductor_inv : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ⁻¹.conductor = χ.conductor
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.String.Subslice
String.Slice.startInclusive_subsliceFrom : ∀ {s : String.Slice} {newStart : s.Pos}, (s.subsliceFrom newStart).startInclusive = newStart
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology.cocycles A 0)),
  (ModuleCat.Hom.hom (groupCohomology.cochainsIso₀ B).hom)
      ((ModuleCat.Hom.hom (groupCohomology.iCocycles B 0))
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesMap f φ 0)) x)) =
    (Rep.Hom.hom φ).toLinearMap
      ((ModuleCat.Hom.hom (groupCohomology.cochainsIso₀ A).hom) ((ModuleCat.Hom.hom (groupCohomology.iCocycles A 0)) x))
-- Init.Data.Nat.Div.Lemmas
Nat.div_mod_eq_mod_div_mod : ∀ {a b c : ℕ}, a < c → b < c → a / b % c = a % c / (b % c)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsUniform.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (ε : 𝕜),
  P.IsUniform G ε = (↑(P.nonUniforms G ε).card ≤ ↑(P.parts.card * (P.parts.card - 1)) * ε)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.dvdCnstr? : Lean.Expr → Lean.MetaM (Option (ℤ × Int.Internal.Linear.Expr × Array Lean.Expr))