mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mem_doubleCoset_of_not_disjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : G},
  ¬Disjoint (DoubleCoset.doubleCoset a ↑H ↑K) (DoubleCoset.doubleCoset b ↑H ↑K) → b ∈ DoubleCoset.doubleCoset a ↑H ↑K
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_congr : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂]
  [inst_12 : Module R₂ N₂] [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] {σ₂₁ : R₂ →+* R}
  [inst_15 : RingHomInvPair σ₁₂ σ₂₁] [inst_16 : RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂}
  [inst_17 : RingHomInvPair σ₂₃ σ₃₂] [inst_18 : RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R}
  [inst_19 : RingHomInvPair σ₁₃ σ₃₁] [inst_20 : RingHomInvPair σ₃₁ σ₁₃] [inst_21 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_22 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂)
  (g₁ : N ≃ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N),
  (TensorProduct.congr f₂ g₂) ((TensorProduct.congr f₁ g₁) x) = (TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂)) x
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.instIsCompactlyGenerated : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsCompactlyGenerated (Submodule R M)
-- Mathlib.Order.Heyting.Basic
sup_sdiff_right_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a ⊔ b) \ b = a \ b
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.Int.neg.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Data.ZMod.Units
ZMod.not_isUnit_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → ¬IsUnit ↑p
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_hom_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} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f.right F),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).hom.right = g.hom
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.mk.injEq : ∀ (lctx : Lean.LocalContext) (c : Lean.Expr) (gen numCases : ℕ) (splitSource : Lean.Meta.Grind.SplitSource)
  (lctx_1 : Lean.LocalContext) (c_1 : Lean.Expr) (gen_1 numCases_1 : ℕ) (splitSource_1 : Lean.Meta.Grind.SplitSource),
  ({ lctx := lctx, c := c, gen := gen, numCases := numCases, splitSource := splitSource } =
      { lctx := lctx_1, c := c_1, gen := gen_1, numCases := numCases_1, splitSource := splitSource_1 }) =
    (lctx = lctx_1 ∧ c = c_1 ∧ gen = gen_1 ∧ numCases = numCases_1 ∧ splitSource = splitSource_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_of_not_and_and : ∀ {R : Type u_1} {A : Type u_2} {p : 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 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬(p a ∧ ContinuousOn f (quasispectrum R a) ∧ f 0 = 0) → cfcₙ f a = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.filter f m)[k]! = (Option.filter (f k') m[k]?).get!
-- Init.Data.Fin.Fold
Fin.last.eq_1 : ∀ (n : ℕ), Fin.last n = ⟨n, ⋯⟩
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyGet_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : σ → α × σ),
  (Std.Do.wp (MonadStateOf.modifyGet f)).apply Q = fun s => Q.1 (f s).1 (f s).2
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.IsZero Y → CategoryTheory.Limits.IsZero X
-- Mathlib.Data.Set.Sigma
Set.biUnion_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β),
  ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_natCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (n : ℕ), (↑n).ofVal = ↑n
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.isRightDerivedFunctor_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (F' : CategoryTheory.Functor D H) (e : L.comp F' ≅ F), F'.IsRightDerivedFunctor e.inv W
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀)
  (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k))
  (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C}
  (h : F.Y ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (u₁ i j k)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (CategoryTheory.CategoryStruct.comp (z i' j' ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) =
    CategoryTheory.CategoryStruct.comp (z i j k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv h)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_eq_sum : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.upcrossingsBefore a b f N ω =
      ∑ i ∈ Finset.Ico 1 (N + 1), {n | MeasureTheory.upperCrossingTime a b f N n ω < N}.indicator 1 i
-- Mathlib.Data.Num.ZNum
ZNum.zneg_pred : ∀ (n : ZNum), -n.pred = (-n).succ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_empty_iff : ∀ {m n : ℤ}, (m...n).toArray = #[] ↔ n ≤ m
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_one : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne], UpperHalfPlane.qExpansion h ⇑1 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k fallback : α}, (compare (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.const_iff : ∀ {c : Tactic.ComputeAsymptotics.MultiseriesExpansion []}, c.IsZero ↔ c.toReal = 0
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.Nondegenerate.toBilin' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  M.Nondegenerate → (Matrix.toBilin' M).Nondegenerate
-- Mathlib.Algebra.Category.Grp.AB
instPreservesFiniteLimitsFunctorAddCommGrpCatColim : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `(K.truncGE' e).X i ≅ K.opcycles i'` when `e.f i = i'`
and `e.BoundaryGE i` holds.  -/
HomologicalComplex.truncGE'XIsoOpcycles : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      {i : ι} → {i' : ι'} → e.f i = i' → e.BoundaryGE i → ((K.truncGE' e).X i ≅ K.opcycles i')
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- Copy of a local subring with a new `carrier` equal to the old one.
Useful to fix definitional equalities.  -/
LocalSubring.copy : {R : Type u_1} → [inst : CommRing R] → (S : LocalSubring R) → (s : Set R) → s = ↑S.toSubring → LocalSubring R
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
_private.Std.Data.Iterators.Lemmas.Equivalence.StepCongr.0.Std.IterM.Equiv.step_eq.aux : ∀ {β α₁ α₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb →
    ∀ {s : Std.IterStep (Quot (Std.BundledIterM.Equiv m β)) β},
      (Std.Iterators.HetT.map Std.IterStep.bundledQuotient ita.stepAsHetT).Property s → ∃ s', s = (↑s').bundledQuotient
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsOpenEmbedding g → Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding (g ∘ f)
-- Mathlib.Data.Fintype.Fin
Fin.Iio_castSucc : ∀ {n : ℕ} (i : Fin n), Finset.Iio i.castSucc = Finset.map Fin.castSuccEmb (Finset.Iio i)
-- Mathlib.SetTheory.ZFC.Class
/-- The universal class  -/
Class.univ : Class.{u_1}
-- Std.Do.Triple.SpecLemmas
/-- Appending the prefix to the suffix yields the original list.  -/
List.Cursor.property : ∀ {α : Type u} {l : List α} (self : l.Cursor), self.prefix ++ self.suffix = l
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.algHom_ext_iff : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M]
  {φ₁ φ₂ : MonoidAlgebra A M →ₐ[R] B},
  φ₁ = φ₂ ↔
    (∀ (m : M), φ₁ (MonoidAlgebra.single m 1) = φ₂ (MonoidAlgebra.single m 1)) ∧
      φ₁.comp MonoidAlgebra.singleOneAlgHom = φ₂.comp MonoidAlgebra.singleOneAlgHom
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α}, ∅.getKey! a = default
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an `AddGroup` inherits a subtraction.  -/
AddSubgroupClass.sub : {G : Type u_5} →
  {S : Type u_6} → [inst : SubNegMonoid G] → [inst_1 : SetLike S G] → [AddSubgroupClass S G] → {H : S} → Sub ↥H
