mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : β k → β k} {hc : k ∈ Std.DTreeMap.Internal.Impl.modify k f t},
  (Std.DTreeMap.Internal.Impl.modify k f t).get k hc = f (t.get k ⋯)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.mk.injEq : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (textDocument : Lean.Lsp.TextDocumentIdentifier) (range : Lean.Lsp.Range) (context : Lean.Lsp.CodeActionContext)
  (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams)
  (toPartialResultParams_1 : Lean.Lsp.PartialResultParams) (textDocument_1 : Lean.Lsp.TextDocumentIdentifier)
  (range_1 : Lean.Lsp.Range) (context_1 : Lean.Lsp.CodeActionContext),
  ({ toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument, range := range, context := context } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        textDocument := textDocument_1, range := range_1, context := context_1 }) =
    (toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧
        textDocument = textDocument_1 ∧ range = range_1 ∧ context = context_1)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Equivalence.property_step : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Monad m] [LawfulMonad m]
  {it : Std.IterM m β}, it.stepAsHetT.Property = it.IsPlausibleStep
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- the map function for the functor `Cofix F`  -/
MvQPF.Cofix.map : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α β : TypeVec.{u} n} → α.Arrow β → MvQPF.Cofix F α → MvQPF.Cofix F β
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [IsOrderedAddMonoid β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r < f x}
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.mul_reindexLinearEquiv_one : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : Semiring A] [inst_2 : Module R A] [inst_3 : Fintype n] [inst_4 : DecidableEq o] (e₁ : o ≃ n) (e₂ : o ≃ n')
  (M : Matrix m n A),
  M * (Matrix.reindexLinearEquiv R A e₁ e₂) 1 = (Matrix.reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂)) M
-- Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
/-- The augmentation map `((singularHomologyFunctor C 0).obj R).obj X ⟶ R`.  -/
TopCat.singularHomology₀ε : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.CategoryWithHomology C] →
          (X : TopCat) → (R : C) → ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ⟶ R
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.setENode.unsafe_impl_2 : (e : Lean.Expr) →
  (n : Lean.Meta.Grind.ENode) →
    (s : Lean.Meta.Grind.Goal) → Lean.Meta.Grind.CongrTable (Lean.PersistentHashMap.insert s.enodeMap { expr := e } n)
-- Batteries.Data.BinomialHeap.Basic
/-- The forest after the minimum element.  -/
Batteries.BinomialHeap.Imp.FindMin.next : {α : Type u_1} → Batteries.BinomialHeap.Imp.FindMin α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.AlgebraicGeometry.Gluing
/-- The underlying topological space of the glued scheme is isomorphic to the gluing of the
underlying spaces  -/
AlgebraicGeometry.Scheme.GlueData.isoCarrier : (D : AlgebraicGeometry.Scheme.GlueData) →
  ↑D.glued.toPresheafedSpace ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineBasis.finite_set : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [FiniteDimensional k V] {s : Set ι} (b : AffineBasis (↑s) k P),
  s.Finite
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Construct a modification isomorphism between lax natural transformations
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Lax.LaxTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
                  CategoryTheory.Lax.LaxTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedNatTrans.mk.sizeOf_spec : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} [inst_4 : SizeOf V] [inst_5 : SizeOf C] [inst_6 : SizeOf D]
  (out : F.forget ⟶ G.forget), sizeOf { out := out } = 1 + sizeOf out
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The short root `2α + β`.  -/
RootPairing.EmbeddedG2.twoShortAddLongRoot : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → [P.EmbeddedG2] → M
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.semilatticeInf : {α : Type u_1} → [SemilatticeInf α] → SemilatticeInf (WithZero α)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] (α : C ≌ D), CategoryTheory.IsGrothendieckAbelian.{w, v₂, u₂} D
-- Mathlib.Topology.Connected.PathConnected
mem_pathComponent_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ∈ pathComponent y → y ∈ pathComponent x
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Class that expresses the fact that three ring homomorphisms form a composition triple. This is
used to handle composition of semilinear maps.  -/
RingHomCompTriple : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : Semiring R₁] →
        [inst_1 : Semiring R₂] → [inst_2 : Semiring R₃] → (R₁ →+* R₂) → (R₂ →+* R₃) → outParam (R₁ →+* R₃) → Prop
