mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAgainstOfIsStableUnderCobaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderCobaseChange] (P' : CategoryTheory.MorphismProperty C), P.IsStableUnderCobaseChangeAgainst P'
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.continuousLinearEquivalence_comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : TopologicalSpace F'] [inst_8 : AddCommMonoid F'] [inst_9 : Module R F']
  {f : E →L[R] F} {g : F ≃L[R] F'}, f.HasLeftInverse → (↑g ∘SL f).HasLeftInverse
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber_d : ∀ {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 : ι),
  (HomologicalComplex.homotopyCofiber φ).d i j = HomologicalComplex.homotopyCofiber.d φ i j
-- Lean.Environment
/-- Kernel isDefEq predicate. We use it mainly for debugging purposes.
Recall that the kernel type checker does not support metavariables.
When implementing automation, consider using the `MetaM` methods.  -/
Lean.Kernel.isDefEq : Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Except Lean.Kernel.Exception Bool
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.mk : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G},
  (x₁, y₁) ∈ A → (x₁, y₂) ∈ A → (x₂, y₁) ∈ A → x₁ + y₂ = x₂ + y₁ → IsCorner A x₁ y₁ x₂ y₂
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.lt_pred : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  Order.IsPredLimit b → b < a → b < Order.pred a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.SimpleFunc.dite.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (s : Set α) (hs : MeasurableSet s)
  (f f_1 : MeasureTheory.SimpleFunc (↑s) β),
  f = f_1 →
    ∀ (g g_1 : MeasureTheory.SimpleFunc (↑sᶜ) β),
      g = g_1 → MeasureTheory.SimpleFunc.dite s hs f g = MeasureTheory.SimpleFunc.dite s hs f_1 g_1
-- Mathlib.Analysis.SpecificLimits.Basic
hasSum_geometric_two' : ∀ (a : ℝ), HasSum (fun n => a / 2 / 2 ^ n) a
-- Std.Http.Data.URI.Encoding
/-- Checks if a byte is valid in a percent-encoded query string component. Extends `isEncodedChar` to also
allow '+' which represents space in application/x-www-form-urlencoded format.
 -/
Std.Http.URI.isEncodedQueryChar : (UInt8 → Bool) → UInt8 → Bool
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.instFunLike : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → (S : GroupExtension N E G) → FunLike S.Section G E
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.lift'_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] (f : α →* β) (x : α),
  (WithZero.lift' f) ↑x = f x
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_of_preservesPullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {E : CategoryTheory.PreOneHypercover X} (F : CategoryTheory.Functor C D) {W : C} {i₁ i₂ : E.I₀}
  (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂),
  CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂) →
    ∀ [CategoryTheory.Limits.HasPullbacks C]
      [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
      CategoryTheory.Sieve.functorPushforward F (E.sieve₁ p₁ p₂) = (E.map F).sieve₁ (F.map p₁) (F.map p₂)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow
`star ⟶ of [0]`.  -/
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.comp
        CategoryTheory.CosimplicialObject.Augmented.toArrow ≅
      (CategoryTheory.Functor.mapArrowFunctor AugmentedSimplexCategory C).comp
        ((CategoryTheory.evaluation (CategoryTheory.Arrow AugmentedSimplexCategory) (CategoryTheory.Arrow C)).obj
          (CategoryTheory.Arrow.mk (CategoryTheory.WithInitial.homTo { len := 0 })))
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then any `R`-basis of `A` is also a `B`-basis of `S`.
 -/
Subalgebra.LinearDisjoint.basisOfBasisLeft : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {A B : Subalgebra R S} →
            A.LinearDisjoint B → A ⊔ B = ⊤ → {ι : Type u_1} → Module.Basis ι R ↥A → Module.Basis ι (↥B) S
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.isRegular : ∀ {R : Type u_1} [inst : Ring R] {p : Polynomial R}, p.Monic → IsRegular p
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn.visit.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [inst : Monad m] (f : α → σ → m (ForInStep σ))
  (a : RBTree.RBNode α) (a_1 : σ),
  RBTree.RBNode.forIn.visit f a a_1 =
    match a, a_1 with
    | RBTree.RBNode.nil, b => pure (ForInStep.yield b)
    | RBTree.RBNode.node c l v r, b =>
      ForInStep.bindM (RBTree.RBNode.forIn.visit f l b) fun b =>
        ForInStep.bindM (f v b) fun x => RBTree.RBNode.forIn.visit f r x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_monomial_eq : ∀ {R : Type u} [inst : Semiring R] (i : ℕ) {r : R}, r ≠ 0 → ((Polynomial.monomial i) r).natDegree = i
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.depthLt.inj : ∀ {lhs n lhs_1 n_1 : ℕ},
  Lean.Meta.Grind.EMatchTheoremConstraint.depthLt lhs n = Lean.Meta.Grind.EMatchTheoremConstraint.depthLt lhs_1 n_1 →
    lhs = lhs_1 ∧ n = n_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniform inducing is a uniform inducing for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is a uniform inducing, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform inducing.  -/
UniformOnFun.postcomp_isUniformInducing : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : UniformSpace γ]
  {f : γ → β},
  IsUniformInducing f → IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- **Alias** of the reverse direction of `Matrix.nonsingular_transpose_iff`. -/
Matrix.Nonsingular.transpose : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A : Matrix n n R}, A.Nonsingular → A.transpose.Nonsingular
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj_counit_app : ∀ (D : Type u) [inst : CategoryTheory.Category.{max u v, u} D],
  CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of D) = (CategoryTheory.Cat.FreeRefl.lift (𝟭rq D)).toCatHom
