mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.commShiftFlipObj : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
        {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} →
          {inst_2 : CategoryTheory.Category.{v_5, u_5} D} →
            {M : Type u_6} →
              {inst_3 : AddCommMonoid M} →
                {inst_4 : CategoryTheory.HasShift C₁ M} →
                  {inst_5 : CategoryTheory.HasShift C₂ M} →
                    {inst_6 : CategoryTheory.HasShift D M} →
                      {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                        (h : CategoryTheory.CommShift₂Setup D M) →
                          [self : G.CommShift₂ h] → (X₂ : C₂) → (G.flip.obj X₂).CommShift M
-- Init.GrindInstances.Ring.UInt
UInt16.natCast : NatCast UInt16
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.Nilpotent.Basic
zero_isRadical_iff : ∀ {R : Type u_1} [inst : MonoidWithZero R], IsRadical 0 ↔ IsReduced R
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.addLeftStrictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)], AddLeftStrictMono (Lex (Π₀ (i : ι), α i))
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.incl.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithInitial.incl =
    { obj := CategoryTheory.WithInitial.of, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Order.Bounds.OrderIso
OrderIso.lowerBounds_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α},
  lowerBounds (⇑f '' s) = ⇑f '' lowerBounds s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.nat_le_lift_iff : ∀ {n : ℕ} {a : Cardinal.{u}}, ↑n ≤ Cardinal.lift.{v, u} a ↔ ↑n ≤ a
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
/-- A constant map between convex spaces, as a bundled affine map.  -/
Convexity.ConvexSpace.AffineMap.const : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            [inst_3 : Convexity.ConvexSpace R X] →
              [inst_4 : Convexity.ConvexSpace R Y] → Y → Convexity.ConvexSpace.AffineMap R X Y
-- Lean.Declaration
Lean.AxiomVal : Type
-- Mathlib.Data.Sym.Sym2
_private.Mathlib.Data.Sym.Sym2.0.Sym2.fromVector.match_1.eq_1 : ∀ {α : Type u_1} (motive : List.Vector α 2 → Sort u_2) (a b : α) (property : [a, b].length = 2)
  (h_1 : (a b : α) → (property : [a, b].length = 2) → motive ⟨[a, b], property⟩),
  (match ⟨[a, b], property⟩ with
    | ⟨[a, b], property⟩ => h_1 a b property) =
    h_1 a b property
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkCongrFun : Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Init.PropLemmas
not_and_of_not_or_not : ∀ {a b : Prop}, ¬a ∨ ¬b → ¬(a ∧ b)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, AddOpposite.op '' (s + t) = AddOpposite.op '' t + AddOpposite.op '' s
-- Init.Data.Bool
Bool.instCommutativeAnd : Std.Commutative fun x1 x2 => x1 && x2
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_X : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S}, PowerSeries.HasSubst a → PowerSeries.subst a PowerSeries.X = a
-- Mathlib.RingTheory.Localization.BaseChange
/-- If `A` is a localization of `R`, tensoring an `A`-module with `A` over `R` does nothing.  -/
IsLocalization.moduleLid : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_2) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              (M₁ : Type u_5) →
                [inst_4 : AddCommMonoid M₁] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module A M₁] → [IsScalarTower R A M₁] → TensorProduct R A M₁ ≃ₗ[A] M₁
-- Mathlib.Order.Heyting.Basic
OrderDual.instBiheytingAlgebra : {α : Type u_2} → [BiheytingAlgebra α] → BiheytingAlgebra αᵒᵈ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateLeft.inj : ∀ {n n_1 : ℕ}, Std.Tactic.BVDecide.BVUnOp.rotateLeft n = Std.Tactic.BVDecide.BVUnOp.rotateLeft n_1 → n = n_1
-- Mathlib.Order.Category.Preord
instFullPreordCatPreordToCat : preordToCat.Full
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.coe_addActionHom_of_embedding : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  (f : Fin n ↪ α), ↑((Set.powersetCard.addActionHom_of_embedding G α n).toFun f) = Finset.map f Finset.univ
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [inst_2 : IsLocalRing R] {x : R},
  IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal R
