mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.normSq_eq_zero_of_eq_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] {x : F}, x = 0 → InnerProductSpace.Core.normSq x = 0
-- Mathlib.Order.PrimeIdeal
Order.Ideal.isPrime_iff_mem_or_compl_mem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {I : Order.Ideal P} [I.IsProper], I.IsPrime ↔ ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
-- Init.Data.Range.Polymorphic.Lemmas
Std.toList_roc_eq_toList_rcc_of_isSome_succ? : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {lo hi : α} (h : (Std.PRange.succ? lo).isSome = true),
  (lo<...=hi).toList = (((Std.PRange.succ? lo).get h)...=hi).toList
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.klFun_eq_zero_iff : ∀ {x : ℝ}, 0 ≤ x → (InformationTheory.klFun x = 0 ↔ x = 1)
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consCollision.inj : ∀ {α : Type u} {β : Type v} {keys : Subarray α} {vals : Subarray β} {a : Std.Slice.size keys = Std.Slice.size vals}
  {a_1 : Lean.PersistentHashMap.Zipper α β} {keys_1 : Subarray α} {vals_1 : Subarray β}
  {a_2 : Std.Slice.size keys_1 = Std.Slice.size vals_1} {a_3 : Lean.PersistentHashMap.Zipper α β},
  Lean.PersistentHashMap.Zipper.consCollision keys vals a a_1 =
      Lean.PersistentHashMap.Zipper.consCollision keys_1 vals_1 a_2 a_3 →
    keys = keys_1 ∧ vals = vals_1 ∧ a_1 = a_3
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a b : α) (xs : List α) (le : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match a :: b :: xs, le with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_3 a b xs le
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent.congr_simp : ∀ {n : Type u_1} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {R : Type u_2}
  [inst_3 : CommSemiring R] (M M_1 : Matrix n n R), M = M_1 → M.permanent = M_1.permanent
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a congruence relation `c` on a type `M` with a multiplication, the order-preserving
bijection between the set of congruence relations containing `c` and the congruence relations
on the quotient of `M` by `c`.  -/
Con.correspondence : {M : Type u_1} → [inst : Mul M] → {c : Con M} → { d // c ≤ d } ≃o Con c.Quotient
-- Mathlib.Order.Heyting.Basic
/-- A generalized Heyting algebra is a lattice with an additional binary operation `⇨` called
Heyting implication such that `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`.

This generalizes `HeytingAlgebra` by not requiring a bottom element.  -/
GeneralizedHeytingAlgebra : Type u_4 → Type u_4
-- Mathlib.Algebra.Algebra.Operations
/-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
is closed under addition, and holds for `m * x` where `m ∈ M` and it holds for `x`  -/
Submodule.pow_induction_on_left : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  {C : A → Prop},
  (∀ (r : R), C ((algebraMap R A) r)) →
    (∀ (x y : A), C x → C y → C (x + y)) → (∀ m ∈ M, ∀ (x : A), C x → C (m * x)) → ∀ {x : A} {n : ℕ}, x ∈ M ^ n → C x
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The torsion subgroup is finite.  -/
NumberField.Units.instFiniteSubtypeUnitsRingOfIntegersMemSubgroupTorsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Finite ↥(NumberField.Units.torsion K)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- **Alias** of the forward direction of `Set.finite_inv`. -/
Set.Finite.of_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹.Finite → s.Finite
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.preimage_image : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (s : Set P₁), ⇑e ⁻¹' ⇑e '' s = s
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.loop_eq : ∀ {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Path v v), p = SimpleGraph.Path.nil
-- Mathlib.GroupTheory.Torsion
instModuleQuotientAddSubgroupTorsion : {R : Type u_3} →
  {M : Type u_4} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → Module R (M ⧸ AddCommGroup.torsion M)
-- Batteries.Data.Vector.Lemmas
Vector.toArray_scanlM : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : β → α → m β} {as : Vector α n}, Vector.toArray <$> Vector.scanlM f init as = Array.scanlM f init as.toArray
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a fallback : α}, (m.insert k).getD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getD a fallback
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.continuousOn_face_Icc : ∀ {X : Type u_2} [inst : TopologicalSpace X] {n : ℕ} {f : (Fin (n + 1) → ℝ) → X} {I : BoxIntegral.Box (Fin (n + 1))},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ {i : Fin (n + 1)} {x : ℝ},
      x ∈ Set.Icc (I.lower i) (I.upper i) → ContinuousOn (f ∘ i.insertNth x) (BoxIntegral.Box.Icc (I.face i))
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.instInvolutiveStarOfContinuousStar : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : InvolutiveStar β] → [ContinuousStar β] → InvolutiveStar C(α, β)
-- Mathlib.Analysis.LocallyConvex.Barrelled
BarrelledSpace.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  [inst_3 : TopologicalSpace E], (∀ (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p) → BarrelledSpace 𝕜 E
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialToCosimplicialAugmented_map_right : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ}
  (f : X ⟶ Y),
  ((CategoryTheory.simplicialToCosimplicialAugmented C).map f).right = CategoryTheory.NatTrans.rightOp f.unop.left
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_antiperiodic : Function.Antiperiodic Real.cos Real.pi
-- Mathlib.Combinatorics.SimpleGraph.Star
/-- On (starGraph r), r is adjacent to v iff v ≠ r.  -/
SimpleGraph.starGraph_adj_center_iff : ∀ {V : Type u_1} {r v : V}, (SimpleGraph.starGraph r).Adj r v ↔ r ≠ v
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso_inv_eq_plusLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  (hP : CategoryTheory.Presheaf.IsSheaf J ((J.plusObj P).comp F)),
  (J.plusCompIso F P).inv = J.plusLift (CategoryTheory.Functor.whiskerRight (J.toPlus P) F) hP
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
AddHom.le_map_tsub : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α]
  [inst_4 : Preorder β] [inst_5 : Add β] [inst_6 : Sub β] [OrderedSub β] (f : α →ₙ+ β),
  Monotone ⇑f → ∀ (a b : α), f a - f b ≤ f (a - b)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' => h_2 sz k' v' l' r') =
    h_1 ()