-- Mathlib.Data.Fin.Fin2
Fin2.instFintype : (n : ℕ) → Fintype (Fin2 n)
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.comp_right : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
  {g : ι → β} {s : Set ι}, AntivaryOn f g s → ∀ (k : ι' → ι), AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)
-- Mathlib.Data.Nat.Count
Nat.count_add : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (a b : ℕ),
  Nat.count p (a + b) = Nat.count p a + Nat.count (fun k => p (a + k)) b
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opFunctorCompOpFunctorIso_hom_app_app_hom_apply : ∀ (X : SSet) (X_1 : SimplexCategoryᵒᵖ) (x : (SSet.opFunctor.obj (SSet.opFunctor.obj X)).obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((SSet.opFunctorCompOpFunctorIso.hom.app X).app X_1)) x =
    SSet.opObjEquiv (SSet.opObjEquiv x)
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im z ≤ ‖z‖
-- Mathlib.Data.Fintype.Perm
mem_perms_of_finset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {f : Equiv.Perm α},
  f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop_unmop : ∀ {C : Type u₁} (X : Cᴹᵒᵖ), { unmop := X.unmop } = X
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.toLawson_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithLawson.toLawson a = Topology.WithLawson.toLawson b ↔ a = b
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.of_unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W.unop.ContainsIdentities], W.ContainsIdentities
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R], IsJacobsonRing R → IsJacobsonRing (Polynomial R)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCancelMonoid (f i)] → AddCancelMonoid ((i : I) → f i)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_neg_iff : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {f : α → E}, MeasureTheory.IntegrableAtFilter (-f) l μ ↔ MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y}
  [self : P.IsStableUnderCobaseChangeAlong f] {Z W : C} {f' : Z ⟶ W} {g' : Y ⟶ W} {g : X ⟶ Z},
  CategoryTheory.IsPushout f g g' f' → P g → P g'
-- Mathlib.FieldTheory.SeparableClosure
/-- `F(S) / F` is a separable extension if and only if all elements of `S` are
separable elements.  -/
IntermediateField.isSeparable_adjoin_iff_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  Algebra.IsSeparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, IsSeparable F x
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- Extension for the `positivity` tactic: `Real.log` of a numeric literal.  -/
Mathlib.Meta.Positivity.evalLogNatLit : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Lie.Basic
LieHom.ext : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂}, (∀ (x : L₁), f x = g x) → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.functorExt_hom_app : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C}
  (left :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMulticospan.left i))
  (right :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.right i) ≅
        G.obj (CategoryTheory.Limits.WalkingMulticospan.right i))
  (wl :
    autoParam
      (∀ (i : J.R),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)) (right i).hom =
          CategoryTheory.CategoryStruct.comp (left (J.fst i)).hom
            (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)))
      CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_1)
  (wr :
    autoParam
      (∀ (i : J.R),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)) (right i).hom =
          CategoryTheory.CategoryStruct.comp (left (J.snd i)).hom
            (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)))
      CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_3)
  (X : CategoryTheory.Limits.WalkingMulticospan J),
  (CategoryTheory.Limits.WalkingMulticospan.functorExt left right wl wr).hom.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMulticospan.left i => left i
      | CategoryTheory.Limits.WalkingMulticospan.right i => right i).hom
