mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (U : CategoryTheory.Over Y),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).counit.app
      U =
    CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.snd X U.left) ⋯
-- Lean.Parser.Term
Lean.Parser.Term.letExpr.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Tactic.GeneralizeProofs
/-- The maximum recursion depth when generalizing proofs.
When `maxDepth > 0`, then proofs are generalized from the types of the generalized proofs too.  -/
Batteries.Tactic.GeneralizeProofs.Config.maxDepth : Batteries.Tactic.GeneralizeProofs.Config → ℕ
-- Mathlib.CategoryTheory.PUnit
/-- The constant functor sending everything to `PUnit.star`.  -/
CategoryTheory.Functor.star : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})
-- Init.Data.BitVec.Bitblast
BitVec.sdiv_ne_intMin_of_ne_intMin : ∀ {w : ℕ} {x y : BitVec w}, x ≠ BitVec.intMin w → x.sdiv y ≠ BitVec.intMin w
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Iso.inv_hom_id_app_apply`. -/
CategoryTheory.FunctorToTypes.inv_hom_id_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (G.obj X)),
  (CategoryTheory.ConcreteCategory.hom (α.hom.app X)) ((CategoryTheory.ConcreteCategory.hom (α.inv.app X)) x) = x
-- Mathlib.NumberTheory.FLT.Three
/-- Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then
`a ^ 3 + b ^ 3 ≠ c ^ 3`.  -/
fermatLastTheoremThree : FermatLastTheoremFor 3
-- Mathlib.Data.Finset.Max
Finset.max'_erase_ne_self : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty), (s.erase x).max' s0 ≠ x
-- Init.PropLemmas
not_exists : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) ↔ ∀ (x : α), ¬p x
-- Mathlib.Order.RelClasses
IsNonstrictStrictOrder.mk : ∀ {α : Type u_1} {r : semiOutParam (α → α → Prop)} {s : α → α → Prop},
  (∀ (a b : α), s a b ↔ r a b ∧ ¬r b a) → IsNonstrictStrictOrder α r s
-- Init.Data.String.Lemmas.StringOrder
String.le_total : ∀ (a b : String), a ≤ b ∨ b ≤ a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorHom.match_1.splitter : (motive : (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) → (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → Sort u_1) →
  (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) →
    (f₁ : x₁ ⟶ y₁) →
      (f₂ : x₂ ⟶ y₂) →
        ((a a_1 a_2 a_3 : SimplexCategory) →
            (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
              (f₂ : CategoryTheory.WithInitial.of a_2 ⟶ CategoryTheory.WithInitial.of a_3) →
                motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1)
                  (CategoryTheory.WithInitial.of a_2) (CategoryTheory.WithInitial.of a_3) f₁ f₂) →
          ((a y₁ y₂ : SimplexCategory) →
              (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₁) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₂) →
                  motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of y₁)
                    CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of y₂) f₁ x) →
            ((y₁ a y₂ : SimplexCategory) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₁) →
                  (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₂) →
                    motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of y₁)
                      (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of y₂) x f₂) →
              ((a a_1 : SimplexCategory) →
                  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                    (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
                      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star
                        (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) x f₂) →
                ((a a_1 : SimplexCategory) →
                    (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
                      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1)
                          CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star f₁ x) →
                  ((x x_1 : AugmentedSimplexCategory) →
                      (x_2 : CategoryTheory.WithInitial.star ⟶ x) →
                        (x_3 : CategoryTheory.WithInitial.star ⟶ x_1) →
                          motive CategoryTheory.WithInitial.star x CategoryTheory.WithInitial.star x_1 x_2 x_3) →
                    motive x₁ y₁ x₂ y₂ f₁ f₂
-- Mathlib.Algebra.Group.Invertible.Basic
val_inv_unitOfInvertible : ∀ {α : Type u} [inst : Monoid α] (a : α) [inst_1 : Invertible a], ↑(unitOfInvertible a)⁻¹ = ⅟a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty =
        ((t.isEmpty || t.size == 1 && Std.DTreeMap.Internal.Impl.contains k t) &&
          (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_prod_prod : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H₁ H₂ : Subgroup G) (K₁ K₂ : Subgroup G'),
  ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.curryEquiv_symm_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [inst_4 : ∀ (i : ι), LocallyCompactSpace (X i)] [inst_5 : ∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)]
  (g : Topology.ContinuousMapGeneratedBy X Z (Topology.ContinuousMapGeneratedBy X Y T)) (y : Y) (z : Z),
  (Topology.ContinuousMapGeneratedBy.curryEquiv.symm g) (y, z) = (g z) y
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Multipliable.mono_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L₁ L₂ : SummationFilter β}, Multipliable f L₂ → L₁.filter ≤ L₂.filter → Multipliable f L₁
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f` is a Hölder continuous map with exponent `r > 0`, then `dimH (f '' s) ≤ dimH s / r`.  -/
HolderOnWith.dimH_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → 0 < r → dimH (f '' s) ≤ dimH s / ↑r
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instNeg.eq_1 : ∀ {α : Type u_1} [inst : Neg α], Colex.instNeg = inst
-- Init.Sym.Lemmas
Lean.Sym.decide_prop_eq_false : ∀ (p : Prop) {inst : Decidable p}, p = False → decide p = false
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceCyclesE : ∀ {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) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂), CategoryTheory.Epi (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g
-- Mathlib.Data.List.Sigma
List.mem_dlookup_iff : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
  l.NodupKeys → (b ∈ List.dlookup a l ↔ ⟨a, b⟩ ∈ l)
-- Mathlib.Order.Category.LinOrd
LinOrd.dualEquiv_inverse : LinOrd.dualEquiv.inverse = LinOrd.dual
-- Mathlib.Order.Heyting.Hom
CoheytingHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : CoheytingAlgebra α} {inst_1 : CoheytingAlgebra β}
  {toLatticeHom : LatticeHom α β} {map_top' : toLatticeHom.toFun ⊤ = ⊤}
  {map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b}
  {toLatticeHom_1 : LatticeHom α β} {map_top'_1 : toLatticeHom_1.toFun ⊤ = ⊤}
  {map_sdiff'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a \ b) = toLatticeHom_1.toFun a \ toLatticeHom_1.toFun b},
  { toLatticeHom := toLatticeHom, map_top' := map_top', map_sdiff' := map_sdiff' } =
      { toLatticeHom := toLatticeHom_1, map_top' := map_top'_1, map_sdiff' := map_sdiff'_1 } →
    toLatticeHom = toLatticeHom_1
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_1 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property none)
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨none, h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_1 h'
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whisker a 1-morphism to a lift.
```
                    b
                  ◹ |
           lift /   |      △
              /     | f    | unit
            /       ▽
x - - - ▷ c - - - ▷ a
     h         g
```
 -/
CategoryTheory.Bicategory.LeftLift.whisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          CategoryTheory.Bicategory.LeftLift f g →
            {x : B} → (h : x ⟶ c) → CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.inductionOn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {motive : T2Quotient X → Prop} (q : T2Quotient X),
  (∀ (x : X), motive (T2Quotient.mk x)) → motive q
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_eq_zero_iff : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀},
  s.prod = 0 ↔ 0 ∈ s
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.add : {A : Type u} → {M : Type v} → M → M → Module.Presentation.tautological.R A M
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mulNat_eq_mul : ∀ (n : ℕ) (o : ONote), o.mulNat n = o * ↑n
-- Mathlib.Computability.Primrec.Basic
Primrec.option_getD_default : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : Inhabited α], Primrec fun o => o.getD default
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.next?.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Stream α → Sort u_2) (v : α) (r : RBTree.RBNode α)
  (tail : RBTree.RBNode.Stream α) (h_1 : Unit → motive RBTree.RBNode.Stream.nil)
  (h_2 :
    (v : α) → (r : RBTree.RBNode α) → (tail : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.Stream.cons v r tail)),
  (match RBTree.RBNode.Stream.cons v r tail with
    | RBTree.RBNode.Stream.nil => h_1 ()
    | RBTree.RBNode.Stream.cons v r tail => h_2 v r tail) =
    h_2 v r tail
