mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.free.eq_1 : MonCat.free =
  { obj := fun α => MonCat.of (FreeMonoid α),
    map := fun {X Y} f => MonCat.ofHom (FreeMonoid.map ⇑(CategoryTheory.ConcreteCategory.hom f)),
    map_id := MonCat.free._proof_1, map_comp := @MonCat.free._proof_2 }
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofIntClamp_of_lt : ∀ {n : ℤ}, n < 2 ^ 7 → (Int8.ofIntClamp n).toNatClampNeg = n.toNat
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkLetS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → optParam Bool false → m Lean.Expr
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.delete.sizeOf_spec : ∀ (a : Lean.Lsp.DeleteFile), sizeOf (Lean.Lsp.DocumentChange.delete a) = 1 + sizeOf a
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.le_gaussNorm : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  PowerSeries.HasGaussNorm v c f → ∀ (t : ℕ), v ((PowerSeries.coeff t) f) * c ^ t ≤ PowerSeries.gaussNorm v c f
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (Aₚ : Type u_7)
  [inst_3 : CommSemiring Aₚ] [inst_4 : Algebra A Aₚ] (x : R) [IsLocalization.Away ((algebraMap R A) x) Aₚ],
  IsLocalization (Algebra.algebraMapSubmonoid A (Submonoid.powers x)) Aₚ
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.le_closure_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] (S : Set G), AddSubmonoid.closure S ≤ (AddSubgroup.closure S).toAddSubmonoid
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : S.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.snd R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst S.hom T.hom) h)
-- Init.Data.List.Attach
List.attach_map_subtype_val : ∀ {α : Type u_1} (l : List α), List.map Subtype.val l.attach = l
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size + 1
-- Mathlib.Data.String.Lemmas
_private.Mathlib.Data.String.Lemmas.0.String.IsPrefix.match_1.splitter : (motive : String → String → Sort u_1) → (x x_1 : String) → ((d1 d2 : String) → motive d1 d2) → motive x x_1
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepSets_comap_of_bcf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} [inst : TopologicalSpace G]
  [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G] {Z : Ω → G}
  [MeasureTheory.IsProbabilityMeasure P] {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    AEMeasurable Z P →
      (∀ A ∈ 𝒜, ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.simpTrace : Lean.ParserDescr
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract : ∀ {b : ByteArray} {i : ℕ} {h : (b.utf8DecodeChar? i).isSome = true},
  b.utf8DecodeChar i h = (b.extract i b.size).utf8DecodeChar 0 ⋯
-- Mathlib.Analysis.Normed.Module.RCLike.Real
nnnorm_surjective : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E], Function.Surjective nnnorm
-- Mathlib.CategoryTheory.Action.Limits
Action.instPreadditive : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → CategoryTheory.Preadditive (Action V G)
-- Lean.Parser.Command
Lean.Parser.Command.structSimpleBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPSnd_comp_forget_to_bipointed : pointedToTwoPSnd.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedSnd
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ} (m : ℕ)
  (hm : n + 1 = m), R.extMk 0 m hm ⋯ = 0
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instAdd : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → {ι : Type u_7} → Add (M [⋀^ι]→ₗ[R] N)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.comp_compMultilinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} {M₄ : Type v₄} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : AddCommMonoid M₄] [inst_5 : (i : ι) → Module R (M₁ i)] [inst_6 : Module R M₂] [inst_7 : Module R M₃]
  [inst_8 : Module R M₄] (g : M₃ →ₗ[R] M₄) (g' : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂),
  (g ∘ₗ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup.append_right : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubMulAction.ofFixingSubgroup M s)) (i : Fin n),
  (SubMulAction.ofFixingSubgroup.append x) (Fin.natAdd s.ncard i) = ↑(x i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.values_eq_map : ∀ {α : Type u} {β : Type v} {l : List ((_ : α) × β)}, Std.Internal.List.values l = List.map (fun x => x.snd) l
-- Init.Data.Array.MinMax
Array.isSome_max?_of_ne_empty : ∀ {α : Type u_1} [inst : Max α] (xs : Array α), xs ≠ #[] → xs.max?.isSome = true
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  [inst_5 : NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ),
  curveIntegralFun ω γ t = (ω (γ.extend t)) (derivWithin (⇑γ.extend) unitInterval t)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.instSMulCarrierPtOppositeRingCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      [CategoryTheory.IsCofiltered C] →
        [CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              (hcR : CategoryTheory.Limits.IsColimit cR) →
                {M : PresheafOfModules R} →
                  {cM : CategoryTheory.Limits.Cocone M.presheaf} →
                    (hcM : CategoryTheory.Limits.IsColimit cM) → SMul (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `inv_mul_lt_iff_lt_mul`. -/
inv_mul_lt_of_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a < b * c → b⁻¹ * a < c
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
/-- If `f : α → ℝ≥0∞` has finite integral, then there exists a measurable set `s` of finite measure
such that the integral of `f` over `sᶜ` is less than a given positive number.

Also used to prove an `Lᵖ`-norm version in
`MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_le`.  -/
MeasureTheory.exists_setLIntegral_compl_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ a = b * star b
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.map_iff_of_leftInverse : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4} {G' : Type u_5}
  [inst_4 : FunLike G α γ] [MonoidHomClass G α γ] [inst_6 : FunLike G' γ α] [MonoidHomClass G' γ α] (g : G) (g' : G'),
  Continuous ⇑g → Continuous ⇑g' → Function.LeftInverse ⇑g' ⇑g → (Multipliable (⇑g ∘ f) L ↔ Multipliable f L)
-- Mathlib.Dynamics.Flow
Flow.mem_orbit_iff : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) {x₁ x₂ : α}, x₂ ∈ ϕ.orbit x₁ ↔ ∃ t, ϕ.toFun t x₁ = x₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_iso_inv_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).iso.inv.app X_1 = (J.obj X_1).iso.inv
-- Mathlib.CategoryTheory.Filtered.Small
/-- One step of the inductive procedure consists of adjoining all maxima and coequalizers of all
objects and morphisms obtained so far. This is quite redundant, picking up many objects which we
already hit in earlier iterations, but this is easier to work with later.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] → (n : ℕ) → ((k : ℕ) → k < n → (t : Type (max v w)) × (t → C)) → Type (max v w)
-- Batteries.Data.UnionFind.Basic
/-- Link two union-find nodes, uniting their respective classes.  -/
Batteries.UnionFind.union : (self : Batteries.UnionFind) → Fin self.size → Fin self.size → Batteries.UnionFind
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_mem' : ∀ {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  γ ∈ CongruenceSubgroup.Gamma N ↔ (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffDist.eq_1 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s t : Set α), Metric.hausdorffDist s t = (Metric.hausdorffEDist s t).toReal
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
/-- If `X` is geometrically reduced over `S`, and `Y` is both reduced and locally noetherian,
then `X ×ₛ Y` is also reduced.

