mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Ring.List
/-- Product of elements of a list `l` equals zero if and only if `0 ∈ l`. See also
`List.prod_eq_zero` for an implication that needs weaker typeclass assumptions.  -/
List.prod_eq_zero_iff : ∀ {M₀ : Type u_4} [inst : MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {l : List M₀}, l.prod = 0 ↔ 0 ∈ l
-- Mathlib.Algebra.Lie.Matrix
Matrix.lieConj.eq_1 : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P : Matrix n n R)
  (h : Invertible P), P.lieConj h = (lieEquivMatrix'.symm.trans (P.toLinearEquiv' h).lieConj).trans lieEquivMatrix'
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → ContinuousOn f s
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instLeftCancelSemigroup : {α : Type u_1} → [RightCancelSemigroup α] → LeftCancelSemigroup αᵐᵒᵖ
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k k' : α},
  (k == k') = true → m.get? k = m.get? k'
-- Mathlib.Topology.Specialization
Specialization.instPreorder : {α : Type u_1} → [TopologicalSpace α] → Preorder (Specialization α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) (p q n : ℤ) (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleMk 0 h = 0
-- Mathlib.Order.CompleteLattice.Basic
sInf_singleton : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {a : α}, sInf {a} = a
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toRingEquiv_toRingHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑e.toRingEquiv = ↑e
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Lean.Parser.Term
Lean.Parser.Term.ensureExpectedType.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Submonoid.Membership
FreeAddMonoid.closure_range_of : ∀ {α : Type u_4}, AddSubmonoid.closure (Set.range FreeAddMonoid.of) = ⊤
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toLinearMap₂'Aux_toMatrix₂Aux : ∀ (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : Semiring R₁] [inst_2 : Semiring S₁] [inst_3 : Semiring R₂]
  [inst_4 : Semiring S₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Module S₁ N₂]
  [inst_8 : Module S₂ N₂] [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂]
  [inst_11 : SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} [inst_12 : Fintype n] [inst_13 : Fintype m]
  [inst_14 : DecidableEq n] [inst_15 : DecidableEq m] (f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂),
  Matrix.toLinearMap₂'Aux σ₁ σ₂ ((LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) f) = f
-- Mathlib.Dynamics.Minimal
IsCompact.exists_finite_cover_smul : ∀ (G : Type u_2) {α : Type u_3} [inst : Group G] [inst_1 : TopologicalSpace α] [inst_2 : MulAction G α]
  [MulAction.IsMinimal G α] [ContinuousConstSMul G α] {K U : Set α},
  IsCompact K → IsOpen U → U.Nonempty → ∃ I, K ⊆ ⋃ g ∈ I, g • U
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.equivalenceOfReindexing_functor : ∀ {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}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α).functor =
    (CategoryTheory.Limits.Cocone.whiskering e.functor).comp (CategoryTheory.Limits.Cocone.precompose α.inv)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.SigmaFinite.withDensity_of_ne_top' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal},
  (∀ (x : α), f x ≠ ⊤) → MeasureTheory.SigmaFinite (μ.withDensity f)
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabRunElab.unsafe_6 : Lean.TSyntax `term → Lean.Elab.TermElabM (Lean.Elab.TermElabM Lean.Expr)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.eq_empty_of_insertMany_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} {ρ : Type v} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.insertMany l = ∅ → m = ∅
-- Std.Do.Internal.Ensures.Def
Std.Do.Internal.IsAttach.mk : ∀ {m : Type u → Type v} [inst : Bind m] {attach : ⦃α : Type u⦄ → (x : m α) → m { a // Std.Do.Internal.MayReturn x a }},
  (∀ {α : Type u} (x : m α), Std.Do.Internal.ErasesTo (attach x) x) → Std.Do.Internal.IsAttach attach
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_edgeSet : ∀ {V : Type u_1} (G G' : SimpleGraph V), G.deleteEdges G'.edgeSet = G \ G'
-- Init.Data.Fin.Lemmas
Fin.reverseInduction.go.eq_1 : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1))
  (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x : motive ⟨j, h⟩),
  Fin.reverseInduction.go cast i j h h2 x =
    if hi : ↑i = j then _root_.cast ⋯ x
    else
      match j, h, h2, x, hi with
      | 0, h, h2, x, hi => ⋯.elim
      | j.succ, h, h2, x, hi => Fin.reverseInduction.go cast i j ⋯ ⋯ (cast ⟨j, ⋯⟩ x)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- the `AddHom` from an additive subsemigroup to its image. See
`AddEquiv.addSubsemigroupMap` for a variant for `AddEquiv`s.  -/
AddHom.subsemigroupMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → (M' : AddSubsemigroup M) → ↥M' →ₙ+ ↥(AddSubsemigroup.map f M')
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_trans_self : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  e.symm.trans e = MeasurableEquiv.refl β
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < 2 ^ 32), { toBitVec := n#'hn } = UInt32.ofNatLT n hn
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_fun_neg : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : E → 𝕜},
  Function.HasTemperateGrowth g → (SchwartzMap.smulLeftCLM F fun x => -g x) = -SchwartzMap.smulLeftCLM F g
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_nonneg : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 ≤ a % b
-- Mathlib.Algebra.Free
FreeAddSemigroup.length.eq_1 : ∀ {α : Type u} (x : FreeAddSemigroup α), x.length = x.tail.length + 1
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The Hom bifunctor sending a type `X` and a commutative monoid `M` to the commutative monoid
`X → M` with pointwise operations.

This is also the coyoneda embedding of `Type` into `CommMonCat`-valued presheaves of commutative
monoids.  -/
CommMonCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor CommMonCat CommMonCat)
-- Mathlib.Data.PFunctor.Univariate.M
/-- Each approximation agrees with the next  -/
PFunctor.MIntl.consistent : ∀ {F : PFunctor.{uA, uB}} (self : F.MIntl), PFunctor.Approx.AllAgree self.approx
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty_erase!_and_not_containsKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ (k : α), t.isEmpty = ((Std.DTreeMap.Internal.Impl.erase! k t).isEmpty && !Std.DTreeMap.Internal.Impl.contains k t)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.exists_effectiveEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))},
  (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
    ∀ (n : ℕ) (X : C) (y : (F.obj (Opposite.op n)).obj.obj (Opposite.op X)),
      ∃ X' φ,
        ∃ (_ : CategoryTheory.EffectiveEpi φ),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app (Opposite.op X'))) x =
              (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op n)).obj.map φ.op)) y
-- Mathlib.NumberTheory.PythagoreanTriples
/-- A primitive Pythagorean triple `x, y, z` is a Pythagorean triple with `x` and `y` coprime.
Such a triple is “primitively classified” if there exist coprime integers `m, n` such that either
* `x = m ^ 2 - n ^ 2` and `y = 2 * m * n`, or
* `x = 2 * m * n` and `y = m ^ 2 - n ^ 2`.
 -/
PythagoreanTriple.IsPrimitiveClassified : {x y z : ℤ} → PythagoreanTriple x y z → Prop
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.whiskerRight_def : ∀ {R : Type u} [inst : CommRing R] {X₁ X₂ : ModuleCat R} (f : X₁ ⟶ X₂) (M : ModuleCat R),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f M =
    ModuleCat.ofHom (LinearMap.rTensor (↑M) (ModuleCat.Hom.hom f))
-- Mathlib.Algebra.Group.Prod
MulHom.prod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N × P),
  ((MulHom.fst N P).comp f).prod ((MulHom.snd N P).comp f) = f
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Minute.Ordinal n
-- Mathlib.CategoryTheory.EssentialImage
/-- If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as
`F ≅ F'`.
 -/
CategoryTheory.Functor.essImage.ofNatIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (h : F ≅ F') {Y : D}, F.essImage Y → F'.essImage Y
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_eq_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {f : α →₀ ℕ},
  Multiset.toFinsupp s = f ↔ s = Finsupp.toMultiset f
-- Mathlib.CategoryTheory.GradedObject
/-- The tautological cofan corresponding to the coproduct decomposition of `X.mapObj p j`.  -/
CategoryTheory.GradedObject.cofanMapObj : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) → (p : I → J) → [X.HasMap p] → (j : J) → X.CofanMapObjFun p j
-- Mathlib.Data.Set.Card
Set.ncard_eq_of_bijective : ∀ {α : Type u_1} {s : Set α} {n : ℕ} (f : (i : ℕ) → i < n → α),
  (∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a) →
    (∀ (i : ℕ) (h : i < n), f i h ∈ s) → (∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) → s.ncard = n
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.Limits.colim.mapShortComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
  {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone S.X₂) (c₃ : CategoryTheory.Limits.Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt)
  (g : c₂.pt ⟶ c₃.pt)
  (hf :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
  (hg :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g = CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
  (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).f = f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Dense.exists_dist_lt : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Dense s → ∀ (x : α) {ε : ℝ}, 0 < ε → ∃ y ∈ s, dist x y < ε
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s : NonemptyInterval α), (-s).length = s.length
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.Simps.findAutomaticProjectionsAux.unsafe_1 : Lean.Name → Lean.Elab.TermElabM Simps.findArgType
-- Mathlib.Data.FinEnum
/-- A type with unique inhabitant has a trivial enumeration. Not registered as an instance, to make
sure that there aren't two definitionally differing instances around.  -/
FinEnum.ofUnique : {α : Type u} → [Unique α] → FinEnum α
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond.eq_3 : ∀ (n : ℕ), n.succ.stirlingSecond 0 = 0
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instMembership : {α : Type u_1} → [inst : MeasurableSpace α] → Membership α (Subtype MeasurableSet)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ : ∀ (x y i : ℕ) (c : Bool), x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ (i + 1)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.empty : {α : Type u_1} → Std.Sat.CNF α
-- Aesop.Stats.Basic
Aesop.modifyStatsIfEnabled : {m : Type → Type} → [Monad m] → [Aesop.MonadStats m] → (Aesop.Stats → Aesop.Stats) → m Unit
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSetCardinalLT : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular] (X : Type u),
  CategoryTheory.IsCardinalFiltered (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ X) κ
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setSimpTheorems : Lean.Meta.Simp.Context → Lean.Meta.SimpTheoremsArray → Lean.Meta.Simp.Context
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodAddEquiv.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H)
  [inst_2 : A.Normal] [inst_3 : B.Normal],
  QuotientAddGroup.prodAddEquiv A B = { toEquiv := QuotientAddGroup.prodEquiv A B, map_add' := ⋯ }
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift an injective algebra homomorphism `K[X] →ₐ[S] L` to a `K⟮X⟯ →ₐ[S] L`
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.liftAlgHom : {K : Type u} →
  [inst : CommRing K] →
    [inst_1 : IsDomain K] →
      {L : Type u_1} →
        {S : Type u_3} →
          [inst_2 : Field L] →
            [inst_3 : CommSemiring S] →
              [inst_4 : Algebra S (Polynomial K)] →
                [inst_5 : Algebra S L] →
                  (φ : Polynomial K →ₐ[S] L) →
                    nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L) → RatFunc K →ₐ[S] L
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.smul : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → {α : Type u_3} → [SMul α Y] → SMul α (LocallyConstant X Y)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulLeftStrictMono.toPosMulReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulLeftReflectLE α], PosMulReflectLE α
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  {unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g}
  {counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b}
  {left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam}
  {right_triangle :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit counit =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam}
  {unit_1 : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g}
  {counit_1 : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b}
  {left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
          (CategoryTheory.Bicategory.rightUnitor f).inv)
      CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam}
  {right_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.rightZigzag unit_1 counit_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
          (CategoryTheory.Bicategory.leftUnitor g).inv)
      CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam},
  { unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
      { unit := unit_1, counit := counit_1, left_triangle := left_triangle_1, right_triangle := right_triangle_1 } →
    unit = unit_1 ∧ counit = counit_1
-- Mathlib.Analysis.Normed.Module.Ray
/-- Two vectors `x y` in a real normed space are on the ray if and only if one of them is zero or
the unit vectors `‖x‖⁻¹ • x` and `‖y‖⁻¹ • y` are equal.  -/
sameRay_iff_inv_norm_smul_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
  SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq_startPos_iff : ∀ {t₁ t₂ s : String} {p : s.Pos}, p.Splits t₁ t₂ → (p = s.startPos ↔ t₁ = "")
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Multiset.Ici a ↔ a ≤ x
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.mk.inj : ∀ {R : Type u_2} {inst : NonUnitalNonAssocRing R} {toAddGroupSeminorm : AddGroupSeminorm R}
  {mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y}
  {toAddGroupSeminorm_1 : AddGroupSeminorm R}
  {mul_le'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y},
  { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 } →
    toAddGroupSeminorm = toAddGroupSeminorm_1
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.truncation.eq_1 : ∀ {α : Type u_1} (f : α → ℝ) (A : ℝ), ProbabilityTheory.truncation f A = (Set.Ioc (-A) A).indicator id ∘ f
-- Mathlib.Algebra.Module.Defs
Module.toDistribMulAction : {R : Type u} →
  {M : Type v} → {inst : Semiring R} → {inst_1 : AddCommMonoid M} → [self : Module R M] → DistribMulAction R M
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isHomeomorph_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U →
    Continuous f → (IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f))
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (b : CategoryTheory.LocallyDiscrete Cᵒᵖ)
  {X Y Z :
    CategoryTheory.ObjectProperty.FullSubcategory (CategoryTheory.Presheaf.IsSheaf (J.over (Opposite.unop b.as)))}
  (a : X ⟶ Y) (a_1 : Y ⟶ Z) (X_1 : (CategoryTheory.Over (Opposite.unop b.as))ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp a a_1).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (a.hom.app X_1) (a_1.hom.app X_1)
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallySeparatedSpace.mk : ∀ {α : Type u} [inst : TopologicalSpace α], IsTotallySeparated Set.univ → TotallySeparatedSpace α
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_ennreal_smul_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (c : ENNReal),
  (c • μ).real s = c.toReal * μ.real s
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.succStruct_prop_le_propArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ],
  (CategoryTheory.SmallObject.succStruct I κ).prop ≤
    (CategoryTheory.SmallObject.propArrow I).functorCategory (CategoryTheory.Arrow C)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.cons_cons_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool},
  FreeAddGroup.Red.Step (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red.Step L₁ L₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertList_of_contains_left_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l toInsert : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getKey! k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey! k toInsert
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso C =
    CategoryTheory.NatIso.ofComponents
      (fun F => CategoryTheory.LaxMonoidalFunctor.isoOfComponents (fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) ⋯ ⋯ ⋯)
      ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_mul_inv_iff₀` for a version with multiplication on the other side.  -/
le_mul_inv_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ b * c⁻¹ ↔ c * a ≤ b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
summable_cotTerm : ∀ {x : ℂ}, x ∈ Complex.integerComplement → Summable fun n => cotTerm x n
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] {Z : D} (h : G.obj (CategoryTheory.Limits.cokernel f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (G.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.π f)) h
-- Init.Data.List.Lemmas
List.head?_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, (List.replicate n a).head? = if n = 0 then none else some a
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁) (a : R),
  (MvPolynomial.map f) (MvPolynomial.C a) = MvPolynomial.C (f a)