mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_def : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G),
  ⁅H₁, H₂⁆ = AddSubgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.gaussNorm_zero : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ), v 0 = 0 → PowerSeries.gaussNorm v c 0 = 0
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.failure.sizeOf_spec : ∀ (ts : List Lean.Expr), sizeOf (Mathlib.Tactic.Choose.ElimStatus.failure ts) = 1 + sizeOf ts
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- A single-point face equals the 0-simplex constructed with
`mkOfPoint`.  -/
Affine.Simplex.face_eq_mkOfPoint : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.face ⋯ = Affine.Simplex.mkOfPoint k (s.points i)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.ext : ∀ {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} {x y : F.Monoidal},
  CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F →
    CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F →
      CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F →
        CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F → x = y
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- Converts an element of `R` to an element of `WithAbs v`.  -/
WithAbs.toAbs : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → R → WithAbs v
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGTD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Init.Data.SInt.Lemmas
ISize.toInt32_neg : ∀ (x : ISize), (-x).toInt32 = -x.toInt32
-- Mathlib.CategoryTheory.Limits.Lattice
/-- A finite product in the category of a `SemilatticeInf` with `OrderTop` is the same as the infimum.
 -/
CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {ι : Type u} [inst_2 : Fintype ι] (f : ι → α),
  ∏ᶜ f = Finset.univ.inf f
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_ae_eq_condExpL1 : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀) [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] (f : α → E),
  μ[f | m] =ᵐ[μ] ↑↑(MeasureTheory.condExpL1 hm μ f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k k_1 : α),
  k = k_1 →
    ∀ (f f_1 : Option β → Option β),
      f = f_1 →
        ∀ (t : Std.DTreeMap.Internal.Impl α fun x => β) (hl : t.Balanced),
          Std.DTreeMap.Internal.Impl.Const.alter k f t hl = Std.DTreeMap.Internal.Impl.Const.alter k_1 f_1 t hl
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Biproducts are unique up to isomorphism. This already follows because bilimits are limits,
but in the case of biproducts we can give an isomorphism with particularly nice definitional
properties, namely that `biproduct.lift b.π` and `biproduct.desc b.ι` are inverses of each
other.  -/
CategoryTheory.Limits.biproduct.uniqueUpToIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            {b : CategoryTheory.Limits.Bicone f} → b.IsBilimit → (b.pt ≅ ⨁ f)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instMonoInl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y], CategoryTheory.Mono (CategoryTheory.Limits.prod.inl X Y)
-- Aesop.Script.GoalWithMVars
Aesop.instReprGoalWithMVars : Repr Aesop.GoalWithMVars
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- If a set is disjoint from its translates by infinitely many bounded vectors, then it has measure
zero.  -/
MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E),
  Bornology.IsBounded (Set.range u) → Pairwise (Function.onFun Disjoint fun n => {u n} + s) → MeasurableSet s → μ s = 0