TODO: get rid of the noetherian hypothesis.  -/
AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyReduced f]
  [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsReduced Y] [AlgebraicGeometry.IsLocallyNoetherian Y],
  AlgebraicGeometry.IsReduced (CategoryTheory.Limits.pullback f g)
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.traceHint : Lean.MessageData
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instCommMonoid : {α : Type u} → [CommSemigroup α] → CommMonoid (WithOne α)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starAlgHom_ext_iff : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  {φ ψ : Unitization R A →⋆ₐ[R] C},
  φ = ψ ↔ (↑φ).comp (Unitization.inrNonUnitalStarAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalStarAlgHom R A)
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
/-- When `F` is given the monoidal structure `functorMonoidalOfComp` that is obtained by lifting along
a monoidal localization functor `L`, then the lifting isomorphism is a monoidal natural
transformation.
 -/
CategoryTheory.Localization.Monoidal.lifting_isMonoidal : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Localization.Lifting.iso L W G F).hom
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- associativity of the tensorator  -/
CategoryTheory.Functor.OplaxMonoidal.oplax_associativity : ∀ {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.OplaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z)))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.getVert_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {w : V} [inst : DecidableEq V] {u v : V} {n : ℕ} {p : G.Walk u v}
  (hw : w ∈ p.support), n ≤ (p.takeUntil w hw).length → (p.takeUntil w hw).getVert n = p.getVert n
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X_1 Y : C₁} (f : X_1 ⟶ Y)
  (X_2 : C₂) (X_3 : C₃),
  ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).map f).app X_2).app X_3 =
    ((X.map (F₁.map f)).app (F₂.obj X_2)).app (F₃.obj X_3)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_apply_le : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedAdd M] {a : α}
  {s : Set α} {f g : α → M}, (a ∈ s → f a ≤ g a) → s.indicator f a ≤ g a
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF)
  {a fallback : α}, m.getKeyD a fallback = Std.DHashMap.Internal.Raw₀.getKeyD ⟨m, ⋯⟩ a fallback
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.diagonal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y},
  P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f)
