mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn.go : {α : Type u} →
  {β : Type v} →
    {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1} →
      {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
        {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
          {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1} →
            (t : Lean.PersistentHashMap.Node α β) →
              ((t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t) →
                ((t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                    Lean.PersistentHashMap.Node.below_1 t → motive_2 t) →
                  ((t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                      Lean.PersistentHashMap.Node.below_2 t → motive_3 t) →
                    ((t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
                        Lean.PersistentHashMap.Node.below_3 t → motive_4 t) →
                      motive_1 t ×' t.below
-- Mathlib.NumberTheory.Real.Irrational
irrational_mul_intCast_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x
-- Mathlib.Analysis.Normed.Group.Basic
norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), ‖a⁻¹ * b‖ = ‖a / b‖
-- Mathlib.Data.Set.Card
Set.Finite.exists_injOn_of_encard_le : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set α} {t : Set β},
  s.Finite → s.encard ≤ t.encard → ∃ f, s ⊆ f ⁻¹' t ∧ Set.InjOn f s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
  MeasureTheory.Integrable f MeasureTheory.volume → HasSum (fun n => ∫ (x : ℝ) in 0..1, f (x + ↑n)) (∫ (x : ℝ), f x)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c : C) {d d' : D}
  (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_neg_eq_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, (fun x => -x) '' s = -s
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.coe_torsion' : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  ↑(Submodule.torsion' R M S) = {x | ∃ a, a • x = 0}
-- Lean.Meta.Tactic.Simp.Types
/-- Number of times each simp theorem has been tried.  -/
Lean.Meta.Simp.Diagnostics.triedThmCounter : Lean.Meta.Simp.Diagnostics → Lean.PHashMap Lean.Meta.Origin ℕ
-- Mathlib.Topology.Order.DenselyOrdered
Ioc_mem_nhds_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a b x : α}, Set.Ioc a b ∈ nhds x ↔ x ∈ Set.Ioo a b
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_target : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)],
  (e₁.prod e₂).target = (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- Any closed ball `Metric.closedBall x r`, `0 ≤ r` is the image of the unit closed ball under
`fun y ↦ x + r • y`.  -/
affinity_unitClosedBall : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 ≤ r → ∀ (x : E), x +ᵥ r • Metric.closedBall 0 1 = Metric.closedBall x r
-- Mathlib.Data.PFun
PFun.dom_toSubtype_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : α → β} {a : α}, (PFun.toSubtype p f a).Dom ↔ p (f a)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyData.map_homologyMap' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  [inst_5 : h₁.left.IsPreservedBy F] [inst_6 : h₁.right.IsPreservedBy F] [inst_7 : h₂.left.IsPreservedBy F]
  [inst_8 : h₂.right.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂) =
    CategoryTheory.ShortComplex.homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.fold_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  m.WF → Std.DHashMap.Raw.fold f init m = Array.foldl (fun a b => f a b.fst b.snd) init m.toArray
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), t.contains a = false)
-- Mathlib.Data.List.Lattice
List.inter_eq_nil_iff_disjoint : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- In a category, given a morphism `f : A ⟶ B` and an object `X`,
this is the obvious pushout diagram:
```
A ⟶ A ⨿ X
|     |
v     v
B ⟶ B ⨿ X
```
 -/
CategoryTheory.IsPushout.of_coprod_inl_with_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) (X : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct B X],
  CategoryTheory.IsPushout CategoryTheory.Limits.coprod.inl f
    (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id X)) CategoryTheory.Limits.coprod.inl
-- Lean.Data.PersistentArray
Lean.PersistentArray.instForInOfMonad : {α : Type u} → {m : Type v → Type w} → [Monad m] → ForIn m (Lean.PersistentArray α) α
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux_perm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → (Multiset.powersetAux l₁).Perm (Multiset.powersetAux l₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff! m₂) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_prodMap : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [inst : CommRing R]
  [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂]
  [inst_5 : LieRing L₃] [inst_6 : LieAlgebra R L₃] [inst_7 : LieRing L₄] [inst_8 : LieAlgebra R L₄] (f : L₁ →ₗ⁅R⁆ L₃)
  (g : L₂ →ₗ⁅R⁆ L₄), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Tactic.Basic
