mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Defs
/-- Build a new metric space from an old one where the bundled uniform structure is provably
(but typically non-definitionaly) equal to some given uniform structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
MetricSpace.replaceUniformity : {γ : Type u_3} → [U : UniformSpace γ] → (m : MetricSpace γ) → uniformity γ = uniformity γ → MetricSpace γ
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default : Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_eq_coe : ∀ {α : Type u} [inst : One α] {a : α}, 1 = ↑a ↔ a = 1
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] (m n : ℕ),
  Polynomial.degreeLT.addLinearEquiv R m n =
    (Polynomial.degreeLT.basis R (m + n)).equiv (Polynomial.degreeLT.basisProd R m n) (Equiv.refl (Fin (m + n)))
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCustomInfo.inj : ∀ {i i_1 : Lean.Elab.CustomInfo}, Lean.Elab.Info.ofCustomInfo i = Lean.Elab.Info.ofCustomInfo i_1 → i = i_1
-- Mathlib.Topology.Path
Path.cast_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a₁ a₂ b₁ b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂),
  γ.symm.cast hb ha = (γ.cast ha hb).symm
-- Mathlib.Order.RelIso.Basic
RelEmbedding.toEmbedding_inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ↪r s},
  f.toEmbedding = g.toEmbedding ↔ f = g
-- Mathlib.Data.Set.Image
Function.LeftInverse.image_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.LeftInverse g f → ∀ (s : Set α), f '' s = Set.range f ∩ g ⁻¹' s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
tendsto_measure_Icc_nhdsWithin_right : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (b : ℝ),
  Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (nhdsWithin 0 (Set.Ici 0)) (nhds (μ {b}))
-- Mathlib.Data.Finset.Sum
Finset.map_inl_subset_iff_subset_toLeft : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)},
  Finset.map Function.Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft
-- Mathlib.Analysis.Normed.Group.InfiniteSum
cauchySeq_finset_of_norm_bounded_eventually : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ},
  Summable g → (∀ᶠ (i : ι) in Filter.cofinite, ‖f i‖ ≤ g i) → CauchySeq fun s => ∑ i ∈ s, f i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  m.WF → ((Std.DHashMap.Raw.filterMap f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), (f k (m.get k h)).isSome = true)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.revAll_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.copy.revAll pat = s.revAll pat
-- Mathlib.Order.Max
noTopOrder_iff' : ∀ (α : Type u_3) [inst : LE α], NoTopOrder α ↔ ∀ (a : α), ∃ b, ¬b ≤ a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonColor.fromJson : Lean.Json → Except String Lean.Lsp.Color
-- Mathlib.Data.PNat.Factors
PNat.factorMultiset_le_iff' : ∀ {m : ℕ+} {v : PrimeMultiset}, m.factorMultiset ≤ v ↔ m ∣ v.prod
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.id : Lean.Meta.Grind.Arith.CommRing.EqCnstr → ℕ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {E F : J.OneHypercover S} (f : E.toPreOneHypercover ≅ F.toPreOneHypercover),
  (CategoryTheory.GrothendieckTopology.OneHypercover.isoMk f).hom = f.hom
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_add_succ_right_eq_append' : ∀ {m n : ℕ}, (m...m + (n + 1)).toList = (m...m + n).toList ++ [m + n]
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.toLaxBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} → [self : F.Braided] → F.LaxBraided
-- Std.Http.Data.Body.Stream
/-- Abstracts over how the next chunk is received, allowing `readAll` to work in both `Async`
(no cancellation) and `ContextAsync` (races with cancellation via `doneSelector`).
 -/
Std.Http.Body.Stream.NextChunk : (Type → Type) → Type
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isLUB_inv' : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.neg_comp_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg =
    CategoryTheory.CategoryStruct.id A
