mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.CharAndCard
/-- A prime `p` is a unit in a finite commutative ring `R`
iff it does not divide the characteristic.  -/
isUnit_iff_not_dvd_char : ∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Finite R], IsUnit ↑p ↔ ¬p ∣ ringChar R
-- Mathlib.CategoryTheory.Category.Cat.AsSmall
CategoryTheory.Cat.asSmallFunctor_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y),
  CategoryTheory.Cat.asSmallFunctor.map F =
    (CategoryTheory.AsSmall.down.comp (F.toFunctor.comp CategoryTheory.AsSmall.up)).toCatHom
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_zero_fun : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.lintegral μ 0 = 0
-- Init.Data.BitVec.Lemmas
BitVec.negOverflow.eq_1 : ∀ {w : ℕ} (x : BitVec w), x.negOverflow = (x.toInt == -2 ^ (w - 1))
-- Mathlib.RingTheory.Perfection
/-- The canonical perfection map from the perfection of a ring.  -/
PerfectionMap.of : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p],
  PerfectionMap p (Perfection.coeff R p 0)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toArray_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.keys.toArray = m.keysArray
-- Mathlib.Order.WithBot
WithTop.le_def : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α}, x ≤ y ↔ y = ⊤ ∨ ∃ a b, a ≤ b ∧ x = ↑a ∧ y = ↑b
-- Mathlib.LinearAlgebra.Matrix.Defs
Set.mem_matrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {S : Set α} {M : Matrix m n α}, M ∈ S.matrix ↔ ∀ (i : m) (j : n), M i j ∈ S
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instForallOfFinite : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_4} [Finite ι], Algebra.IsFiniteSplit R (ι → R)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.rootD_empty : ∀ {a : ℕ}, Batteries.UnionFind.empty.rootD a = a
-- Mathlib.Data.List.Basic
List.length_injective : ∀ {α : Type u} [Subsingleton α], Function.Injective List.length
-- Mathlib.NumberTheory.Multiplicity
padicValNat.pow_two_sub_one : ∀ {x n : ℕ},
  1 < x →
    ¬2 ∣ x →
      n ≠ 0 → Even n → padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsDominant
-- Mathlib.Data.Rat.Init
NNRat.den_mk : ∀ (q : ℚ) (hq : 0 ≤ q), NNRat.den ⟨q, hq⟩ = q.den
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
DifferentiableAt.lineDeriv_eq_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {x v : E}, DifferentiableAt 𝕜 f x → lineDeriv 𝕜 f x v = (fderiv 𝕜 f x) v
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The **Holley Inequality**.  -/
holley : ∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f g μ : α → β) [inst_5 : Fintype α],
  0 ≤ μ →
    0 ≤ f →
      0 ≤ g →
        Monotone μ →
          ∑ a, f a = ∑ a, g a → (∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) → ∑ a, μ a * f a ≤ ∑ a, μ a * g a
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  (g : sInfHom β γ) (f : sInfHom α β), sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι),
  Differentiable 𝕜 fun f => f i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.braiding_hom_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (β_ R S).hom = (CategoryTheory.Limits.pullbackSymmetry R.hom S.hom).hom
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.mk.sizeOf_spec : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] [inst_6 : SizeOf A] [inst_7 : SizeOf B] (toRingEquiv : A ≃+* B)
  (map_star' : ∀ (a : A), toRingEquiv.toFun (star a) = star (toRingEquiv.toFun a)),
  sizeOf { toRingEquiv := toRingEquiv, map_star' := map_star' } = 1 + sizeOf toRingEquiv
-- Lean.Message
Lean.MessageData.arrayExpr.toMessageData : Array Lean.Expr → ℕ → Lean.MessageData → Lean.MessageData
-- Mathlib.SetTheory.Ordinal.Notation
ONote.FundamentalSequenceProp.eq_2 : ∀ (o a : ONote), o.FundamentalSequenceProp (Sum.inl (some a)) = (o.repr = Order.succ a.repr ∧ (o.NF → a.NF))
-- Mathlib.Algebra.Group.Prod
Prod.instAddRightCancelSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddRightCancelSemigroup G] [inst_1 : AddRightCancelSemigroup H],
  Prod.instAddRightCancelSemigroup = { toAddSemigroup := Prod.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Init.Data.List.Lemmas
List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α}, l ≠ [] → ∃ b l', l = b :: l'
-- Mathlib.GroupTheory.Commutator.Finite
Subgroup.instFGSubtypeMemCommutator : ∀ {G : Type u_1} [inst : Group G] [Finite ↑(commutatorSet G)], Group.FG ↥(commutator G)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_sheafification : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] (K : Type t) [inst_8 : CategoryTheory.SmallCategory K]
  [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D]
  [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)]
  [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)],
  CategoryTheory.Limits.PreservesLimitsOfShape K (J.sheafification D)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofBijective_apply : ∀ {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B]
  [inst_9 : StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f) (a : A), (StarAlgEquiv.ofBijective f hf) a = f a
