mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_symm_apply_snd : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)] (p : B × F₁ × F₂),
  (↑(e₁.prod e₂).symm p).snd = (e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_neg : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A} (x : ↥S),
  ↑(-x) = -↑x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_eq.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} (hst : s = t),
  SubAddAction.ofFixingAddSubgroup_of_eq M hst =
    {
      toFun := fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨x, ⋯⟩,
      map_vadd' := ⋯ }
-- Init.Data.Int.LemmasAux
Int.neg_ofNat_le_ofNat : ∀ (n m : ℕ), -OfNat.ofNat n ≤ OfNat.ofNat m
-- Mathlib.CategoryTheory.GradedObject
/-- The canonical inclusion `X i ⟶ X.mapObj p j` when `i : I` and `j : J` are such
that `p i = j`.  -/
CategoryTheory.GradedObject.ιMapObj : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) →
          (p : I → J) → [inst_1 : X.HasMap p] → (i : I) → (j : J) → p i = j → (X i ⟶ X.mapObj p j)
-- Init.System.ST
/-- Creates a new mutable reference that contains the provided value `a`.
 -/
ST.mkRef : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → α → m (ST.Ref σ α)
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.monotone_transfiniteIterate_φ : ∀ {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] {X : Type w}
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)),
  (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)) →
    ∀
      (m :
        (B : Set X) →
          (hB : HasCardinalLT (↑B) κ₂) →
            (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X)
      (A : Set X),
      Monotone fun j => transfiniteIterate (Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m) j A
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, this expresses the compatibility of
`e₁` and `e₂` with the counit of the adjunction `adj`.
 -/
CategoryTheory.Adjunction.CommShift.CompatibilityCounit : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddMonoid A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      {a : A} →
                        ((CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) →
                          ((CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)) → Prop
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.instPseudoMetricSpace.eq_1 : ∀ {α : Type u_1} [inst : PseudoMetricSpace α],
  AddOpposite.instPseudoMetricSpace = PseudoMetricSpace.induced AddOpposite.unop inst
-- Mathlib.Algebra.Lie.Basic
LieEquiv.toLieHom : {R : Type u} →
  {L : Type v} →
    {L' : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → [inst_3 : LieRing L'] → [inst_4 : LieAlgebra R L'] → (L ≃ₗ⁅R⁆ L') → L →ₗ⁅R⁆ L'
-- Mathlib.Order.Concept
mem_upperPolar_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {b : β}, b ∈ upperPolar r s ↔ ∀ ⦃a : α⦄, a ∈ s → r a b
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_slice : ∀ {δ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {γ : Type u'}
  {α β : Type u} [inst_4 : Std.ToIterator (Std.Slice γ) Id α β] [inst_5 : Std.Iterator α Id β]
  [inst_6 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] {init : δ}
  {f : β → δ → m (ForInStep δ)} {xs : Std.Slice γ} (inv : Std.Internal.Do.Invariant xs.toList δ Pred) {epost : EPred},
  (∀ (pref : List β) (cur : β) (suff : List β) (h : xs.toList = pref ++ cur :: suff) (b : δ),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator, or `none` if no such output is found.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. The elements in `it` are examined in order of
iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
productive. If such a proof is not available, consider using `Iter.first?`.

Examples:
* `[7, 6].iter.first? = some 7`
* `[].iter.first? = none`
 -/
Std.Iter.Total.first? : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] → [Std.Iterators.Productive α Id] → Std.Iter.Total β → Option β
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_fst' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  ⇑(ContinuousAlgHom.fst R A B) = Prod.fst
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The morphism `K.truncGE e ⟶ L.truncGE e` induced by a morphism `K ⟶ L`.  -/
HomologicalComplex.truncGEMap : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              {K L : HomologicalComplex C c'} →
                (K ⟶ L) →
                  (e : c.Embedding c') →
                    [inst_2 : e.IsTruncGE] →
                      [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                        [inst_4 : ∀ (i' : ι'), L.HasHomology i'] →
                          [inst_5 : CategoryTheory.Limits.HasZeroObject C] → K.truncGE e ⟶ L.truncGE e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)] {b : β a}, (t.insert a b).get! a = b
-- Mathlib.Analysis.Convex.Basic
AntitoneOn.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
-- Init.Data.List.Perm
List.Perm.unattach : ∀ {α : Type u} {p : α → Prop} {l₁ l₂ : List { x // p x }}, l₁.Perm l₂ → l₁.unattach.Perm l₂.unattach
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size - 1
-- Mathlib.Topology.Algebra.UniformConvergence
instMulUniformFun : {α : Type u_1} → {β : Type u_2} → [Mul β] → Mul (UniformFun α β)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
alternatingGroup.isCoatom_stabilizer_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  3 ≤ Nat.card α →
    ∀ {s : Set α}, s.Nonempty → s.Subsingleton → IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Restrict a finite measure μ to a set A.  -/
MeasureTheory.FiniteMeasure.restrict : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → Set Ω → MeasureTheory.FiniteMeasure Ω
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The signature of the permutation on the complex embeddings of `K` defined by sending an embedding
to its conjugate has signature `(-1) ^ nrComplexPlaces K`.
 -/
NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Equiv.Perm.sign (Function.Involutive.toPerm NumberField.ComplexEmbedding.conjugate ⋯) =
    (-1) ^ NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.Logic.Relation
Relation.EqvGen.refl : ∀ {α : Type u_1} {r : α → α → Prop} (x : α), Relation.EqvGen r x x
-- Std.Http.Data.Version
Std.Http.instInhabitedVersion : Inhabited Std.Http.Version
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instDecidableEqOrdinal : DecidableEq Std.Time.Week.Aligned.Ordinal
-- Std.Tactic.Do.Syntax
/-- If `true` (the default), we substitute away let-declarations that are used at most once before
starting VC generation and will do the same for every VC generated.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.elimLets : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J'), P.IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J'
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.toFreeAddMonoid_of : ∀ {α : Type u_1} (x : α), FreeAddSemigroup.toFreeAddMonoid (FreeAddSemigroup.of x) = FreeAddMonoid.of x
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.span_leadingTerm_eq_span_monomial' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [inst : Field k] {B : Set (MvPolynomial σ k)},
  Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun p => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.ext_iff : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) (x y : ↥L'), x = y ↔ ↑x = ↑y
-- Mathlib.Algebra.Algebra.Equiv
AlgHom.down_ulift_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S →ₐ[R] T) (x : ULift.{u_4, u_2} S),
  ((AlgHom.ulift.{u_4, u_6, u_5, u_1, u_2, u_3} f) x).down = f x.down
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddCommMonoidQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddCommMonoid M] → (c : ModuleCon S M) → AddCommMonoid (ModuleCon.Quotient M c)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.fan.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  CategoryTheory.Pretriangulated.productTriangle.fan T =
    CategoryTheory.Limits.Fan.mk (CategoryTheory.Pretriangulated.productTriangle T)
      (CategoryTheory.Pretriangulated.productTriangle.π T)
-- Mathlib.Order.Interval.Finset.Defs
Ici_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : αᵒᵈ),
  Finset.Ici a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic (OrderDual.ofDual a))
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates finite limits, then `F : Cᵒᵖ ⥤ D` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteLimits F.rightOp] → CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  [AddMonoidHomClass F M N] (f : F) {x : M}, IsAddUnit x → IsAddUnit (f x)
-- Mathlib.CategoryTheory.Sites.Plus
/-- `J.diagram P`, as a functor in `P`.  -/
CategoryTheory.GrothendieckTopology.diagramFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            (X : C) → CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor (J.Cover X)ᵒᵖ D)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (y : AddOreLocalization S R) (x : AddOreLocalization S X),
  y.vadd x = AddOreLocalization.liftExpand (fun x1 x2 => AddOreLocalization.vadd''✝ x1 x2 x) ⋯ y
-- Mathlib.RingTheory.WittVector.Basic
WittVector.ghostComponent_apply : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (n : ℕ) (x : WittVector p R),
  (WittVector.ghostComponent n) x = (MvPolynomial.aeval x.coeff) (wittPolynomial p ℤ n)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_def : ∀ (K : Type u_2) [inst : Field K],
  Valued.v = IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The first hexagon identity.  -/
CategoryTheory.BraidedCategory.hexagon_forward : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom))
-- Mathlib.Data.Finset.Lattice.Fold
Finset.disjoint_sup_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
  Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.map_coe_atTop : Filter.map NNReal.toReal Filter.atTop = Filter.atTop