-- Mathlib.Topology.Algebra.FilterBasis
/-- If a ring is endowed with a topological structure coming from
a ring filter basis then it's a topological ring.  -/
RingFilterBasis.isTopologicalRing : ∀ {R : Type u} [inst : Ring R] (B : RingFilterBasis R), IsTopologicalRing R
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp._auto_3) {Z : C}
  (h :
    X'.E (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄) (CategoryTheory.homOfLE hi₄₅) n₀ n₁ n₂ hn₁ hn₂ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₃ i₄ i₅ hi₀₁ ⋯ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_iSup₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {ι : Sort u_1}
  {κ : ι → Sort u_2} (s : (i : ι) → κ i → X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (⨆ i, ⨆ j, s i j) =
    ⨆ i, ⨆ j, (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (s i j)
-- Mathlib.Order.Directed
DirectedOn.mono : ∀ {α : Type u_1} {r r' : α → α → Prop} {s : Set α}, DirectedOn r s → (∀ ⦃a b : α⦄, r a b → r' a b) → DirectedOn r' s
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_of_unop : ∀ {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.PreservesColimits F.unop],
  CategoryTheory.Limits.PreservesLimits F
-- Lean.Meta.Sym.DSimp.DSimpM
_private.Lean.Meta.Sym.DSimp.DSimpM.0.Lean.Meta.Sym.DSimp.MethodsRefPointed : NonemptyType
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.Constraint.isImpossible.match_1.eq_1 : ∀ (motive : Lean.Omega.Constraint → Sort u_1) (x y : ℤ)
  (h_1 : (x y : ℤ) → motive { lowerBound := some x, upperBound := some y })
  (h_2 : (x : Lean.Omega.Constraint) → motive x),
  (match { lowerBound := some x, upperBound := some y } with
    | { lowerBound := some x, upperBound := some y } => h_1 x y
    | x => h_2 x) =
    h_1 x y
-- Mathlib.Data.Set.Image
Prod.range_fst : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β], Set.range Prod.fst = Set.univ
-- Mathlib.Data.Rat.Defs
Rat.den_one : Rat.den 1 = 1
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] → [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → (E₁ →ₚ[R] E₂) → E₁ →ₗ[R] E₂
-- Lean.Util.FindExpr
/-- Found desired subterm  -/
Lean.Expr.FindStep.found : Lean.Expr.FindStep
-- Init.Data.Int.OfNat
Nat.ToInt.ofNat_toNat : ∀ (a : ℤ), ↑a.toNat = if a ≤ 0 then 0 else a
-- Init.Prelude
/-- A macro scope identifier is just a `Nat` that gets bumped every time we
enter a new macro scope. Within a macro scope, all occurrences of identifier `x`
parse to the same thing, but `x` parsed from different macro scopes will
produce different identifiers.
 -/
Lean.MacroScope : Type
-- Mathlib.Order.CompleteLattice.Basic
iInf_or : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∨ q → α},
  ⨅ (x : p ∨ q), s x = (⨅ (i : p), s ⋯) ⊓ ⨅ (j : q), s ⋯
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_mul_mul_comm : ∀ {S : Type u_3} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a b : B} {a' : C} {f g : a ⟶ b}
  (β : f ⟶ g) (h : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addCommSemigroup : {α : Type u} → [AddCommSemigroup α] → AddCommSemigroup (WithBot α)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.mk.injEq : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H]
  (toClosedSubmodule : ClosedSubmodule ℝ H) (IsSeparating : toClosedSubmodule ⊓ toClosedSubmodule.mulI = ⊥)
  (IsCyclic : toClosedSubmodule ⊔ toClosedSubmodule.mulI = ⊤) (toClosedSubmodule_1 : ClosedSubmodule ℝ H)
  (IsSeparating_1 : toClosedSubmodule_1 ⊓ toClosedSubmodule_1.mulI = ⊥)
  (IsCyclic_1 : toClosedSubmodule_1 ⊔ toClosedSubmodule_1.mulI = ⊤),
  ({ toClosedSubmodule := toClosedSubmodule, IsSeparating := IsSeparating, IsCyclic := IsCyclic } =
      { toClosedSubmodule := toClosedSubmodule_1, IsSeparating := IsSeparating_1, IsCyclic := IsCyclic_1 }) =
    (toClosedSubmodule = toClosedSubmodule_1)
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.reduceDIte' : ℕ → Bool → Lean.Meta.Simp.Simproc
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced.instDecidableRel_adj : {α : 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] → {ε δ : 𝕜} → DecidableRel (SimpleGraph.regularityReduced P G ε δ).Adj
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  k ∈ t₂ → Std.ExtDTreeMap.Const.getD (t₁ ∩ t₂) k fallback = Std.ExtDTreeMap.Const.getD t₁ k fallback
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Right homotopy is a transitive relation.  -/
CategoryTheory.Arrow.RightHomotopy.trans : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {e f g : u ⟶ v} →
          CategoryTheory.Arrow.RightHomotopy e f →
            CategoryTheory.Arrow.RightHomotopy f g → CategoryTheory.Arrow.RightHomotopy e g
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instMulActionQuotientOfIsScalarTower : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid α] →
      [inst_1 : NonAssocSemiring R] →
        [inst_2 : MulAction α R] → [IsScalarTower α R R] → (c : RingCon R) → MulAction α c.Quotient
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy oy of `mul_right_eq_iff_eq_mul_invOf` for rectangular matrices.  -/
Matrix.mul_right_eq_iff_eq_mul_invOf : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  {A B : Matrix m n α} {C : Matrix n n α} [inst_3 : Invertible C], A * C = B ↔ A = B * ⅟C
-- Mathlib.Data.Fin.Fin2
Fin2.rev_castSucc : ∀ {n : ℕ} (i : Fin2 n), i.castSucc.rev = i.rev.fs
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The morphism `K.cylinder ⟶ F` that is induced by two morphisms `φ₀ φ₁ : K ⟶ F`
and a homotopy `h : Homotopy φ₀ φ₁`.  -/
HomologicalComplex.cylinder.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F K : HomologicalComplex C c} →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → (φ₀ φ₁ : K ⟶ F) → Homotopy φ₀ φ₁ → (K.cylinder ⟶ F)
-- Aesop.Options.Public
Aesop.Strategy.breadthFirst.sizeOf_spec : sizeOf Aesop.Strategy.breadthFirst = 1
-- Mathlib.Analysis.Complex.Exponential
Real.add_one_lt_exp : ∀ {x : ℝ}, x ≠ 0 → x + 1 < Real.exp x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of the forward direction of `hasFDerivWithinAt_univ`. -/
HasFDerivWithinAt.hasFDerivAt_of_univ : ∀ {𝕜 : 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} {f' : E →L[𝕜] F} {x : E},
  HasFDerivWithinAt f f' Set.univ x → HasFDerivAt f f' x
-- Init.Data.SInt.Lemmas
Int8.toInt32_ofNat : ∀ {n : ℕ}, n ≤ 127 → (OfNat.ofNat n).toInt32 = OfNat.ofNat n
-- Mathlib.Order.JordanHolder
CompositionSeries.strictMono : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X), StrictMono s.toFun
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_subset' : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.dedup ⊆ t ↔ s ⊆ t
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndPureAnd_1 : ∀ {φ ψ : Prop} (σs : List (Type u_1)) (P Q : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame P Q ψ],
  Std.Do.SPred.Tactic.HasFrame spred(P ∧ ⌜φ⌝) Q (ψ ∧ φ)
-- Init.Conv
/-- `conv` is the syntax category for a "conv tactic", where "conv" is short
for conversion. A conv tactic is a program which receives a target, printed as
`| a`, and is tasked with coming up with some term `b` and a proof of `a = b`.
It is mainly used for doing targeted term transformations, for example rewriting
only on the left side of an equality.  -/
Lean.Parser.Category.conv : Lean.Parser.Category
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.revSkipWhile_char_eq_revSkipWhile_beq : ∀ {c : Char} {s : String.Slice} (curr : s.Pos), curr.revSkipWhile c = curr.revSkipWhile fun x => x == c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.negAddY P P = 0
-- Mathlib.Data.Sum.Order
WithBot.orderIsoPUnitSumLex_symm_inr : ∀ {α : Type u_1} [inst : LE α] (a : α), WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inr a)) = ↑a
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.smul_Spec_def : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U : (AlgebraicGeometry.Spec R).Opens} (r : ↑R)
  (x : ↑(M.presheaf.obj (Opposite.op U))),
  r • x =
    (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Spec R).presheaf.map (TopologicalSpace.Opens.leTop U).op))
        ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) r) •
      x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  (a : A), 0 ≤ a⁺