-- Init.Data.List.Lemmas
List.getElem_cons : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α} (w : i < (a :: l).length), (a :: l)[i] = if h : i = 0 then a else l[i - 1]
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.isIdempotentElem_map_one_iff : ∀ {R : Type u_1} [inst : Semiring R] {f : Module.End R R}, IsIdempotentElem (f 1) ↔ IsIdempotentElem f
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)}
  [IsCancelVAdd G P], (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State : Type
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_refl : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), f =Θ[l] f
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.mk.sizeOf_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} [inst_1 : SizeOf K]
  (toSolution' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  (hab :
    (hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ toSolution' + FermatLastTheoremForThreeGen.Solution'.b✝ toSolution'),
  sizeOf { toSolution' := toSolution', hab := hab } = 1 + sizeOf toSolution' + sizeOf hab
-- Batteries.Data.List.Basic
/-- Auxiliary for `mapDiagM`: `mapDiagM.go as f acc = (acc.toList ++ ·) <$> mapDiagM f as`  -/
List.mapDiagM.go : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → α → m β) → List α → Array β → m (List β)
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.BitVec.bne_to_beq : ∀ {w : ℕ} (a b : BitVec w), (a != b) = !a == b
-- Std.Async.Signal
Std.Async.Signal.sigalrm.sizeOf_spec : sizeOf Std.Async.Signal.sigalrm = 1
-- Mathlib.FieldTheory.LinearDisjoint
/-- Similar to `IntermediateField.LinearDisjoint.of_le` but this is for abstract fields.  -/
IntermediateField.LinearDisjoint.of_le' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E]
  {A' : IntermediateField F E},
  A.LinearDisjoint L →
    A' ≤ A →
      ∀ (L' : Type u_1) [inst_7 : Field L'] [inst_8 : Algebra F L'] [inst_9 : Algebra L' L] [IsScalarTower F L' L]
        [inst_11 : Algebra L' E] [inst_12 : IsScalarTower F L' E] [IsScalarTower L' L E], A'.LinearDisjoint L'
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.ne_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M}, S.IsPrimary → S ≠ ⊤
-- Mathlib.Tactic.CrossRefAttribute
/-- The `#wikidata_tags` command retrieves all declarations that have the `wikidata` attribute.

For each found declaration, it prints a line
```
'declaration_name' corresponds to tag 'declaration_tag'.
```
The variant `#wikidata_tags!` also adds the theorem statement (for theorems)
or declaration type (for definitions, structures, instances, etc.) after each summary line.
 -/
Mathlib.CrossRef.wikidataTags : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_sum_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α ⊕ β)},
  MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instRxiHasSize_eq : Int16.instRxiHasSize = HasModel.instRxiHasSize✝
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f = g` on some neighbourhood of `x`,
then `f` is a submersion at `x` if and only if `g` is a submersion at `x`.  -/
Manifold.IsSubmersionAt.congr_iff : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N}
  {x : M}, f =ᶠ[nhds x] g → (Manifold.IsSubmersionAt I J n f x ↔ Manifold.IsSubmersionAt I J n g x)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.inner_ortho_nonneg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 → ‖y‖ = 1 → 0 ≤ inner ℝ x (InnerProductGeometry.ortho✝ y x)
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.alts.inj : ∀ {ref : Lean.Syntax} {a : List Lean.Elab.Tactic.RCases.RCasesPatt} {ref_1 : Lean.Syntax}
  {a_1 : List Lean.Elab.Tactic.RCases.RCasesPatt},
  Lean.Elab.Tactic.RCases.RCasesPatt.alts ref a = Lean.Elab.Tactic.RCases.RCasesPatt.alts ref_1 a_1 →
    ref = ref_1 ∧ a = a_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.canonical_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.LeftHomologyData.canonical S).i = S.iCycles
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_mul_left_right : ∀ (m n k : ℕ), m.lcm n ∣ m.lcm (k * n)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.nonempty : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ], Nonempty J
-- Mathlib.Algebra.Order.GroupWithZero.Basic
neg_iff_neg_of_mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α] [MulPosMono α],
  0 < a * b → (a < 0 ↔ b < 0)
-- Mathlib.Order.IsNormal
Order.IsNormal.iSup_iterate_mem_fixedPoints : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [WellFoundedLT α] {f : α → α} (a : α),
  Order.IsNormal f → BddAbove (Set.range fun n => f^[n] a) → ⨆ n, f^[n] a ∈ Function.fixedPoints f
-- Init.Data.UInt.Lemmas
USize.add_comm : ∀ (a b : USize), a + b = b + a
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_induction : ∀ {α : Type u_1} (C : Set (Set α)) (p : (s : Set α) → MeasurableSet s → Prop),
  (∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht) →
    p ∅ ⋯ →
      (∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯) →
        (∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯) →
          ∀ (s : Set α) (hs : MeasurableSet s), p s hs
-- Std.Internal.Do.WP.Basic
/-- Soundness for `EStateM`: if `wp prog P s` holds, then `P` holds of `(prog.run s)`.  -/
Std.Internal.Do.EStateM.of_wp_run_eq : ∀ {ε σ α : Type} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} {s : σ},
  prog.run s = x →
    ∀ (P : EStateM.Result ε σ α → Prop),
      Std.Internal.Do.wp prog (fun a s' => P (EStateM.Result.ok a s')) (fun e s' => P (EStateM.Result.error e s')) s →
        P x
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x c₁) = 1 + sizeOf x + sizeOf c₁
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.ker_comp : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) {E : Type u_2} [inst_2 : CategoryTheory.Groupoid E] (ψ : CategoryTheory.Functor D E),
  CategoryTheory.Subgroupoid.ker (φ.comp ψ) = CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.ker ψ)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  (μ : MeasureTheory.Measure α) [Countable G] {s t : Set α} [MeasureTheory.VAddInvariantMeasure G α μ]
  [MeasurableConstVAdd G α],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s) =
        MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict t)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.log_lt_log : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] {x y : WithZero (Multiplicative G)},
  x ≠ 0 → y ≠ 0 → (x.log < y.log ↔ x < y)
-- Mathlib.Tactic.TypeStar
/-- The syntax `variable (X Y ... Z : Type*)` creates a new distinct implicit universe variable
`> 0` for each variable in the sequence.  -/
Lean.Elab.Term.«termType*» : Lean.ParserDescr
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- Generalized version of `bind` allowing `f` to only be defined on the support of `p`.
`p.bind f` is equivalent to `p.bindOnSupport (fun a _ ↦ f a)`, see `bindOnSupport_eq_bind`.  -/
PMF.bindOnSupport : {α : Type u_1} → {β : Type u_2} → (p : PMF α) → ((a : α) → a ∈ p.support → PMF β) → PMF β
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Cache of expressions that have been visited, and their reflection as a linear combination.
 -/
Lean.Elab.Tactic.Omega.Cache : Type
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instVAddAssocClassSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd α β]
  [inst_2 : VAdd M' α] [inst_3 : VAdd M' β] [VAddAssocClass M' α β], VAddAssocClass (↥s) α β
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.refl : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.Commensurable H
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_map_map : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : E →ₐ[F] L),
  (IntermediateField.map f A).relrank (IntermediateField.map f B) = A.relrank B
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_scale : ∀ (x : ONote) [x.NF] (o : ONote) [o.NF], (x.scale o).NF
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.tower_bot : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B)
  (p : Ideal A) [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P], P.LiesOver p
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.metadataBlock.closer : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Topology.Inseparable
Relation.Fibration.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β),
  Relation.Fibration rα rβ f = ∀ ⦃a : α⦄ ⦃b : β⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b
-- Init.Data.SInt.Lemmas
Int64.toNat_toBitVec : ∀ (x : Int64), x.toBitVec.toNat = x.toUInt64.toNat
-- Mathlib.GroupTheory.Index
AddAction.index_stabilizer : ∀ (G : Type u_1) {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X),
  (AddAction.stabilizer G x).index = (AddAction.orbit G x).ncard
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.apply_eq_zero_of_comp_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : Q ⟶ R)
  (a : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp a f = 0 →
    CategoryTheory.Abelian.Pseudoelement.pseudoApply f
        (Quot.mk (CategoryTheory.Abelian.PseudoEqual Q) (CategoryTheory.Over.mk a)) =
      0
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallyInjective_whisker_iff : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA],
  CategoryTheory.CoverPreserving J K H →
    ∀ [H.IsCocontinuous J K] [H.IsCoverDense K],
      CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f) ↔ CategoryTheory.Presheaf.IsLocallyInjective K f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_iff_ne_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isSome = true ↔ t ≠ ∅
-- Mathlib.LinearAlgebra.Pi
Submodule.biInf_comap_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)},
  ⨅ i ∈ I, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi I p
-- Mathlib.Algebra.Ring.Commute
Commute.neg_left : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute (-a) b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, dist f g = sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C}
-- Mathlib.Topology.FiberBundle.Basic
PartialEquiv.symm.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β),
  e.symm =
    { toFun := e.invFun, invFun := ↑e, source := e.target, target := e.source, map_source' := ⋯, map_target' := ⋯,
      left_inv' := ⋯, right_inv' := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.div` -/
TendstoLocallyUniformlyOn.fun_div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 / G i i_1) (fun i => f i / g i) l s
-- Mathlib.Algebra.Group.End
/-- `Equiv.Perm.subtypeCongr` as a `MonoidHom`.  -/
Equiv.Perm.subtypeCongrHom : {α : Type u_4} → (p : α → Prop) → [DecidablePred p] → Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a } →* Equiv.Perm α
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Affine isomorphisms between the domains and codomains of two spaces of affine maps give an
affine isomorphism between the two function spaces.