-- Lean.Structure
/-- If this field is for a subobject (i.e., an embedded parent structure), contains the name of the parent structure.  -/
Lean.StructureFieldInfo.subobject? : Lean.StructureFieldInfo → Option Lean.Name
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `support_getElem_one` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.snd_eq_support_getElem_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hnil : ¬p.Nil), p.snd = p.support[1]
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldl_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : δ → α → δ} {init : δ},
  List.foldl (fun a b => f a b.fst) init l = List.foldl f init (Std.Internal.List.keys l)
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_neg_mul_exp_self : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a : A},
  IsNilpotent a → IsNilpotent.exp (-a) * IsNilpotent.exp a = 1
-- Init.Data.List.TakeDrop
List.head_dropWhile_not : ∀ {α : Type u_1} (p : α → Bool) {l : List α} (w : List.dropWhile p l ≠ []), p ((List.dropWhile p l).head w) = false
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 →
    ∀ (I I_1 : FractionalIdeal (nonZeroDivisors R) K),
      I = I_1 → FractionalIdeal.count K v I = FractionalIdeal.count K v_1 I_1
-- Lean.ResolveName
/-- Given a namespace identifier, return a list of possible interpretations.  -/
Lean.resolveNamespace : {m : Type → Type} →
  [Monad m] → [Lean.MonadResolveName m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Ident → m (List Lean.Name)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is maximized when `f` and
`g` monovary together. Stated by permuting the entries of `f`.  -/
Monovary.sum_comp_perm_mul_le_sum_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι], Monovary f g → ∑ i, f (σ i) * g i ≤ ∑ i, f i * g i
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Algebra equivalence between the linear maps and continuous linear maps on a finite-dimensional
space.  -/
Module.End.toContinuousLinearMap : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      (E : Type v) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → (E →ₗ[𝕜] E) ≃ₐ[𝕜] E →L[𝕜] E
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (a : Lean.Grind.CommRing.Expr),
  x = a.neg →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_8 a
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.equalizerCondition_w' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {X B : C}
  (π : X ⟶ B) [inst_1 : CategoryTheory.Limits.HasPullback π π],
  CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map (CategoryTheory.Limits.pullback.fst π π).op) =
    CategoryTheory.CategoryStruct.comp (P.map π.op) (P.map (CategoryTheory.Limits.pullback.snd π π).op)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.List.headI.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (tail : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (tail : List α) → motive (a :: tail)),
  (match a :: tail with
    | [] => h_1 ()
    | a :: tail => h_2 a tail) =
    h_2 a tail
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.M : Type → Type
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a<...=b`
by varying the upper bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a`, the statement holds for the empty range `a<...=b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, if the
statement holds for `a<...=b`, it also holds for the larger range `a<...=(b + 1)`.

The following is an example reproving `length_toList_roc`.

```
example (a b : Int) : (a<...=b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_roc_right
  case base =>
    simp only [Int.toList_roc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step a b hle ih =>
    rw [Int.toList_roc_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega
``` -/
Int.induct_roc_right : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a → motive a b) → (∀ (a b : ℤ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℤ), motive a b