-- Mathlib.Topology.UniformSpace.CompleteSeparated
IsDenseInducing.continuous_extend_of_cauchy : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {γ : Type u_4}
  [inst_2 : UniformSpace γ] [CompleteSpace γ] [T0Space γ] {e : α → β} {f : α → γ} (de : IsDenseInducing e),
  (∀ (b : β), Cauchy (Filter.map f (Filter.comap e (nhds b)))) → Continuous (de.extend f)
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics (`aroots` version).  -/
Polynomial.eq_mul_mul_of_aroots_quadratic_eq_pair : ∀ {T : Type u_2} {S : Type u_3} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  {a b c : T} {x1 x2 : S},
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).aroots S = {x1, x2} →
    (algebraMap T S) c = (algebraMap T S) a * x1 * x2
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ↑S.toSubsemiring = ↑S
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ico_succ_left_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] (a b : α),
  Finset.Ico (Order.succ a) b = Finset.Ioo a b
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical_mul_radical : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a : E}, EuclideanDomain.divRadical a * UniqueFactorizationMonoid.radical a = a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductLimitCone_cone : ∀ (X Y : Type u),
  (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for a family of functions `f : Fin (n + 1) → ℝⁿ⁺¹ → E`. See also
`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable'` for a version formulated
in terms of a vector-valued function `f : ℝⁿ⁺¹ → Eⁿ⁺¹`.  -/
MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable' : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ),
  a ≤ b →
    ∀ (f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E) (f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E)
      (s : Set (Fin (n + 1) → ℝ)),
      s.Countable →
        (∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) →
          (∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) →
            MeasureTheory.IntegrableOn (fun x => ∑ i, (f' i x) (Pi.single i 1)) (Set.Icc a b) MeasureTheory.volume →
              ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' i x) (Pi.single i 1) =
                ∑ i,
                  ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (b i) x)) -
                    ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (a i) x))
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isThin_of_isCoseparating_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], ⊥.IsCoseparating → Quiver.IsThin C
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- If `M` is an `R`-module and `ι` is a type, then an additive endomorphism of `M` that
commutes with all `R`-endomorphisms of `M` gives rise to an additive endomorphism of `ι →₀ M`
that commutes with all `R`-endomorphisms of `ι →₀ M`.  -/
Module.End.ringHomEndFinsupp : (ι : Type u_4) →
  {R : Type u_5} →
    {M : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.End (Module.End R M) M →+* Module.End (Module.End R (ι →₀ M)) (ι →₀ M)
-- Mathlib.Computability.Partrec
Nat.Partrec.succ : Nat.Partrec ↑Nat.succ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rco_eq_add : ∀ {m n i fallback : ℕ}, i < n - m → (m...n).toList.getD i fallback = m + i
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_one_iff : ∀ {α : Type u_1} (F : Type u_4) {E''' : Type u_12} [inst : Norm F] [inst_1 : SeminormedAddGroup E'''] {l : Filter α}
  [inst_2 : One F] [NormOneClass F] {f : α → E'''}, (f =o[l] fun _x => 1) ↔ Filter.Tendsto f l (nhds 0)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.hom₂_ext_iff : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b} {x y : α ⟶ β},
  x = y ↔ x.τl = y.τl
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle between three points is zero if and only if one of the first and third
points is weakly between the other two.  -/
EuclideanGeometry.oangle_eq_zero_iff_wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
-- Mathlib.Order.Nucleus
Nucleus.map_inf : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n : Nucleus X} {x y : X}, n (x ⊓ y) = n x ⊓ n y
-- Init.Core
Std.Trichotomous.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a b : α), ¬r a b → ¬r b a → a = b) → Std.Trichotomous r
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_disjoint_of_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t₁ t₂ : (a : α) → Finset (δ a))
  {a : α}, Disjoint (t₁ a) (t₂ a) → Disjoint (Fintype.piFinset t₁) (Fintype.piFinset t₂)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsLittleO.trans_isTheta : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [inst : Norm E] [inst_1 : Norm F]
  [inst_2 : SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'},
  f =o[l] g → g =Θ[l] k → f =o[l] k
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_ne_top_iff : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {p : Submodule R M} [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_8 : RingHomInvPair σ₂₁ σ₁₂] {e : M ≃ₛₗ[σ₁₂] M₂}, Submodule.map (↑e) p ≠ ⊤ ↔ p ≠ ⊤
-- Mathlib.RingTheory.Localization.Module
/-- An `R`-module isomorphism `M ≃ₗ[R] N` gives an `Rₛ`-module isomorphism `Mₛ ≃ₗ[Rₛ] Nₛ`.  -/
IsLocalizedModule.mapEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M'] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M'] →
                  (f : M →ₗ[R] M') →
                    [IsLocalizedModule S f] →
                      {N : Type u_4} →
                        {N' : Type u_5} →
                          [inst_6 : AddCommMonoid N] →
                            [inst_7 : AddCommMonoid N'] →
                              [inst_8 : Module R N] →
                                [inst_9 : Module R N'] →
                                  (g : N →ₗ[R] N') →
                                    [IsLocalizedModule S g] →
                                      (Rₛ : Type u_6) →
                                        [inst_11 : CommSemiring Rₛ] →
                                          [inst_12 : Algebra R Rₛ] →
                                            [inst_13 : Module Rₛ M'] →
                                              [inst_14 : Module Rₛ N'] →
                                                [IsScalarTower R Rₛ M'] →
                                                  [IsScalarTower R Rₛ N'] →
                                                    [IsLocalization S Rₛ] → (M ≃ₗ[R] N) → M' ≃ₗ[Rₛ] N'
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_mem_nonZeroDivisors_iff : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  QuadraticAlgebra.norm z ∈ nonZeroDivisors R ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)
-- Mathlib.Analysis.Convex.StrictConvexBetween
eq_lineMap_of_dist_eq_mul_of_dist_eq_mul : ∀ {E : Type u_3} {PE : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E]
  [inst_3 : MetricSpace PE] [inst_4 : NormedAddTorsor E PE] {r : ℝ} {x y z : PE},
  dist x y = r * dist x z → dist y z = (1 - r) * dist x z → y = (AffineMap.lineMap x z) r
-- Mathlib.Analysis.Normed.Group.AddTorsor
IsometryEquiv.vaddConst_apply : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x : P) (v : V), (IsometryEquiv.vaddConst x) v = v +ᵥ x
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.mk : {m : Type u → Type u} →
  (listM : Type u → Type u) →
    ({α : Type u} → listM α) →
      ({α : Type u} → α → listM α → listM α) →
        ({α : Type u} → (Unit → listM α) → listM α) →
          ({α : Type u} → (Unit → m (listM α)) → listM α) →
            ({α : Type u} → [Monad m] → listM α → m (Option (α × listM α))) →
              ({α : Type u} → listM α → Option (Option (α × listM α))) → MLList.Spec✝ m
-- Init.Data.Float.Model.Float
Float.Model.instDecidableLE : DecidableLE Float.Model
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor.eq_1 : ∀ {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 E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G),
  CategoryTheory.Join.mkFunctor F G α =
    {
      obj := fun X =>
        match X with
        | CategoryTheory.Join.left x => F.obj x
        | CategoryTheory.Join.right x => G.obj x,
      map := fun {X Y} f =>
        CategoryTheory.Join.homInduction (fun x x_1 f => F.map f) (fun x x_1 g => G.map g) (fun c d => α.app (c, d)) f,
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ico_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)
-- Mathlib.LinearAlgebra.Dimension.DivisionRing
/-- Also see `rank_quotient_add_rank`.  -/
rank_quotient_add_rank_of_divisionRing : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (p : Submodule K V),
  Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
-- Batteries.Data.List.Interleave
List.interleave.eq_1 : ∀ {α : Type u_1} (x : List α), [].interleave x = x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).isEmpty = m.isEmpty
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofUserWidgetInfo.sizeOf_spec : ∀ (i : Lean.Elab.UserWidgetInfo), sizeOf (Lean.Elab.Info.ofUserWidgetInfo i) = 1 + sizeOf i
-- Mathlib.Data.Set.Lattice
Set.iInter_iInter_eq_right : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = x → Set α}, ⋂ x, ⋂ (h : b = x), s x h = s b ⋯
-- Init.Data.AC
Lean.Data.AC.Context.mk : {α : Sort u} →
  (op : α → α → α) →
    Std.Associative op →
      Option (PLift (Std.Commutative op)) →
        Option (PLift (Std.IdempotentOp op)) → List (Lean.Data.AC.Variable op) → α → Lean.Data.AC.Context α
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C}
  {f g : X ⟶ Y} (x : (F.obj X).obj)
  (h : (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) x),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.equalizer.ι f g)))
      ((CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g).symm ⟨x, h⟩) =
    x
-- Mathlib.Tactic.Algebra.Basic
/-- Given two rings, determine which is 'larger' in the sense that the larger is an algebra
over the smaller. Returns the first ring if they're the same or incompatible.  -/
Mathlib.Tactic.Algebra.pickLargerRing : (u : Lean.Level) × Q(Type u) → (u : Lean.Level) × Q(Type u) → Lean.MetaM ((u : Lean.Level) × Q(Type u))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGT_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂), t₁.getGT k h' = t₂.getGT k ⋯
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.pseudoEqual_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : C}, Std.Refl (CategoryTheory.Abelian.PseudoEqual P)
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → x ≤ n → Sort u_1) →
    (x : ℕ) → (x_1 : x ≤ n) → ((i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) → ((x : 0 ≤ n) → motive 0 x) → motive x x_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k k' fallback : α},
  (↑m).WF →
    ∀ {f : Option (β k) → Option (β k)},
      (m.alter k f).getKeyD k' fallback =
        if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_compl_singleton_one : ∀ {M : Type u_1} [inst : Group M], SimpleGraph.mulCayley {1}ᶜ = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The spectral sequence attached to a spectral object in an abelian category.  -/
CategoryTheory.Abelian.SpectralObject.spectralSequence : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    [X.HasSpectralSequence data] → CategoryTheory.SpectralSequence C c r₀
-- Mathlib.Tactic.FunProp.Theorems
/-- Apply theorem e.g. `Continuous fun (f : (x : X) → Y x ↦ f x)`  -/
Mathlib.Meta.FunProp.LambdaTheoremType.apply : Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Topology.MetricSpace.Defs
Metric.closedBall_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x : γ}, Metric.closedBall x 0 = {x}
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendsScalars_map_rightUnitor_inv_one_tmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom
        ((ModuleCat.extendScalars f).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv))
      (1 ⊗ₜ[R] m) =
    1 ⊗ₜ[R] (m ⊗ₜ[R] 1)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : C} {X₀ : C₀}
  (f : F.obj X₀ ⟶ X) (g : X ⟶ Y) {Z : A} (h : G₀.obj.obj (Opposite.op X₀) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀
        (CategoryTheory.CategoryStruct.comp f g))
      h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_id : ∀ (A : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A], ⇑(ContinuousAddMonoidHom.id A) = id