-- Mathlib.Order.Fin.Basic
/-- `predAbove` is injective at the pivot  -/
Fin.predAbove_left_inj : ∀ {n : ℕ} {x y : Fin n}, x.predAbove = y.predAbove ↔ x = y
-- Init.Internal.Order.Basic
Lean.Order.monotone_bind : ∀ (m : Type u → Type v) [inst : Bind m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Sort w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → m α) (g : γ → α → m β),
  Lean.Order.monotone f → Lean.Order.monotone g → Lean.Order.monotone fun x => f x >>= g x
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Opens.isDominant_homOfLE : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens},
  Dense ↑U → ∀ (hU' : U ≤ V), AlgebraicGeometry.IsDominant (X.homOfLE hU')
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.instInhabited : {d : ℤ} → Inhabited (Pell.Solution₁ d)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroupEquivFixingSubgroup.congr_simp : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g g_1 : M} (e_g : g = g_1)
  (hg : g • t = s), SubMulAction.fixingSubgroupEquivFixingSubgroup hg = SubMulAction.fixingSubgroupEquivFixingSubgroup ⋯
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Theory.IsUniversal.mk : ∀ {L : FirstOrder.Language} {T : L.Theory},
  (∀ ⦃φ : L.Sentence⦄, φ ∈ T → FirstOrder.Language.BoundedFormula.IsUniversal φ) → T.IsUniversal
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 :
    idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig.decls[idx] =
    aig.decls[idx]
-- Mathlib.RingTheory.Kaehler.Basic
/-- The kernel of `S ⊗[R] S →ₐ[R] S` is generated by `1 ⊗ s - s ⊗ 1` as an `S`-module.  -/
KaehlerDifferential.submodule_span_range_eq_ideal : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) =
    Submodule.restrictScalars S (KaehlerDifferential.ideal R S)
-- Mathlib.Data.Nat.Nth
/-- `Nat.nth p` is the least strictly monotone function whose image is contained in
`Set.ofPred p`  -/
Nat.nth_le_of_strictMonoOn_of_mapsTo : ∀ {p : ℕ → Prop} (f : ℕ → ℕ),
  Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p) →
    StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} → ∀ {n : ℕ}, Nat.nth p n ≤ f n
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.add_assoc : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X (a + b + c) (a + (b + c))
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat_k.eq_1 : ∀ (s₁ : Lean.Grind.AC.Seq),
  s₁.concat_k =
    Lean.Grind.AC.Seq.rec (motive := fun x => Lean.Grind.AC.Seq → Lean.Grind.AC.Seq)
      (fun x s₂ => Lean.Grind.AC.Seq.cons x s₂) (fun x x_1 ih s₂ => Lean.Grind.AC.Seq.cons x (ih s₂)) s₁
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.coe_torsionBy : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  ↑(Submodule.torsionBy R M a) = ⇑(DistribSMul.toLinearMap R M a) ⁻¹' {0}
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_map_of_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M},
  x ∈ S → f x ∈ AddSubmonoid.map f S
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.neg_hom_apply : ∀ {M N : AddMagmaCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.succeeded.inj : ∀ {newRapps newRapps_1 : Array Aesop.RappRef},
  Aesop.SafeRulesResult.succeeded newRapps = Aesop.SafeRulesResult.succeeded newRapps_1 → newRapps = newRapps_1
-- Mathlib.Data.Quot
Quot.induction_on : ∀ {α : Sort u_4} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r), (∀ (a : α), β (Quot.mk r a)) → β q
-- Mathlib.GroupTheory.Coset.Basic
one_leftCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), 1 • s = s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ},
  m.size ≤ (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).size