-- Mathlib.Data.Int.ModEq
Int.sub_modulus_modEq_iff : ∀ {n a b : ℤ}, a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Aesop.Tree.Traversal
Aesop.traverseUp : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Bool) →
        (Aesop.GoalRef → m Unit) →
          (Aesop.RappRef → m Bool) →
            (Aesop.RappRef → m Unit) →
              (Aesop.MVarClusterRef → m Bool) → (Aesop.MVarClusterRef → m Unit) → Aesop.TreeRef → m Unit
-- Mathlib.Algebra.Group.Defs
AddZeroClass.toAddZero : {M : Type u} → [self : AddZeroClass M] → AddZero M
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_ite_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => x = b] (a : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  (∑'[L] (b' : β), if b' = b then a b' else 0) = a b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_inf : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s t : Subring R) (f : R →+* S),
  Function.Injective ⇑f → Subring.map f (s ⊓ t) = Subring.map f s ⊓ Subring.map f t
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.Reorder.mk.injEq : ∀ (univReorder : Mathlib.Tactic.Translate.Permutation) (reorder : Mathlib.Tactic.Translate.ArgReorder)
  (univReorder_1 : Mathlib.Tactic.Translate.Permutation) (reorder_1 : Mathlib.Tactic.Translate.ArgReorder),
  ({ univReorder := univReorder, reorder := reorder } = { univReorder := univReorder_1, reorder := reorder_1 }) =
    (univReorder = univReorder_1 ∧ reorder = reorder_1)
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.piScalarRight_tmul_apply : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {ι : Type u_4}
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : A) (y : ι → R) (i : ι),
  (Algebra.TensorProduct.piScalarRight R S A ι) (x ⊗ₜ[R] y) i = y i • x
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instModule : {R : Type u_1} → [inst : Semiring R] → [Module R ℝ] → Module R ℂ
-- Init.PropLemmas
forall₃_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop},
  (∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) →
    ((∀ (a : α) (b : β a) (c : γ a b), p a b c) ↔ ∀ (a : α) (b : β a) (c : γ a b), q a b c)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.zero_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (v : ι → M), 0 v = 0