-- Mathlib.Algebra.Polynomial.Laurent
/-- The degree of a Laurent polynomial takes values in `WithBot ℤ`.
If `f : R[T;T⁻¹]` is a Laurent polynomial, then `f.degree` is the maximum of its support of `f`,
or `⊥`, if `f = 0`.  -/
LaurentPolynomial.degree : {R : Type u_1} → [inst : Semiring R] → LaurentPolynomial R → WithBot ℤ
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ),
  ((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).obj X).obj.obj X_1 =
    ULift.{w, v} (Opposite.unop X_1 ⟶ X)
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → Topology.IsEmbedding f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionItem : Lean.ToJson Lean.Lsp.CompletionItem
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).IsRootSystem
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getElem?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁[k]? = t₂[k]?
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- A simplicial set is preconnected when it has at most one connected component.  -/
SSet.IsPreconnected : SSet → Prop
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_iff_not_exists_st : ∀ {x : ℝ*}, x.Infinite ↔ ¬∃ r, x.IsSt r
-- Plausible.Testable
/-- Run a test suite for `p` and throw an exception if `p` does not hold.  -/
Plausible.Testable.check : (p : Prop) →
  optParam Plausible.Configuration { } →
    (p' : autoParam (Plausible.Decorations.DecorationsOf p) Plausible.Testable.check._auto_1) →
      [Plausible.Testable p'] → Lean.CoreM PUnit.{1}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.all.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β) (p : (a : α) → β a → Bool),
  t.all p =
    (do
        let __s ←
          forIn t (none, ()) fun x __s =>
              match x with
              | ⟨a, b⟩ =>
                if p a b = false then pure (ForInStep.done (some false, ())) else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure true).run
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotationCoeff.eq_2 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) (n : ℕ),
  WittVector.frobeniusRotationCoeff p ha₁ ha₂ n.succ =
    WittVector.RecursionMain.succNthVal p n a₁ a₂ (fun i => WittVector.frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂
-- Mathlib.Order.UpperLower.Principal
LowerSet.mem_Iio_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ LowerSet.Iio a ↔ b < a
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Note that the identity satisfies `IsCycleOn` for any subsingleton set, but not `IsCycle`.  -/
Equiv.Perm.IsCycleOn.isCycle_subtypePerm : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s), s.Nontrivial → (f.subtypePerm ⋯).IsCycle
-- Lean.PrettyPrinter.Delaborator.Metavariable
/-- String version of `delabMVarAux`, for use in dynamic docstrings.  -/
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.delabMVarAsStr : Lean.MVarId → Lean.MetaM String
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_add_le_add : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I J : LieIdeal R L)
  (k l : ℕ),
  LieAlgebra.derivedSeriesOfIdeal R L (k + l) (I + J) ≤
    LieAlgebra.derivedSeriesOfIdeal R L k I + LieAlgebra.derivedSeriesOfIdeal R L l J
-- Lean.Meta.Closure
Lean.Meta.Closure.State.exprFVarArgs : Lean.Meta.Closure.State → Array Lean.Expr
-- Mathlib.Data.Opposite
Opposite.equivToOpposite_coe : ∀ {α : Sort u}, ⇑Opposite.equivToOpposite = Opposite.op
-- Mathlib.Data.Set.Basic
Set.inter_right_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
-- Aesop.Tree.Data
/-- A refinement of the `NodeState`, distinguishing between goals proven during
normalisation and goals proven by a child rule application.
 -/
Aesop.GoalState : Type
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.eventually_exists_mem_iff : ∀ {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {P : β → α → Prop},
  is.Finite → ((∀ᶠ (i : α) in ↑f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in ↑f, P a i)
-- Std.Sync.CancellationContext
Std.CancellationContext.mk : Std.Mutex Std.CancellationContext.State → Std.CancellationToken → UInt64 → Std.CancellationContext
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β}, Std.ExtDTreeMap.Const.getD t a fallback = t.getD a fallback
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.conjAct_smul_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ spinGroup Q → ∀ [Invertible 2], ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.deg_ne_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) [Nontrivial S], f.natDegree ≠ 0
-- Mathlib.Topology.Algebra.FilterBasis
/-- An `AddGroupFilterBasis` on an additive group is a `FilterBasis` satisfying some additional
axioms. Example : if `G` is a topological group then the neighbourhoods of the identity are an
`AddGroupFilterBasis`. Conversely given an `AddGroupFilterBasis` one can define a topology
compatible with the group structure on `G`.  -/
AddGroupFilterBasis : (A : Type u) → [AddGroup A] → Type u
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- `weightedHomogeneousComponent w n φ` is the part of `φ` that is weighted homogeneous of
weighted degree `n`, with respect to the weights `w`.
See `sum_weightedHomogeneousComponent` for the statement that `φ` is equal to the sum
of all its weighted homogeneous components.  -/
MvPolynomial.weightedHomogeneousComponent : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → {σ : Type u_3} → [AddCommMonoid M] → (σ → M) → M → MvPolynomial σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.Order.Interval.Multiset
Multiset.Ico.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), Multiset.Ico a b = (Finset.Ico a b).val
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (a : PrimeSpectrum S),
  ↑(↑((IsLocalization.primeSpectrumOrderIso M S) a)).asIdeal = ⇑(algebraMap R S) ⁻¹' ↑a.asIdeal
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_mul_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), a⁻ᵐ * a⁺ᵐ = |a|ₘ
-- Mathlib.Analysis.ConstantSpeed
HasConstantSpeedOnWith.hasLocallyBoundedVariationOn : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal},
  HasConstantSpeedOnWith f s l → LocallyBoundedVariationOn f s