-- Mathlib.Order.Atoms
isCoatomic_of_orderTop_gt_wellFounded : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α], (WellFounded fun x1 x2 => x1 > x2) → IsCoatomic α
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_star_mul_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), star ↑U * ↑U = 1
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_hom_rightUnitor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    M.form.tensorRId.toIsometry
-- Mathlib.Algebra.Group.Commute.Defs
Commute.right_comm : ∀ {S : Type u_3} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a : S), a * b * c = a * c * b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidalStruct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMon.monMonoidalStruct =
    {
      tensorObj := fun M N =>
        { X := CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X,
          addMon := CategoryTheory.AddMonObj.tensorObj.instTensorObj },
      whiskerLeft := fun X x x_1 g =>
        { hom := CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X g.hom, isAddMonHom_hom := ⋯ },
      whiskerRight := fun {X₁ X₂} f Y =>
        { hom := CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X, isAddMonHom_hom := ⋯ },
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g =>
        { hom := CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom, isAddMonHom_hom := ⋯ },
      tensorUnit :=
        { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C,
          addMon := CategoryTheory.AddMonObj.instTensorAddUnit },
      associator := fun M N P =>
        CategoryTheory.AddMon.mkIso' (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X),
      leftUnitor := fun M => CategoryTheory.AddMon.mkIso' (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X),
      rightUnitor := fun M => CategoryTheory.AddMon.mkIso' (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X) }
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- The canonical isomorphism `((shiftFunctor C n).obj K).X i ≅ K.X m` when `m = i + n`.  -/
CochainComplex.shiftFunctorObjXIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : CochainComplex C ℤ) → (n i m : ℤ) → m = i + n → (((CochainComplex.shiftFunctor C n).obj K).X i ≅ K.X m)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Left identity of the `L^p` product as an isometric equivalence.  -/
IsometryEquiv.withLpUniqueProd : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] →
        [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → [Unique α] → WithLp p (α × β) ≃ᵢ β
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.Internal.List.alterKey_cons_perm.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} {k : α} (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_le_succ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) (x : X),
  Urysohns.CU.approx n c x ≤ Urysohns.CU.approx (n + 1) c x
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.ext_iff : ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M}, S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).toList = []
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_natural_left : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map f)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))
      (CategoryTheory.Localization.Monoidal.μ L W ε X₂ Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₁ Y).hom
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
-- Mathlib.Order.Defs.LinearOrder
compare_ge_iff_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, compare a b ≠ Ordering.lt ↔ b ≤ a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.ediam_Ioc : ∀ (a b : ℝ), Metric.ediam (Set.Ioc a b) = ENNReal.ofReal (b - a)
-- Mathlib.Control.Random
Random.instFinOfNeZeroNat : {m : Type → Type u_1} → [Monad m] → {n : ℕ} → [NeZero n] → Random m (Fin n)
-- Init.Data.UInt.Lemmas
UInt32.add_eq_right : ∀ {a b : UInt32}, a + b = b ↔ a = 0
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_iff_subset_iUnion_closedEBall : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, Metric.closedEBall y ↑ε
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → x ∈ F ∧ y ∈ F
-- Mathlib.Order.Hom.Bounded
TopHom.instOrderTop : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [inst_1 : LE β] → [inst_2 : OrderTop β] → OrderTop (TopHom α β)
-- Mathlib.Algebra.Algebra.StrictPositivity
IsUnit.isStrictlyPositive_star_left_conjugate_iff : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A] {u a : A},
  IsUnit u → (IsStrictlyPositive (star u * a * u) ↔ IsStrictlyPositive a)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isClosed_eqLocus : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [T2Space M₂] (f g : M₁ →SL[σ₁₂] M₂),
  IsClosed ↑((↑f).eqLocus ↑g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two monotone functions is monotone.  -/
MonotoneOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftMono α] [AddRightMono α], MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x + g x) s
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_rii : ∀ {α : Type u_1} {xs : Subarray α}, Std.Rii.Sliceable.mkSlice xs *...* = xs
-- Mathlib.Order.Filter.Partial
Filter.ptendsto'_of_ptendsto : ∀ {α : Type u} {β : Type v} {f : α →. β} {l₁ : Filter α} {l₂ : Filter β},
  f.Dom ∈ l₁ → Filter.PTendsto f l₁ l₂ → Filter.PTendsto' f l₁ l₂
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.isTerminalΩ₀`.

---

Given `c : Classifier C`, `c.Ω₀` is a terminal object.
Prefer `c.χ₀` over `c.isTerminalΩ₀.from`.  -/
CategoryTheory.Classifier.isTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {c : CategoryTheory.Subobject.Classifier C} → CategoryTheory.Limits.IsTerminal c.Ω₀
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel (ProbabilityTheory.Kernel.prodMkLeft γ κ)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Colon
/-- A minimal prime over an ideal of the form `N.colon {x}` in a Noetherian ring is
itself an ideal of the form `N.colon {x'}`.  -/
Submodule.exists_eq_colon_of_mem_minimalPrimes : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R} {x : M} [IsNoetherianRing R],
  I ∈ (N.colon {x}).minimalPrimes → ∃ x', I = N.colon {x'}