-- Mathlib.Topology.Constructions
ContinuousAt.finInsertNth : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] (i : Fin (n + 1)) {f : X → A i}
  {g : X → (j : Fin n) → A (i.succAbove j)} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => i.insertNth (f a) (g a)) x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.mul : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S},
  f₁ =O[l] g₁ → f₂ =O[l] g₂ → (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x
-- Mathlib.RingTheory.FreeRing
/-- The canonical map from α to `FreeRing α`.  -/
FreeRing.of : {α : Type u} → α → FreeRing α
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (Std.Slice.toArray xs).extract (lo + 1) hi
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.add CommRingCat.Colimits.Prequotient.zero) x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, U = V ↔ ↑U = ↑V
-- Mathlib.Geometry.Manifold.Notation
/-- `CMDiffAt n f x` elaborates to `ContMDiffAt I J n f x`
trying to determine `I` and `J` from the local context.
`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).
The argument `x` can be omitted.  -/
Manifold.termCMDiffAt____ : Lean.ParserDescr
-- Mathlib.Data.PNat.Basic
PNat.sub_add_of_lt : ∀ {a b : ℕ+}, b < a → a - b + b = a
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_ne_top`.

---

In a metric space, the minimal edistance to a nonempty set is finite.  -/
Metric.infEdist_ne_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, s.Nonempty → Metric.infEDist x s ≠ ⊤
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The natural inclusion induced by implications of morphism properties.  -/
CategoryTheory.MorphismProperty.Arrow.changeProp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q W : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : W.IsMultiplicative] →
          {P' Q' W' : CategoryTheory.MorphismProperty T} →
            [inst_3 : Q'.IsMultiplicative] →
              [inst_4 : W'.IsMultiplicative] →
                P ≤ P' → Q ≤ Q' → W ≤ W' → CategoryTheory.Functor (P.Arrow Q W) (P'.Arrow Q' W')
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit_obj_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  {H : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {k : K} {W : C} {f g : (CategoryTheory.Limits.colimit H).obj k ⟶ W},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k) f =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k) g) →
    f = g
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.QuasiCompact.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)) → AlgebraicGeometry.QuasiCompact f
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.MonObj A], CategoryTheory.Mod.instInhabited A = { default := CategoryTheory.Mod.regular A }
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.kerLift_injective : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  Function.Injective ⇑(QuotientGroup.kerLift φ)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.rightOp j)
      (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).hom =
    (CategoryTheory.Limits.limit.π F (Opposite.op j)).op
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] {f : β × γ → α},
  BddAbove (Set.range f) → ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