-- Mathlib.GroupTheory.Torsion
/-- Subgroups of torsion groups are torsion groups.  -/
IsMulTorsion.subgroup : ∀ {G : Type u_1} [inst : Group G], IsMulTorsion G → ∀ (H : Subgroup G), IsMulTorsion ↥H
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_eq_getElem : ∀ {w : ℕ} (x : BitVec w) (i : ℕ) (h : i < w), x.getMsbD i = x[w - 1 - i]
-- Init.Data.SInt.Bitwise
Int16.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int16}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
        i ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv h_1)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instCharZero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  [CharZero R], CharZero (WithVal v)
-- Init.Core
Function.comp_id : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), f ∘ id = f
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_ne_zero : ∀ (n : ℕ), n.factorial ≠ 0
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology.eq_1 : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X =
    (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).inducedTopology (Opens.grothendieckTopology ↥X)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
        ⟨k, v⟩ ∈ l → ∀ {h' : (↑(m.insertMany l)).contains k' = true}, (↑(m.insertMany l)).get k' h' = cast ⋯ v
-- Lean.Parser.Syntax
Lean.Parser.Syntax.paren.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Submodule.LinearMap
Module.End.pow_restrict : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f' : M →ₗ[R] M}
  {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯),
  f'.restrict h ^ n = (f' ^ n).restrict h'