Mathlib.Tactic.withResetServerInfo.Result.mk : {α : Type} →
  Option α → Lean.MessageLog → Lean.PersistentArray Lean.Elab.InfoTree → Mathlib.Tactic.withResetServerInfo.Result α
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendLeft.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition n),
  c.extendLeft =
    { length := c.length + 1, partSize := Fin.cons 1 c.partSize, partSize_pos := ⋯,
      emb := fun i =>
        Fin.cases (motive := fun x => Fin (Fin.cons 1 c.partSize x) → Fin (n + 1)) (fun x => 0)
          (fun m => Fin.succ ∘ c.emb m) i,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The set of infinite places of `L` that are unramified over a given infinite place of `K`.  -/
NumberField.InfinitePlace.unramifiedPlacesOver : {K : Type u_4} →
  (L : Type u_5) →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace K → Set (NumberField.InfinitePlace L)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_mono_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (s : Set α),
  f ≤ᵐ[μ] g → ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ
-- Mathlib.Algebra.Group.Basic
add_eq_zero_iff_neg_eq' : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ -b = a
-- Mathlib.Analysis.Normed.Group.Basic
exists_nnnorm_ne_zero' : ∀ (E : Type u_5) [inst : SeminormedGroup E] [NontrivialTopology E], ∃ x, ‖x‖₊ ≠ 0
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.comma.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.comma✝ = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.instIsSemitopologicalRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Star A] [IsSemitopologicalRing A] (s : NonUnitalStarSubalgebra R A),
  IsSemitopologicalRing ↥s
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}, (m.bind fun x => ν) = m Set.univ • ν
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- The kernel of `g y` gives a family of subobjects of `X` indexed by `Under j₀`, and
we consider it as a functor `Under j₀ ⥤ MonoOver X`.  -/
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] →
      {X : C} →
        {J : Type w} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            {Y : CategoryTheory.Functor J C} →
              {j₀ : J} → (X ⟶ Y.obj j₀) → CategoryTheory.Functor (CategoryTheory.Under j₀) (CategoryTheory.MonoOver X)
-- Batteries.Data.List.Count
List.surjective_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : List α}, Function.Surjective xs.idxToSigmaCount
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagram_obj : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (a : CategoryTheory.Pairwise ι),
  (CategoryTheory.Pairwise.diagram U).obj a = CategoryTheory.Pairwise.diagramObj U a
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₁_of_right : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Finite α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {left : Std.IterM m β₁}
  {b b' : Option { out // ∃ it, it.IsPlausibleOutput out }} {it' it : Std.IterM m β₂},
  b' = b →
    it'.finitelyManySkips.Rel it.finitelyManySkips →
      Std.Iterators.Types.Zip.Rel₁ m { internalState := { left := left, memoizedLeft := b', right := it' } }
        { internalState := { left := left, memoizedLeft := b, right := it } }
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `n`-th homology of the alternating constant complex is zero for non-zero even `n`.  -/
ChainComplex.alternatingConstHomologyDataEvenNEZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] →
        (X : C) →
          (n : ℕ) → Even n → n ≠ 0 → (HomologicalComplex.sc (ChainComplex.alternatingConst.obj X) n).HomologyData
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.card_biUnion_offDiag_le' : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A},
  P.IsEquipartition → ↑(P.parts.biUnion Finset.offDiag).card ≤ ↑A.card * (↑A.card + ↑P.parts.card) / ↑P.parts.card
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
groupCohomology.Hilbert90.aux_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] (f : Gal(L/K) → Lˣ), groupCohomology.Hilbert90.aux f ≠ 0
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.isRightAdjoint_comp_iff_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence], (F.comp G).IsRightAdjoint ↔ G.IsRightAdjoint
-- Mathlib.Data.Set.Basic
Set.not_notMem : ∀ {α : Type u} {a : α} {s : Set α}, ¬a ∉ s ↔ a ∈ s
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.GrindM.runAtGoal : {α : Type} →
  Lean.MVarId →
    Lean.Meta.Grind.Params →
      (Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM α) →
        optParam (Option Lean.Meta.Grind.EvalTactic) none → Lean.MetaM α