-- Mathlib.Data.Set.Function
Equiv.bijOn : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β}, (∀ (a : α), e a ∈ t ↔ a ∈ s) → Set.BijOn (⇑e) s t
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.ball_strictAnti : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M], StrictAnti (FiniteArchimedeanClass.ball K)
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
/-- Constructor for constant functor  -/
MvQPF.Const.mk : {n : ℕ} → {A : Type u} → {α : TypeVec.{u} n} → A → MvQPF.Const n A α
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where an antitone function is not continuous
is at most countable.  -/
Antitone.countable_not_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β],
  Antitone f → {x | ¬ContinuousAt f x}.Countable
-- Mathlib.Topology.MetricSpace.Isometry
/-- The natural `IsometryEquiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`.
`Fin.appendEquiv` as an `IsometryEquiv`.  -/
Fin.appendIsometry : {α : Type u} → [inst : PseudoEMetricSpace α] → (m n : ℕ) → (Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α), f.support = {x | f x ≠ x}
-- Lean.Declaration
/-- Number of parameters. A parameter is an argument to the defined type that is fixed over constructors.
An example of this is the `α : Type` argument in the vector constructors
`nil : Vector α 0` and `cons : α → Vector α n → Vector α (n+1)`.

The intuition is that the inductive type must exhibit _parametric polymorphism_ over the inductive
parameter, as opposed to _ad-hoc polymorphism_.
 -/
Lean.InductiveVal.numParams : Lean.InductiveVal → ℕ
-- Mathlib.Algebra.Order.Ring.Interval
/-- Let `k : ℤ`. If its multiple of `r > 0` in a strict ordered ring lies strictly between
multiples `r * (m - 1)` and `r * (n + 1)`, then `m ≤ k ≤ n`.  -/
IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {r : R},
  0 < r → ∀ {k m n : ℤ}, r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(n + 1)) → k ∈ Finset.Icc m n