-- Mathlib.Data.ENat.Lattice
ENat.sub_iInf : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, a - ⨅ i, f i = ⨆ i, a - f i
-- Mathlib.RingTheory.PowerBasis
/-- `PowerBasis.map pb (e : S ≃ₐ[R] S')` is the power basis for `S'` generated by `e pb.gen`.  -/
PowerBasis.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          {S' : Type u_7} →
            [inst_3 : CommRing S'] → [inst_4 : Algebra R S'] → PowerBasis R S → (S ≃ₐ[R] S') → PowerBasis R S'
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (r : NNReal) (f : X → Y),
  MemHolder r f = ∃ C, HolderWith C r f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A convenience function for `PreservesLimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
 -/
CategoryTheory.Limits.isLimitOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cone K} →
                  CategoryTheory.Limits.IsLimit c →
                    [CategoryTheory.Limits.PreservesLimit K F] → CategoryTheory.Limits.IsLimit (F.mapCone c)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toDualProd_injective : ∀ {α : Type u_1} [inst : LE α], Function.Injective NonemptyInterval.toDualProd
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `le_of_smul_le_smul_left` instead.  -/
PosSMulReflectLE.le_of_smul_le_smul_left : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  [self : PosSMulReflectLE α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ ≤ a • b₂ → b₁ ≤ b₂
-- Mathlib.Data.List.Sort
List.sortedGT_iff_getElem_gt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedGT ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).functor = (Opposite.unop X).inverse
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.dual.eq_1 : ∀ {α : Type u_1}, Ordnode.nil.dual = Ordnode.nil
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ_def : AlgebraicGeometry.Scheme.Γ =
  AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.op.comp AlgebraicGeometry.LocallyRingedSpace.Γ
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.instCoeArrayByteArray : Coe (Array ByteArray) Std.Http.Internal.ChunkedBuffer
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.WF → m.keys.all p = m.all fun a x => p a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filterMap : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β β₂ γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_6 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β}
  {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)},
  forIn (Std.IterM.filterMap f it) init g =
    forIn it init fun out acc =>
      match f out with
      | some c => g c acc
      | none => pure (ForInStep.yield acc)
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_fmod : ∀ (a b : ℤ), (a.fmod b).fmod b = a.fmod b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ R : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R₀ ⟶ R) [CategoryTheory.Presheaf.IsLocallyInjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Functor Cᵒᵖ AddCommGrpCat} (φ : M₀.presheaf ⟶ A)
  [CategoryTheory.Presheaf.IsLocallyInjective J φ],
  CategoryTheory.Presheaf.IsSeparated J A →
    ∀ {X : C} (r : ↑(R.obj (Opposite.op X))) (m : ↑(A.obj (Opposite.op X))) {Y Z : C} (f : Y ⟶ X) (g : Z ⟶ Y)
      (r₀ : ↑(R₀.obj (Opposite.op Y))) (r₀' : ↑(R₀.obj (Opposite.op Z))) (m₀ : ↑(M₀.obj (Opposite.op Y)))
      (m₀' : ↑(M₀.obj (Opposite.op Z))),
      (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ =
          (CategoryTheory.ConcreteCategory.hom (R.map f.op)) r →
        (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' =
            (CategoryTheory.ConcreteCategory.hom (R.map (CategoryTheory.CategoryStruct.comp f.op g.op))) r →
          (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
              (CategoryTheory.ConcreteCategory.hom (A.map f.op)) m →
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' =
                (CategoryTheory.ConcreteCategory.hom (A.map (CategoryTheory.CategoryStruct.comp f.op g.op))) m →
              (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z)))
                  ((CategoryTheory.ConcreteCategory.hom (M₀.map g.op)) (r₀ • m₀)) =
                (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z))) (r₀' • m₀')
-- Mathlib.Topology.Constructions.SumProd
continuous_prodMk : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : X → Z}, (Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Oplax functoriality.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {K : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} K] (e : J ≌ K) {F : CategoryTheory.Functor K C}
  {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.Cocone.whisker e.functor c) ↔
    CategoryTheory.IsUniversalColimit c
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.decomp_hom_from : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (f : X ⊞ Y ⟶ Z),
  ∃ f₁ f₂,
    f =
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁ +
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Alternative `ext` lemma for `Comma.Hom`.  -/
CategoryTheory.MorphismProperty.Comma.Hom.ext' : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} {f g : X ⟶ Y},
  CategoryTheory.MorphismProperty.Comma.Hom.hom f = CategoryTheory.MorphismProperty.Comma.Hom.hom g → f = g
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_le_eq_Ici : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a : α} [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun x => a ≤ x], {x | a ≤ x} = Finset.Ici a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.stepBound_mono : Monotone SzemerediRegularity.stepBound
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The identity is `C^n`.  -/
contDiff_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}, ContDiff 𝕜 n id
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α] {k : α}, k ∈ t → t.getKey! k = k
-- Lean.Linter.Init
Lean.Linter.instInhabitedLinterSetsState : Inhabited Lean.Linter.LinterSetsState
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroup_neg_one : ∀ {G : Type u_1} [inst : Group G] (A B : Subgroup G), HNNExtension.toSubgroup A B (-1) = B
-- Init.Data.SInt.Lemmas
Int64.lt_of_le_of_lt : ∀ {a b c : Int64}, a ≤ b → b < c → a < c
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation_le_one_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x : ℚ}, (Rat.padicValuation p) x ≤ 1 ↔ ¬p ∣ x.den
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_symm_single : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι) (c : R), (b.repr.symm fun₀ | i => c) = c • b i
-- Mathlib.Data.ZMod.Basic
ZMod.val_neg_of_ne_zero : ∀ {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a], (-a).val = n - a.val
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousOn.const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {s : Set β}, ContinuousOn g s → ∀ (c : M), ContinuousOn (c • g) s
-- Init.Data.String.Basic
String.ofList_eq_empty_iff : ∀ {l : List Char}, String.ofList l = "" ↔ l = []
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertEntry_of_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  (k == a) = false →
    Std.Internal.List.getValue? a (Std.Internal.List.insertEntry k v l) = Std.Internal.List.getValue? a l
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_sum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] {ι : Type u_7} (s : Finset ι) (f : ι → V),
  WithLp.toLp p (∑ i ∈ s, f i) = ∑ i ∈ s, WithLp.toLp p (f i)
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.toSDiff : {α : Type u_1} → [self : CompleteDistribLattice α] → SDiff α
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `s : Cone F` is a limit cone, so is `s` whiskered by an equivalence `e`.  -/
CategoryTheory.Limits.IsLimit.whiskerEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cone F} →
                CategoryTheory.Limits.IsLimit s →
                  (e : K ≌ J) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Cone.whisker e.functor s)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (ea eb : Lean.Grind.AC.Expr) (a_1 b_1 : Lean.Expr) (ea_1 eb_1 : Lean.Grind.AC.Expr),
  (Lean.Meta.Grind.AC.EqCnstrProof.core a b ea eb = Lean.Meta.Grind.AC.EqCnstrProof.core a_1 b_1 ea_1 eb_1) =
    (a = a_1 ∧ b = b_1 ∧ ea = ea_1 ∧ eb = eb_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap α β compare} {k : α} {f : β → β}
  {fallback : α}, compare ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.isBotZeroClass : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)], IsBotZeroClass (Lex (Π₀ (i : ι), α i))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateJmp! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.Code pu
-- Init.Data.Nat.ToString
Nat.ofDigitChars_cons : ∀ {b : ℕ} {c : Char} {cs : List Char} {init : ℕ},
  b.ofDigitChars (c :: cs) init = b.ofDigitChars cs (b * init + (c.toNat - '0'.toNat))