-- Mathlib.Algebra.Notation.Defs
Subsingleton.eq_zero : ∀ {α : Type u} [inst : Zero α] [Subsingleton α] (a : α), a = 0
-- Mathlib.NumberTheory.Chebyshev
/-- The Chebyshev lower bound for `ψ`.  -/
Chebyshev.psi_ge : ∀ (n : ℕ), ↑n * Real.log 2 - Real.log (↑n + 1) ≤ Chebyshev.psi ↑n
-- Init.Data.SInt.Basic
/-- Constructs an `ISize` from an `Int` that is known to be in bounds.  -/
ISize.ofIntLE : (i : ℤ) → ISize.minValue.toInt ≤ i → i ≤ ISize.maxValue.toInt → ISize
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₁.congr_simp : ∀ {w w_1 : UInt8} (e_w : w = w_1) (_w _w_1 : UInt8),
  _w = _w_1 →
    ∀ (_h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done),
      ByteArray.utf8DecodeChar?.verify₁ _w _h = ByteArray.utf8DecodeChar?.verify₁ _w_1 ⋯
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ioo_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b < c → Set.Icc a b ∪ Set.Ioo b c = Set.Ico a c
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Real powers of operators, based on the non-unital continuous functional calculus.  -/
CFC.nnrpow : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : NonUnitalRing A] →
      [inst_2 : TopologicalSpace A] →
        [inst_3 : StarRing A] →
          [inst_4 : Module ℝ A] →
            [inst_5 : SMulCommClass ℝ A A] →
              [inst_6 : IsScalarTower ℝ A A] →
                [StarOrderedRing A] →
                  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → [NonnegSpectrumClass ℝ A] → A → NNReal → A
-- Mathlib.Order.WellFoundedSet
Set.isWF_iff_no_descending_seq : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsWF ↔ ∀ (f : ℕ → α), StrictAnti f → ¬∀ (n : ℕ), f n ∈ s
-- Mathlib.Data.ENat.Lattice
ENat.exists_eq_iSup_of_lt_top : ∀ {ι : Sort u_1} {f : ι → ℕ∞} [Nonempty ι], ⨆ i, f i < ⊤ → ∃ i, f i = ⨆ i, f i
-- Mathlib.Order.Defs.PartialOrder
le_of_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → a ≤ b
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_comp'`.

---

Change of variables. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous on `f '' [a, b]`, then we can substitute `u = f x` to get
`∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.
Compared to `intervalIntegral.integral_deriv_smul_comp` we only require that `g` is continuous on
`f '' [a, b]`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_comp_smul_deriv' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) →
      ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_three' : (Matrix.reindex ((↑[0, 1]).formPerm ⋯) ((↑[0, 1]).formPerm ⋯)) (CartanMatrix.D 3) = CartanMatrix.A 3
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiff 𝕜 n f → ContDiffAt 𝕜 n f x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_erase_eq_iff_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq
-- Std.Internal.UV.System
/-- Returns the absolute path of the current executable.
 -/
Std.Internal.UV.System.exePath : IO String
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_floor_singleton : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (m : ℤ),
  Int.floor ⁻¹' {m} = Set.Ico (↑m) (↑m + 1)
-- Lean.Parser.Extra
/-- No-op parser combinator that annotates subtrees to be ignored in syntax patterns.  -/
Lean.Parser.patternIgnore : Lean.Parser.Parser → Lean.Parser.Parser