-- Mathlib.Data.Set.Lattice
Set.sUnion_eq_iUnion : ∀ {α : Type u_1} {s : Set (Set α)}, ⋃₀ s = ⋃ i, ↑i
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.variation_transpose_le : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (μ.transpose B).variation ≤ ‖B‖₊ • μ.variation
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightEq_hom_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r r' : R₂ ⟶ R₁) (h : r = r') (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightEq L r r' h).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_unitOfList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  (Std.ExtHashMap.unitOfList l).size ≤ l.length
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_think : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.WSeq α), Stream'.WSeq.map f s.think = (Stream'.WSeq.map f s).think
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_eq_lsub : ∀ {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [inst : IsWellOrder ι r] [inst_1 : IsWellOrder ι' r']
  {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o)
  (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = Ordinal.lsub (Ordinal.familyOfBFamily' r' ho' f)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.class.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.class = 1
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodProdProdComm_apply : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'] (mnmn : (M × N) × M' × N'),
  (MulEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- A canonical bilinear form on the span of roots in a finite root pairing, taking values in a
commutative ring, where the root-coroot pairing takes values in that ring.  -/
RootPairing.RootFormIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_5) →
                      [inst_5 : CommRing S] →
                        [inst_6 : Algebra S R] →
                          [FaithfulSMul S R] →
                            [inst_8 : Module S M] →
                              [IsScalarTower S R M] →
                                [P.IsValuedIn S] → [Fintype ι] → LinearMap.BilinForm S ↥(P.rootSpan S)
-- Mathlib.Topology.Order.Hom.Esakia
/-- Copy of a `PseudoEpimorphism` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
PseudoEpimorphism.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → (f : PseudoEpimorphism α β) → (f' : α → β) → f' = ⇑f → PseudoEpimorphism α β
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₂_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (j : J) (h' : c₁.π c₂ c (i₁, i₂') = j),
      HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j =
        c₁.ε₂ c₂ c (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h')
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_right₀ : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ), (Turing.Tape.mk' L R).right₀ = R
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SL2.transvection_induction : ∀ {F : Type u_1} [inst : Field F] (P : Matrix.SpecialLinearGroup (Fin 2) F → Prop),
  (∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (Matrix.SpecialLinearGroup.transvection h c)) →
    (∀ (A B : Matrix.SpecialLinearGroup (Fin 2) F), P A → P B → P (A * B)) →
      ∀ (A : Matrix.SpecialLinearGroup (Fin 2) F), P A
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval_toMvPolynomial : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (f : σ → R) (i : σ) (p : Polynomial R),
  (MvPolynomial.eval f) ((Polynomial.toMvPolynomial i) p) = Polynomial.eval (f i) p
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.cancel_left : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {g f₁ f₂ : CentroidHom α},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Order.Filter.CountableInter
/-- Infimum of two `CountableInterFilter`s is a `CountableInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`.  -/
countableInterFilter_inf : ∀ {α : Type u_2} (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂], CountableInterFilter (l₁ ⊓ l₂)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comap_comp : ∀ {R : Type u} {S : Type v} {S' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommSemiring S']
  (f : R →+* S) (g : S →+* S'), PrimeSpectrum.comap (g.comp f) = PrimeSpectrum.comap f ∘ PrimeSpectrum.comap g
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAdd : {α : Type u} → [Add α] → Add (WithZero α)
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.closure_coe_completion_v_lt : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {γ : Γ₀ˣ}, closure (UniformSpace.Completion.coe' '' {x | Valued.v x < ↑γ}) = {x | Valued.extensionValuation x < ↑γ}
-- Mathlib.Logic.Relation
Relation.ReflTransGen.lift : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} (f : α → β),
  r ≤ Function.onFun p f → Relation.ReflTransGen r ≤ Function.onFun (Relation.ReflTransGen p) f
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.toEnd_eq : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) [inst_8 : LieModule.LinearWeights R L M] (x : L),
  (LieModule.toEnd R L ↥(LieModule.shiftedGenWeightSpace R L M χ)) x =
    (LieModule.shiftedGenWeightSpace.shift R L M χ).conj
      ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ)) x - χ x • LinearMap.id)
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_compL_besselPotential : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (s s' : ℝ),
  TemperedDistribution.besselPotential E F s' ∘SL TemperedDistribution.besselPotential E F s =
    TemperedDistribution.besselPotential E F (s + s')
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instPow : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Monoid β] → [ContinuousMul β] → Pow C(α, β) ℕ
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_d'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j),
  ¬c.Rel j (c.next j) →
    ∀ {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) =
        CategoryTheory.CategoryStruct.comp (φ.f j)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) h)