-- Mathlib.Computability.Primrec.Basic
Primrec.sumInl : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Sum.inl
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.isSome = !t.isEmpty
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.instHasPropTrue : ∀ (X : Type u_1) [inst : TopologicalSpace X], CompHausLike.HasProp (fun x => True) X
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.isPiSystem_squareCylinders : ∀ {ι : Type u_2} {α : ι → Type u_1} {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), IsPiSystem (C i)) → (∀ (i : ι), Set.univ ∈ C i) → IsPiSystem (MeasureTheory.squareCylinders C)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring homomorphism `f` from `M` to `P` whose kernel contains `c`,
the lift of `M` to `P` is injective iff `ker f = c`.  -/
RingCon.lift_injective_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  {h : c ≤ RingCon.ker f}, Function.Injective ⇑(c.lift f h) ↔ c = RingCon.ker f
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.mul : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} →
      CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.assocIsometry_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)),
  (TensorProduct.assocIsometry 𝕜 E F G).symm x = (TensorProduct.assoc 𝕜 E F G).symm x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeOp_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.mapCoconeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
-- Mathlib.Algebra.Group.Submonoid.Support
/-- The support of a submonoid `M` of a group `G` is `M ∩ M⁻¹`,
the largest subgroup of `G` contained in `M`.
 -/
Submonoid.mulSupport : {G : Type u_1} → [inst : Group G] → Submonoid G → Subgroup G
-- Init.Data.Sum.Lemmas
Sum.not_isRight : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, ¬x.isRight = true ↔ x.isLeft = true
-- Mathlib.Analysis.Normed.Lp.lpSpace
zero_memℓp : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)], Memℓp 0 p
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : ℝ),
  (r • s).toJordanDecomposition = r • s.toJordanDecomposition
-- Mathlib.CategoryTheory.Types.Basic
/-- A morphism in `Type` is a monomorphism if and only if it is injective.  -/
CategoryTheory.ofHom_mono_iff_injective : ∀ {X Y : Type u} (f : X → Y), CategoryTheory.Mono (TypeCat.ofHom f) ↔ Function.Injective f
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.mul_iff_left : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : CommGroup G]
  [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure α} {f g : α → G},
  AEMeasurable f μ → (AEMeasurable (g * f) μ ↔ AEMeasurable g μ)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.tensorμ_braid_swap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X X Y Y)
      (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ X X).hom (β_ Y Y).hom)
      (CategoryTheory.MonoidalCategory.tensorμ X X Y Y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Lean.Util.LeanOptions
/-- Formats the lean option value as a CLI flag argument.  -/
Lean.LeanOptionValue.asCliFlagValue : Lean.LeanOptionValue → String
-- Mathlib.Logic.Relation
Relation.ReflTransGen.refl : ∀ {α : Type u_1} {r : α → α → Prop} {a : α}, Relation.ReflTransGen r a a
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.instSFiniteMap : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (f : α → β) [MeasureTheory.SFinite μ], MeasureTheory.SFinite (MeasureTheory.Measure.map f μ)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.mk : (toDistLat : DistLat) → [isBoundedOrder : BoundedOrder ↑toDistLat] → BddDistLat
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.FindSplitImpl.visit.visitApp? : Lean.Expr → Lean.Meta.FindSplitImpl.FindM (Option Lean.Expr)
-- Mathlib.Data.Sym.Sym2
Sym2.forall : ∀ {α : Type u_4} {f : Sym2 α → Prop}, (∀ (x : Sym2 α), f x) ↔ ∀ (x y : α), f s(x, y)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualEquivDual_def : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  ↑W.dualEquivDual = W.dualLift.rangeRestrict
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for the `whiskerLeft` operator of monoidal categories  -/
CategoryTheory.MonoidalCategory.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors'.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
  Associates.factors' a = Multiset.pmap (fun a ha => ⟨Associates.mk a, ⋯⟩) (UniqueFactorizationMonoid.factors a) ⋯
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The monad used in `#click_suggestions`.  -/
Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM : Type → Type
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_1.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_2 t ×' Lean.Elab.Term.Do.Code.below_1 t
-- Init.Data.SInt.Lemmas
Int32.toInt_div_of_ne_left : ∀ (a b : Int32), a ≠ Int32.minValue → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
isometry_cfcₙHom : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : MetricSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A)
  (ha : autoParam (p a) isometry_cfcₙHom._auto_1), Isometry ⇑(cfcₙHom ⋯)