mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- A morphism in `Over X` from the chosen pullback along `g` of `f` to `Over.mk f`.  -/
CategoryTheory.ChosenPullbacksAlong.fst' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            (CategoryTheory.Over.map g).obj
                ((CategoryTheory.ChosenPullbacksAlong.pullback g).obj (CategoryTheory.Over.mk f)) ⟶
              CategoryTheory.Over.mk f
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_iff_subset : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
-- Mathlib.Algebra.Algebra.Unitization
/-- The functorial map on morphisms between the category of non-unital C⋆-algebras with non-unital
star homomorphisms and unital C⋆-algebras with unital star homomorphisms.

This sends `φ : A →⋆ₙₐ[R] B` to a map `Unitization R A →⋆ₐ[R] Unitization R B` given by the formula
`(r, a) ↦ (r, φ a)` (or perhaps more precisely,
`algebraMap R _ r + ↑a ↦ algebraMap R _ r + ↑(φ a)`).  -/
Unitization.starMap : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : NonUnitalSemiring A] →
            [inst_3 : StarRing A] →
              [inst_4 : Module R A] →
                [inst_5 : SMulCommClass R A A] →
                  [inst_6 : IsScalarTower R A A] →
                    [inst_7 : NonUnitalSemiring B] →
                      [inst_8 : StarRing B] →
                        [inst_9 : Module R B] →
                          [inst_10 : SMulCommClass R B B] →
                            [inst_11 : IsScalarTower R B B] →
                              [StarModule R B] → (A →⋆ₙₐ[R] B) → Unitization R A →⋆ₐ[R] Unitization R B
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_8 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftLeft rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_8 w n lhs rhs
-- Mathlib.Order.Max
IsBot.isMin_iff : ∀ {α : Type u_3} [inst : PartialOrder α] {i j : α}, IsBot i → (IsMin j ↔ j = i)
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.IsTotallyUnimodular.transpose : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] {A : Matrix m n R},
  A.IsTotallyUnimodular → A.transpose.IsTotallyUnimodular
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toIsometryEquiv_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.symm.toIsometryEquiv = e.toIsometryEquiv.symm
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_vadd_sphere : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ), (fun x => c +ᵥ x) ⁻¹' Metric.sphere x r = Metric.sphere (-c +ᵥ x) r
-- Lean.DocString.Extension
Lean.instReprVersoModuleDocs : Repr Lean.VersoModuleDocs
-- Mathlib.Topology.Algebra.Group.Matrix
Continuous.generalLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Continuous ⇑f → Continuous ⇑(Matrix.GeneralLinearGroup.map f)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- If a function is `C^n`, then its bundled derivative is `C^m` when `m+1 ≤ n`.  -/
ContMDiff.contMDiff_tangentMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} [Is : IsManifold I 1 M]
  [I's : IsManifold I' 1 M'], ContMDiff I I' n f → m + 1 ≤ n → ContMDiff I.tangent I'.tangent m (tangentMap I I' f)
-- Lean.Data.PersistentArray
Lean.PersistentArray.forIn : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → Lean.PersistentArray α → β → (α → β → m (ForInStep β)) → m β
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBasis_restrict_iff' : ∀ {α : Type u_1} {M : Matroid α} {R I X : Set α}, (M.restrict R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R
-- Init.Internal.Order.Basic
Lean.Order.monotone_dite : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.PartialOrder α] [inst_1 : Lean.Order.PartialOrder β] (c : Prop)
  [inst_2 : Decidable c] (k₁ : α → c → β) (k₂ : α → ¬c → β),
  Lean.Order.monotone k₁ → Lean.Order.monotone k₂ → Lean.Order.monotone fun x => dite c (k₁ x) (k₂ x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K))
  {x : NumberField.mixedEmbedding.mixedSpace K},
  (∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun w => ‖x.1 w‖, x.2) ∈ A) →
    x ∈ A →
      (∀ (w : { w // w.IsReal }), x.1 w ≠ 0) →
        (x ∈ ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A ↔
          (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Linearly evaluating a sequence in the completion at a given input.  -/
AdicCompletion.eval : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (n : ℕ) → AdicCompletion I M →ₗ[R] M ⧸ I ^ n • ⊤
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J]
  {D : CategoryTheory.Limits.Cocone F} {i j : J} (hD : CategoryTheory.Limits.IsColimit D)
  (x : CategoryTheory.ToType (F.obj i)) (y : CategoryTheory.ToType (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (D.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y →
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict_apply : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L] (σ : Gal(L/K))
  (x : B), ((galRestrict A K L B) σ) x = ((galRestrictHom A K L B) ↑σ) x
-- Mathlib.Algebra.Algebra.Rat
Rat.algebra_rat_subsingleton : ∀ {R : Type u_4} [inst : Semiring R], Subsingleton (Algebra ℚ R)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_apply_le_of_tendsto : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5} {l : Filter ι} [l.NeBot]
  {C : ℝ} {F : ι → ↥(lp E ⊤)},
  (∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) →
    ∀ {f : (a : α) → E a}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds f) → ∀ (a : α), ‖f a‖ ≤ C
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- The quotient `R/I` of a ring `R` by an ideal `I`,
defined to equal the quotient of `I` as an `R`-submodule of `R`.  -/
Ideal.instHasQuotient : {R : Type u} → [inst : Ring R] → HasQuotient R (Ideal R)
-- Lean.Expr
/-- Given `a : Int`, returns `- a`  -/
Lean.mkIntNeg : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.AddMon C} {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Mathlib.Order.Atoms
Prop.isCoatom_iff : ∀ {p : Prop}, IsCoatom p ↔ ¬p
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_eq_mul_pow_sub_pow_div_char_of_commute : ∀ (R : Type u_1) [inst : Ring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_monotone : ∀ {u v : ℕ → EReal}, u ≤ v → LinearGrowth.linearGrowthSup u ≤ LinearGrowth.linearGrowthSup v
-- Mathlib.Data.Int.Log
Int.log.eq_1 : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (b : ℕ) (r : R),
  Int.log b r = if 1 ≤ r then ↑(Nat.log b ⌊r⌋₊) else -↑(Nat.clog b ⌈r⁻¹⌉₊)
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_biSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ : Type u_5}
  [inst_1 : CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), LowerSemicontinuousWithinAt (f i hi) s x) →
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') s x
-- Init.Data.List.Sublist
List.instDecidableIsInfixOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁ <:+: l₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.le_mul_inv_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a ≤ b * ↑u⁻¹ ↔ a * ↑u ≤ b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap (-φ) = -CategoryTheory.ShortComplex.rightHomologyMap φ
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_monomial_eq_zero_of_not_subset : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : τ →₀ ℕ} (c : R), ¬↑s.support ⊆ Set.range f → (MvPolynomial.killCompl hf) ((MvPolynomial.monomial s) c) = 0
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.lift_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i),
  (DirectLimit.NonUnitalAlgebra.lift G f P g Hg) ((DirectLimit.NonUnitalAlgebra.of G f i) x) = (g i) x
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_mor₃ : ∀ {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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).mor₃ =
    CategoryTheory.CategoryStruct.comp v₂₃ w₁₂
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_toRingHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑↑e = ↑e
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.instCoeSortType : CoeSort MeasCat (Type u_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.mk : Lean.Lsp.ParameterInformationLabel → Option Lean.Lsp.MarkupContent → Lean.Lsp.ParameterInformation
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.coe_opensRestrict_apply_coe : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (a : (↑U).Opens),
  ↑↑((AlgebraicGeometry.opensRestrict U) a) = (fun a => ↑a) '' ↑a
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.GrothendieckTopology.OneHypercover.glueMorphisms.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f f_1 : (i : E.I₀) → E.X i ⟶ T) (e_f : f = f_1)
  (h :
    ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
      CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j)),
  E.glueMorphisms f h = E.glueMorphisms f_1 ⋯