-- Mathlib.FieldTheory.SeparableClosure
/-- The separable closure in `E` of the separable closure of `F` in `E` is equal to itself.  -/
separableClosure.separableClosure_eq_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  separableClosure (↥(separableClosure F E)) E = ⊥
-- Mathlib.LinearAlgebra.Countable
Finsupp.Uncountable.of_moduleFinite : ∀ {M : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [hM : Uncountable M] [Module.Finite R M], Uncountable R
-- Mathlib.SetTheory.Ordinal.Notation
NONote.cmp_compares : ∀ (a b : NONote), (a.cmp b).Compares a b
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `E / F` is a field extension and `E` is algebraically closed, then the algebraic closure
of `F` in `E` is equal to `F` if and only if `F` is algebraically closed.  -/
IsAlgClosed.algebraicClosure_eq_bot_iff : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsAlgClosed E],
  algebraicClosure F E = ⊥ ↔ IsAlgClosed F
-- Lean.Elab.App
/-- Remaining named arguments to be elaborated.  -/
Lean.Elab.Term.ElabAppArgs.State.namedArgs : Lean.Elab.Term.ElabAppArgs.State → List Lean.Elab.Term.NamedArg
-- Mathlib.RingTheory.Length
Module.length_finsupp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5},
  Module.length R (ι →₀ M) = ENat.card ι * Module.length R M
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.origins : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.PHashSet Lean.Meta.Grind.Origin
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderiv_mem_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set (E →L[𝕜] F)} {x : E},
  fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