-- Mathlib.Order.BooleanAlgebra.Basic
Disjoint.sdiff_eq_of_sup_eq : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], Disjoint x z → x ⊔ z = y → y \ x = z
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_bilin_of_stronglyMeasurable_right : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace F]
  {f : Ω → F} {g : Ω → E},
  MeasureTheory.StronglyMeasurable g →
    MeasureTheory.Integrable (fun ω => (B (f ω)) (g ω)) μ →
      MeasureTheory.Integrable f μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (μ[f | m] ω)) (g ω)
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.binaturality : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
  (fun {α} => η.app α) (bitraverse f f' x) = bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f') x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.Hom.w_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (φ : f ⟶ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right φ) h) =
    CategoryTheory.CategoryStruct.comp g.hom h
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- `true` if `r` can depend on the maximal ratio of sides of the
same box of a partition. Presence of this case makes quite a few proofs harder but we can prove
the divergence theorem only for the filter `BoxIntegral.IntegrationParams.GP = ⊥ =
{bRiemann := false, bHenstock := true, bDistortion := true}`.  -/
BoxIntegral.IntegrationParams.bDistortion : BoxIntegral.IntegrationParams → Bool
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_down : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑(ULift.down ⁻¹' s) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- `TendstoInMeasure` expressed with an extended norm instead of a distance.  -/
MeasureTheory.tendstoInMeasure_iff_enorm : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ENNReal), 0 < ε → ε ≠ ⊤ → Filter.Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖ₑ}) l (nhds 0)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.ref : Lean.Meta.Match.AltLHS → Lean.Syntax
-- Batteries.Data.List.Lemmas
List.diff_sublist : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α), (l₁.diff l₂).Sublist l₁
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The morphism that is part of a costructured arrow.  -/
CategoryTheory.CostructuredArrow.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} → {T : D} → (X : CategoryTheory.CostructuredArrow S T) → S.obj X.left ⟶ T
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSlice_ne_endPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos},
  p ≠ (s.slice p₀ p₁ h).endPos → String.Slice.Pos.ofSlice p ≠ s.endPos
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux'_cons : ∀ {α : Type u_1} (a : α) (l : List α),
  Multiset.powersetAux' (a :: l) = Multiset.powersetAux' l ++ List.map (Multiset.cons a) (Multiset.powersetAux' l)
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelSMul.toIsOrderedSMul : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : SMul G P} [self : IsOrderedCancelSMul G P],
  IsOrderedSMul G P
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- This variation on `List.fold` ensures that the array `keys`
isn't copied unnecessarily.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodeExprWithEta.go.fold : Array Lean.Meta.RefinedDiscrTree.Key →
  List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry) →
    Array (Array Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry) →
      Array (Array Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)
-- Init.Control.Lawful.Instances
StateT.ext : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : StateT σ m α}, (∀ (s : σ), x.run s = y.run s) → x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.mk.sizeOf_spec : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (simplex : Y.obj (Opposite.op { len := d }))
  (nonDegenerate : simplex ∈ Y.nonDegenerate d)
  (notMem : simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))),
  sizeOf { simplex := simplex, nonDegenerate := nonDegenerate, notMem := notMem } = 1 + sizeOf simplex
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by some of the matrices in `listTransvecCol M` does not change the last row.  -/
Matrix.Pivot.listTransvecCol_mul_last_row_drop : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ},
  k ≤ r → ((List.drop k (Matrix.Pivot.listTransvecCol M)).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
-- Mathlib.Order.Filter.Basic
Filter.iSup_principal : ∀ {α : Type u} {ι : Sort w} {s : ι → Set α}, ⨆ x, Filter.principal (s x) = Filter.principal (⋃ i, s i)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ico_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ico a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ico a b, f i.castSucc
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.exists_card_eq : ∀ {α : Type u_1} [inst : BooleanAlgebra α] [Nontrivial α] [inst_2 : Fintype α] {s : Finset α},
  (↑s).Intersecting → ∃ t, s ⊆ t ∧ 2 * t.card = Fintype.card α ∧ (↑t).Intersecting
-- Aesop.Script.Main
_private.Aesop.Script.Main.0.Aesop.Script.UScript.optimize.structureDynamic : Aesop.Script.UScript →
  Bool → Lean.Meta.SavedState → Lean.MVarId → Lean.MetaM (Option (Aesop.Script.SScript × Aesop.ScriptGenerated))
-- Mathlib.Data.Nat.Choose.Multinomial
Finset.symInsertEquiv.congr_simp : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α] {n : ℕ} (h : a ∉ s),
  Finset.symInsertEquiv h = Finset.symInsertEquiv h
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_inf : ∀ {M : Type u_1} [inst : AddMonoid M] (S T : AddSubgroup (AddUnits M)), (S ⊔ T).ofAddUnits = S.ofAddUnits ⊔ T.ofAddUnits
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.refl_apply : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (x : M), (FirstOrder.Language.Equiv.refl L M) x = x
-- Mathlib.CategoryTheory.Galois.EssSurj
CategoryTheory.SingleObj.natTrans.congr_simp : ∀ {M : Type u} [inst : Monoid M] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C]
  {F G : CategoryTheory.Functor (CategoryTheory.SingleObj M) C}
  (u u_1 : F.obj (CategoryTheory.SingleObj.star M) ⟶ G.obj (CategoryTheory.SingleObj.star M)) (e_u : u = u_1)
  (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.map a) u = CategoryTheory.CategoryStruct.comp u (G.map a)),
  CategoryTheory.SingleObj.natTrans u h = CategoryTheory.SingleObj.natTrans u_1 ⋯