-- Mathlib.Order.Max
IsTop.isMax_iff : ∀ {α : Type u_3} [inst : PartialOrder α] {i j : α}, IsTop i → (IsMax j ↔ j = i)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`.  -/
isClosedMap_smul₀ : ∀ {G₀ : Type u_4} [inst : GroupWithZero G₀] {E : Type u_5} [inst_1 : Zero E] [inst_2 : MulActionWithZero G₀ E]
  [inst_3 : TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀), IsClosedMap fun x => c • x
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_abs_right : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b : ℤ), IsEllipticNet.atom W a |b| = IsEllipticNet.atom W a b
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_bot : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], ⊥.FG
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_X_pow_self : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.coeff n) (PowerSeries.X ^ n) = 1
-- Mathlib.Logic.Function.Basic
Function.not_injective : Function.Injective Not
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instAdd : {α : ℚ} → Add (Std.Time.Internal.UnitVal α)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves all colimits if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesColimits_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)),
  (∀ (k : K),
      CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v', v, u', u}
        (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F
-- Mathlib.Probability.Kernel.RadonNikodym
/-- Singular part of the kernel `κ` with respect to the kernel `η`.  -/
ProbabilityTheory.Kernel.singularPart : {α : Type u_3} →
  {γ : Type u_4} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          (κ η : ProbabilityTheory.Kernel α γ) →
            [ProbabilityTheory.IsSFiniteKernel κ] → [ProbabilityTheory.IsSFiniteKernel η] → ProbabilityTheory.Kernel α γ
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZif.mk.inj : ∀ {v1 : Std.Time.TimeZone.TZif.TZifV1} {v2 : Option Std.Time.TimeZone.TZif.TZifV2}
  {v1_1 : Std.Time.TimeZone.TZif.TZifV1} {v2_1 : Option Std.Time.TimeZone.TZif.TZifV2},
  { v1 := v1, v2 := v2 } = { v1 := v1_1, v2 := v2_1 } → v1 = v1_1 ∧ v2 = v2_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
/-- **Alias** of `MeasureTheory.memLp_finsetSum`. -/
MeasureTheory.memLp_finset_sum : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) → MeasureTheory.MemLp (fun a => ∑ i ∈ s, f i a) p μ
-- Mathlib.Algebra.Group.Prod
Prod.instGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Prod.instGroup = { toDivInvMonoid := Prod.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- Given an element `m` of a presheaf of modules `M`, this is the associated
canonical section of the presheaf `M.freeYonedaCoproduct` over the object `m.1`.  -/
PresheafOfModules.freeYonedaCoproductMk : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → (m : M.Elements) → ↑(M.freeYonedaCoproduct.obj m.fst)
-- Mathlib.Data.NNReal.Defs
/-- The absolute value on `ℝ` as a map to `ℝ≥0`.  -/
Real.nnabs : ℝ →*₀ NNReal
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.toLaxMonoidal_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D),
  Function.Injective (@CategoryTheory.Functor.Monoidal.toLaxMonoidal C inst inst_1 D inst_2 inst_3 F)
-- Init.Core
/-- Heterogeneous equality is symmetric.  -/
HEq.symm : ∀ {α β : Sort u} {a : α} {b : β}, a ≍ b → b ≍ a
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_norm : ∀ {R : Type u_4} [inst : SeminormedAddCommGroup R], IsUltrametricDist R ↔ IsNonarchimedean fun x => ‖x‖