-- Mathlib.Order.Fin.Tuple
Fin.consOrderIso_toEquiv : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)],
  (Fin.consOrderIso α).toEquiv = Fin.consEquiv α
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.trans : ∀ {R : Type u_6} (A : Type u_7) (M : Type u_8) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [IsScalarTower R A M] [Module.Finite R A]
  [Module.Finite A M], Module.Finite R M
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F : C ⥤ D` is fully faithful, every isomorphism `F.obj X ≅ F.obj Y` has a preimage.  -/
CategoryTheory.Functor.preimageIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X Y : C} → [F.Full] → [F.Faithful] → (F.obj X ≅ F.obj Y) → (X ≅ Y)
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (ys : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match [], ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_1 ys
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSymbolInformation : Lean.FromJson Lean.Lsp.SymbolInformation
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_neg : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Ring R] [inst_1 : Ring S] (f : R →+ S)
  (x : AddMonoidAlgebra R M), AddMonoidAlgebra.map f (-x) = -AddMonoidAlgebra.map f x
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addGroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddGroup (f i)],
  Pi.addGroup = { toSubNegMonoid := Pi.subNegMonoid, neg_add_cancel := ⋯ }
-- Mathlib.Data.Real.ConjExponents
Real.holderConjugate_comm : ∀ {p q : ℝ}, p.HolderConjugate q ↔ q.HolderConjugate p
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop},
  (∀ᶠ (a : β) in f, p a → u a = v a) → Filter.blimsup u f p = Filter.blimsup v f p
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.mulSingle.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (i : I),
  MonoidHom.mulSingle f i = { toOneHom := OneHom.mulSingle f i, map_mul' := ⋯ }
-- Batteries.Data.AssocList
Batteries.AssocList.find?.eq_def : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (x : Batteries.AssocList α β),
  Batteries.AssocList.find? a x =
    match x with
    | Batteries.AssocList.nil => none
    | Batteries.AssocList.cons k v es =>
      match k == a with
      | true => some v
      | false => Batteries.AssocList.find? a es
-- Plausible.Testable
Plausible.NamedBinder.eq_1 : ∀ (_n : String) (p : Prop), Plausible.NamedBinder _n p = p
-- Mathlib.Topology.Compactness.Lindelof
/-- **Alias** of `Quot.lindelofSpace`. -/
Quot.LindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop} [LindelofSpace X], LindelofSpace (Quot r)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.nnnorm_le_one_iff_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A),
  autoParam (0 ≤ a) CStarAlgebra.nnnorm_le_one_iff_of_nonneg._auto_1 → (‖a‖₊ ≤ 1 ↔ a ≤ 1)
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.foldlM.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match 0 with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_1 ()
-- Mathlib.Algebra.Regular.ULift
ULift.isLeftRegular_up : ∀ {R : Type v} [inst : Mul R] {a : R}, IsLeftRegular { down := a } ↔ IsLeftRegular a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_set_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {g : β → Set α},
  Measurable g ↔ ∀ (a : α), Measurable fun x => a ∈ g x
-- Mathlib.Order.Filter.Pi
Filter.hasBasis_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {ι' : ι → Type u_3} {s : (i : ι) → ι' i → Set (α i)}
  {p : (i : ι) → ι' i → Prop},
  (∀ (i : ι), (f i).HasBasis (p i) (s i)) →
    (Filter.pi f).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => If.1.pi fun i => s i (If.2 i)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getCommRingInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- The connecting homomorphism `δ` is actually a natural transformation between
`groupCohomology.funtor`s.  -/
groupCohomology.δ_naturality : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X1 X2 : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX1 : X1.ShortExact) (hX2 : X2.ShortExact) (F : X1 ⟶ X2) (i j : ℕ) (hij : i + 1 = j),
  CategoryTheory.CategoryStruct.comp (groupCohomology.δ hX1 i j hij) (groupCohomology.map (MonoidHom.id G) F.τ₁ j) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) F.τ₃ i) (groupCohomology.δ hX2 i j hij)
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.Shrink.eq_1 : ∀ (α : Type u), Std.Shrink α = ↑Std.Internal.idOpaque✝ α
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), CategoryTheory.IsIso (t.eTruncGEπ ⊥)
-- Std.Time.Date.ValidDate
Std.Time.instInhabitedValidDate : {l : Bool} → Inhabited (Std.Time.ValidDate l)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lsubtypeDomain_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (f : α →₀ M), (Finsupp.lsubtypeDomain s) f = Finsupp.subtypeDomain (fun x => x ∈ s) f
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.toCommGrp_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.Preadditive.toCommGrp C).map f =
    CategoryTheory.InducedCategory.homMk (CategoryTheory.Grp.homMk'' f ⋯ ⋯)
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorem.mk.sizeOf_spec : ∀ (funPropName thmName : Lean.Name)
  (keys : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)) (priority : ℕ),
  sizeOf { funPropName := funPropName, thmName := thmName, keys := keys, priority := priority } =
    1 + sizeOf funPropName + sizeOf thmName + sizeOf keys + sizeOf priority