See also `AffineEquiv.arrowCongrEquiv` and `AffineEquiv.arrowCongrₗ`.  -/
AffineEquiv.arrowCongr : {P₁ : Type u_2} →
  {P₂ : Type u_3} →
    {P₃ : Type u_4} →
      {P₄ : Type u_5} →
        {V₁ : Type u_6} →
          {V₂ : Type u_7} →
            {V₃ : Type u_8} →
              {V₄ : Type u_9} →
                [inst : AddCommGroup V₁] →
                  [inst_1 : AddCommGroup V₂] →
                    [inst_2 : AddCommGroup V₃] →
                      [inst_3 : AddCommGroup V₄] →
                        [inst_4 : AddTorsor V₁ P₁] →
                          [inst_5 : AddTorsor V₂ P₂] →
                            [inst_6 : AddTorsor V₃ P₃] →
                              [inst_7 : AddTorsor V₄ P₄] →
                                {R : Type u_10} →
                                  [inst_8 : CommRing R] →
                                    [inst_9 : Module R V₁] →
                                      [inst_10 : Module R V₂] →
                                        [inst_11 : Module R V₃] →
                                          [inst_12 : Module R V₄] →
                                            (P₁ ≃ᵃ[R] P₂) → (P₃ ≃ᵃ[R] P₄) → (P₁ →ᵃ[R] P₃) ≃ᵃ[R] P₂ →ᵃ[R] P₄
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.toRegularMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Adhesive C],
  CategoryTheory.IsRegularMonoCategory C
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- If `G` is a ring object, then `Hom(X, G)` has a ring structure.  -/
CategoryTheory.Hom.ring : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → {R : C} → [CategoryTheory.RingObj R] → {X : C} → Ring (X ⟶ R)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
eq_affineCombination_of_mem_affineSpan_of_fintype : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p1 : P} {p : ι → P},
  p1 ∈ affineSpan k (Set.range p) → ∃ w, ∑ i, w i = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (G : C)
  (x : (CategoryTheory.End G)ᵐᵒᵖ),
  (CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite G).symm x =
    match x with
    | { unop' := f } => f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Product of subsemirings is isomorphic to their product as monoids.  -/
Subsemiring.prodEquiv : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] → (s : Subsemiring R) → (t : Subsemiring S) → ↥(s.prod t) ≃+* ↥s × ↥t
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_inj : ∀ {α : Type u_1} {p q : PMF α}, p.toOuterMeasure = q.toOuterMeasure ↔ p = q
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.isBigO_psi_sub_theta_sqrt : (Chebyshev.psi - Chebyshev.theta) =O[Filter.atTop] Real.sqrt
-- Std.Time.Format.Modifier
/-- `H`: Hour of day (0-23) (e.g., 0).
 -/
Std.Time.Modifier.H : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal'` as an `AddMonoidHom`.  -/
Matrix.blockDiagonal'AddMonoidHom : {o : Type u_4} →
  (m' : o → Type u_7) →
    (n' : o → Type u_8) →
      (α : Type u_12) →
        [DecidableEq o] →
          [inst : AddZeroClass α] → ((i : o) → Matrix (m' i) (n' i) α) →+ Matrix ((i : o) × m' i) ((i : o) × n' i) α
-- Mathlib.Analysis.CStarAlgebra.Basic
Metric.star_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x : E) (r : ℝ),
  star (Metric.closedBall x r) = Metric.closedBall (star x) r
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.instDecidableLE : DecidableLE BoxIntegral.IntegrationParams