-- ProofWidgets.Presentation.Expr
ProofWidgets.instRpcEncodableExprPresentationData : Lean.Server.RpcEncodable ProofWidgets.ExprPresentationData
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
  [CompleteSpace α], Summable f → ∀ (p : β → Prop), Summable (f ∘ Subtype.val)
-- Mathlib.Topology.Constructions
isOpenMap_ofAdd : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑Multiplicative.ofAdd
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.AC.EqCnstr → Sort u} {motive_2 : Lean.Meta.Grind.AC.EqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.AC.EqCnstr) (F_1 : (t : Lean.Meta.Grind.AC.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.AC.EqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.AC.EqCnstr.brecOn.go t F_1 F_2).2
-- Lean.Elab.DefView
Lean.Elab.DefKind.instance.sizeOf_spec : sizeOf Lean.Elab.DefKind.instance = 1
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_slice_eq_false_iff : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zeroLEOneClass : ∀ {α : Type u} [inst : One α] [inst_1 : Zero α] [inst_2 : LE α] [ZeroLEOneClass α], ZeroLEOneClass (WithBot α)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithTop α}, a ≠ 0 → a * ⊤ = ⊤
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app b) ≅ CategoryTheory.CategoryStruct.comp (app a) (G.map f))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
            (naturality g).hom =
          CategoryTheory.CategoryStruct.comp (naturality f).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
      CategoryTheory.Oplax.StrongTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a)).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
              (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
      CategoryTheory.Oplax.StrongTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g)).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
      CategoryTheory.Oplax.StrongTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Mathlib.CategoryTheory.Generator.StrongGenerator
/-- A property `P : ObjectProperty C` is a strong generator
if it is separating and for any proper subobject `A ⊂ X`, there exists
a morphism `G ⟶ X` which does not factor through `A` from an object
such that `P G` holds.  -/
CategoryTheory.ObjectProperty.IsStrongGenerator : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.logCounting.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E],
  Function.locallyFinsuppWithin.logCounting = Function.locallyFinsuppWithin.logCounting
-- Mathlib.Analysis.Normed.Group.Basic
IndiscreteTopology.norm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] [IndiscreteTopology E] (x : E), ‖x‖ = 0
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Metric.diam_closure : ∀ {α : Type u_4} [inst : PseudoMetricSpace α] (s : Set α), Metric.diam (closure s) = Metric.diam s
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_inf : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x \ y ⊓ (x ⊓ y) = ⊥
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_re_ge : ∀ (r : ℝ), Convex ℝ {c | r ≤ c.re}
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_iff_mul_rearrangement`.

---

Two functions antivary iff the rearrangement inequality holds.  -/
AntivaryOn.mul_add_mul_le_mul_add_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
-- Mathlib.Data.Multiset.ZeroCons
Multiset.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ {a}
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseOffsetX : (Std.Time.OffsetX → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_of_degree_lt_right : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).eraseLead = p + q.eraseLead
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM : Type → Type
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.ae_withDensity_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal},
  Measurable f → ((∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x)
-- Mathlib.MeasureTheory.Measure.Content
/-- For the outer measure coming from a content, all Borel sets are measurable.  -/
MeasureTheory.Content.borel_le_caratheodory : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G]
  [BorelSpace G], S ≤ μ.outerMeasure.caratheodory
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid have a representation of the base value in
the `AddMonoid`.  -/
AddUnits.instRepr : {α : Type u} → [inst : AddMonoid α] → [Repr α] → Repr (AddUnits α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_obj : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) (i : SimplexCategoryᵒᵖ),
  (A.image f).obj i = ⇑(CategoryTheory.ConcreteCategory.hom (f.app i)) '' A.obj i
-- Mathlib.ModelTheory.Definability
/-- Constant functions are `TermDefinable`, assuming the constant value is a language constant.  -/
Set.TermDefinable.const : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁}
  (C : (L.withConstants ↑A).Constants), A.TermDefinable L (Function.const (α → M) ↑C)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.abs_arg_le_pi : ∀ (z : ℂ), |z.arg| ≤ Real.pi
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : AddMonoid Y]
  [inst_3 : ContinuousAdd Y],
  LocallyConstant.toContinuousMapAddMonoidHom =
    { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` is even.  -/
Real.posLog_neg : ∀ (x : ℝ), (-x).posLog = x.posLog
-- Mathlib.Algebra.Order.AddGroupWithTop
add_le_add_iff_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F]
  (x_1 : carrier (X.presheaf.obj (Opposite.op (h.functor.obj V)))),
  (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv)
      ((CategoryTheory.ConcreteCategory.hom
          (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) x_1
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.orderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [inst_1 : (i : ι) → AddCommMonoid (α i)] →
        [inst_2 : (i : ι) → PartialOrder (α i)] → [∀ (i : ι), IsBotZeroClass (α i)] → OrderBot (Lex (Π₀ (i : ι), α i))