-- Init.Data.Array.Extract
Array.extract_replicate : ∀ {α : Type u_1} {a : α} {n i j : ℕ}, (Array.replicate n a).extract i j = Array.replicate (min j n - i) a
-- Mathlib.Algebra.Order.Floor.Div
Pi.instCeilDiv : {ι : Type u_1} →
  {α : Type u_2} →
    {π : ι → Type u_4} →
      [inst : AddCommMonoid α] →
        [inst_1 : PartialOrder α] →
          [inst_2 : (i : ι) → AddCommMonoid (π i)] →
            [inst_3 : (i : ι) → PartialOrder (π i)] →
              [inst_4 : (i : ι) → SMulZeroClass α (π i)] → [(i : ι) → CeilDiv α (π i)] → CeilDiv α ((i : ι) → π i)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E` is a perfect field, then the (relative) perfect closure
`perfectClosure F E` is perfect.  -/
perfectClosure.perfectField : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [PerfectField E],
  PerfectField ↥(perfectClosure F E)
-- Plausible.Testable
Plausible.True.printableProp : Plausible.PrintableProp True
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `CommMonoidWithZero` along an injective function.
See note [reducible non-instances].  -/
Function.Injective.commMonoidWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : CommMonoidWithZero M₀] →
              (f : M₀' → M₀) →
                Function.Injective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀'), f (x * y) = f x * f y) →
                        (∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoidWithZero M₀'
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.topology_eq : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α], inst_1 = Topology.lower α
-- Mathlib.Data.EReal.Basic
EReal.coe_toReal_le : ∀ {x : EReal}, x ≠ ⊥ → ↑x.toReal ≤ x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Comma.mapRight.eq_1 : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right))),
  CategoryTheory.MorphismProperty.Comma.mapRight L r hr =
    CategoryTheory.MorphismProperty.Comma.lift
      ((CategoryTheory.MorphismProperty.Comma.forget L R₁ P Q W).comp (CategoryTheory.Comma.mapRight L r)) hr ⋯ ⋯
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- `Z` is the kernel of `I.cocomplex.X 0 ⟶ I.cocomplex.X 1` when `I : InjectiveResolution Z`.  -/
CategoryTheory.InjectiveResolution.isLimitKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (I : CategoryTheory.InjectiveResolution Z) → CategoryTheory.Limits.IsLimit I.kernelFork
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The `weightedTotalDegree` of the zero polynomial is `⊥`.  -/
MvPolynomial.weightedTotalDegree_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M), MvPolynomial.weightedTotalDegree w 0 = ⊥
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.add_projection_respects_measure : ∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) {U : Set (AddCircle T)},
  MeasurableSet U → MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ioc t (t + T))
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_neg : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (x : CentroidHom α), (-x).toEnd = -x.toEnd
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_inj : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (√x = √y ↔ x = y)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_eq_bot_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {I : Ideal S},
  (Ideal.relNorm R) I = ⊥ ↔ I = ⊥
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_guard : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.findSome? (Option.guard p) = Fin.find? p
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- Given a multiset which sums to `n`, construct a partition of `n` with the same multiset, but
without the zeros.
 -/
Nat.Partition.ofSums : (n : ℕ) → (l : Multiset ℕ) → l.sum = n → n.Partition
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.infsep_anti : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s t : Set α}, s.Nontrivial → s ⊆ t → t.infsep ≤ s.infsep
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.ae_covers : ∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsFundamentalDomain._auto_1},
  MeasureTheory.IsFundamentalDomain G s μ → ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_3.eq_3 : ∀ (motive : Std.HashSet Lean.Syntax.Range → Lean.Syntax → Sort u_1) (curr : Std.HashSet Lean.Syntax.Range)
  (x : Lean.Syntax)
  (h_1 :
    (curr : Std.HashSet Lean.Syntax.Range) →
      (s : Lean.Syntax) →
        (info : Lean.SourceInfo) →
          (kind : Lean.SyntaxNodeKind) →
            (args : Array Lean.Syntax) →
              s = Lean.Syntax.node info kind args → motive curr (Lean.Syntax.node info kind args))
  (h_2 :
    (curr : Std.HashSet Lean.Syntax.Range) → (info : Lean.SourceInfo) → motive curr (Lean.Syntax.atom info "where"))
  (h_3 : (curr : Std.HashSet Lean.Syntax.Range) → (x : Lean.Syntax) → motive curr x),
  (∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
      x = Lean.Syntax.node info kind args → False) →
    (∀ (info : Lean.SourceInfo), x = Lean.Syntax.atom info "where" → False) →
      (match curr, x with
        | curr, s@h:(Lean.Syntax.node info kind args) => h_1 curr s info kind args h
        | curr, Lean.Syntax.atom info "where" => h_2 curr info
        | curr, x => h_3 curr x) =
        h_3 curr x
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} {f : α → β} {g : α → γ},
  Filter.EventuallyConst f l →
    ∀ (op : β → γ → δ), Filter.EventuallyConst g l → Filter.EventuallyConst (fun x => op (f x) (g x)) l
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousLinearMap.isBoundedLinearMap_comp_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F),
  IsBoundedLinearMap 𝕜 fun g => g ∘SL f
-- Mathlib.Topology.Algebra.AsymptoticCone
smul_mem_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} {c : k} {v : V},
  0 ≤ c → v ∈ asymptoticCone k s → c • v ∈ asymptoticCone k s
-- Mathlib.Topology.Piecewise
ContinuousOn.if : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {p : α → Prop} [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ s ∩ frontier {a | p a}, f a = g a) →
    ContinuousOn f (s ∩ closure {a | p a}) →
      ContinuousOn g (s ∩ closure {a | ¬p a}) → ContinuousOn (fun a => if p a then f a else g a) s
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.opOp_symm_apply : ∀ (R : Type u_7) [inst : Add R] [inst_1 : Mul R] (a : Rᵐᵒᵖᵐᵒᵖ),
  (RingEquiv.opOp R).symm a = MulOpposite.unop (MulOpposite.unop a)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.right_le_veblenWith : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (o a : Ordinal.{u}), a ≤ Ordinal.veblenWith f o a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_mk_shrink'' : ∀ (α : Type (max u v)) [inst : Small.{v, max u v} α],
  Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, max u v} α)) = Cardinal.mk α