mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convolution
/-- Approximate `(f ⋆ g) x₀` if the support of the `f` is bounded within a ball, and `g` is near
`g x₀` on a ball with the same radius around `x₀`. See `dist_convolution_le` for a special case.

We can simplify the second argument of `dist` further if we add some extra type-classes on `E`
and `𝕜` or if `L` is scalar multiplication.  -/
MeasureTheory.dist_convolution_le' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G] [μ.IsAddLeftInvariant]
  [MeasureTheory.SFinite μ] {x₀ : G} {R ε : ℝ} {z₀ : E'},
  0 ≤ ε →
    MeasureTheory.Integrable f μ →
      Function.support f ⊆ Metric.ball 0 R →
        MeasureTheory.AEStronglyMeasurable g μ →
          (∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) →
            dist (MeasureTheory.convolution f g L μ x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_submatrix_left : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {l' : Type u_15} {m' : Type u_16} (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (r : l' → l) (c : m' → m),
  Matrix.kroneckerMap f (A.submatrix r c) B = (Matrix.kroneckerMap f A B).submatrix (Prod.map r id) (Prod.map c id)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_inv_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.unop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).hom
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_succ_eq : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {N : ι} {n : ℕ} (ω : Ω),
  MeasureTheory.upperCrossingTime a b f N (n + 1) ω =
    MeasureTheory.hittingBtwn f (Set.Ici b) (MeasureTheory.lowerCrossingTime a b f N n ω) N ω
-- Init.Data.List.Lemmas
List.getLast_cons_cons : ∀ {α : Type u_1} {b a : α} {l : List α}, (a :: b :: l).getLast ⋯ = (b :: l).getLast ⋯
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (f : R →+* S) (x : AddMonoidAlgebra R M) (m : M), ((AddMonoidAlgebra.mapRingHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a diagram
```
a --φ--> b        b'
|        |        |
v        v        v
R --f--> S --g--> S'
```
such that `φ` is strongly co-Cartesian, and a morphism `φ' : a ⟶ b'`. Then `map` is the map
`b ⟶ b'` lying over `g` obtained from the universal property of `φ`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.map : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} →
            {a b : 𝒳} →
              (f : R ⟶ S) →
                (φ : a ⟶ b) →
                  [p.IsStronglyCocartesian f φ] →
                    {S' : 𝒮} →
                      {b' : 𝒳} →
                        {g : S ⟶ S'} →
                          {f' : R ⟶ S'} →
                            f' = CategoryTheory.CategoryStruct.comp f g → (φ' : a ⟶ b') → [p.IsHomLift f' φ'] → b ⟶ b'
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_intCast_iff_of_nonneg : ∀ {z : ℤ}, 0 ≤ z → (Irrational √↑z ↔ ¬IsSquare z)
-- Mathlib.Data.Finset.Union
Finset.subset_biUnion_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] (u : α → Finset β) {x : α},
  x ∈ s → u x ⊆ s.biUnion u
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.cons_not_rev : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeAddGroup.Red.Step ((x, !b) :: (x, b) :: L) L
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any colimit cocone over a pair into a bicone.  -/
CategoryTheory.Limits.BinaryBicone.ofColimitCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} →
          CategoryTheory.Limits.IsColimit t → CategoryTheory.Limits.BinaryBicone X Y
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_two_mul : ∀ (n : ℤ), (2 * n).negOnePow = 1
-- Mathlib.Order.Antichain
IsAntichain.mono_on : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α},
  IsAntichain r₁ s → (s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b) → IsAntichain r₂ s
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3) →
      (x : Option (Λ × Turing.TM0.Stmt Γ)) →
        (Unit → motive none) → ((q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))) → motive x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankFiniteMap : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankFinite] {f : α → β} (hf : Set.InjOn f M.E),
  (M.map f hf).RankFinite
-- Init.Data.Int.Gcd
Int.gcd_le_natAbs_mul : ∀ {a b : ℤ}, a ≠ 0 → b ≠ 0 → a.gcd b ≤ a.natAbs * b.natAbs
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.isOpenMap_iff_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1}
  [inst_3 : AddMonoid H] [inst_4 : TopologicalSpace H] [ContinuousConstVAdd H H] {F : Type u_2} [inst_6 : FunLike F G H]
  [AddMonoidHomClass F G H] {f : F}, IsOpenMap ⇑f ↔ nhds 0 ≤ Filter.map (⇑f) (nhds 0)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {fallback : β} {f : β → β},
  (m.modify k f).getD k' fallback = if (k == k') = true then (Option.map f m[k]?).getD fallback else m.getD k' fallback
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensorAddUnit_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Topology.Order.LeftRightNhds
/-- The set of points which are isolated on the right is countable when the space is
second-countable.  -/
countable_setOfPred_isolated_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | nhdsWithin x (Set.Ioi x) = ⊥}.Countable
-- Init.Internal.Order.Basic
Lean.Order.MonoBind.bind_mono_left : ∀ {m : Type u → Type v} {inst : Bind m} {inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)}
  [self : Lean.Order.MonoBind m] {α β : Type u} {a₁ a₂ : m α} {f : α → m β},
  Lean.Order.PartialOrder.rel a₁ a₂ → Lean.Order.PartialOrder.rel (a₁ >>= f) (a₂ >>= f)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_comp : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  ↑e.symm ∘ₛₗ ↑e = LinearMap.id
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [inst_3 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_pow : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] (m : M) (r : R) (n : ℕ),
  MonoidAlgebra.single m r ^ n = MonoidAlgebra.single (m ^ n) (r ^ n)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectLOfProdMk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))],
  NeZero ((κ.sectL b) a)
-- Mathlib.GroupTheory.Coxeter.Basic
/-- If `p : W → Prop` holds for all simple reflections, it holds for the identity, and it is
preserved under multiplication, then it holds for all elements of `W`.  -/
CoxeterSystem.simple_induction : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : W → Prop} (w : W),
  (∀ (i : B), p (cs.simple i)) → p 1 → (∀ (w w' : W), p w → p w' → p (w * w')) → p w
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_normalizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {g : G},
  g ∈ AddSubgroup.normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g + h + -g ∈ H
-- Lean.Meta.Tactic.Grind.Anchor
/-- Returns the number of digits needed to distinguish the anchors in `es`.

Elements with identical (full) anchors cannot be distinguished by adding more digits.
Thus, they are ignored by this function. Callers must handle these collisions separately
(e.g., the `cases` tactic uses ordinal references such as `#a56e/2`).
 -/
Lean.Meta.Grind.getNumDigitsForAnchors : {α : Type u_1} → [Lean.Meta.Grind.HasAnchor α] → Array α → ℕ
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.mkArgVal : Lean.TSyntax `arg_val → Lean.Doc.DocM Lean.Term
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.of_dist_ne_zero : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v ≠ 0 → G.Reachable u v
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {x : M} {n : WithTop ℕ∞} [Subsingleton M'], ContMDiffWithinAt I I' n f s x
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- Stronger form of `congrLinearEquiv.trans` applying to semilinear maps. Not a simp lemma as
`σ₁₃` and `σ₃₁` cannot be inferred from the LHS.  -/
LinearMap.GeneralLinearGroup.congrLinearEquiv_trans' : ∀ {R₁ : Type u_3} {R₂ : Type u_4} {R₃ : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁}
  [inst_9 : RingHomInvPair σ₁₂ σ₂₁] [inst_10 : RingHomInvPair σ₂₃ σ₃₂] [inst_11 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_12 : RingHomInvPair σ₂₁ σ₁₂] [inst_13 : RingHomInvPair σ₃₂ σ₂₃] [inst_14 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_16 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂)
  (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃),
  (LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂).trans (LinearMap.GeneralLinearGroup.congrLinearEquiv e₂₃) =
    LinearMap.GeneralLinearGroup.congrLinearEquiv (e₁₂.trans e₂₃)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A version of `liftPropWithinAt_indep_chart`, only for the target.  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    f ∈ StructureGroupoid.maximalAtlas M' G' →
      g x ∈ f.source →
        (ChartedSpace.LiftPropWithinAt P g s x ↔
          ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g) s x)
-- Mathlib.Data.EReal.Operations
EReal.neg_add : ∀ {x y : EReal}, x ≠ ⊥ ∨ y ≠ ⊤ → x ≠ ⊤ ∨ y ≠ ⊥ → -(x + y) = -x - y
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_lt_one : ∀ {α : Type u_1} [inst : LT α] {a : α} [inst_1 : One α], ↑a < 1 ↔ a < 1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : SizeOf C] (toHom : E.Hom F.toPreZeroHypercover)
  (s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j))
  (h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k))
  (w₁₁ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam)
  (w₁₂ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam),
  sizeOf { toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ } = 1 + sizeOf toHom
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ ⟶ X₂)
  (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂]
  [inst_5 : X₃.HasTensor Y₃] {Z : CategoryTheory.GradedObject I C}
  (h : CategoryTheory.GradedObject.Monoidal.tensorObj X₃ Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
        (CategoryTheory.CategoryStruct.comp g₁ g₂))
      h
-- Mathlib.RingTheory.WittVector.Defs
WittVector.zero_coeff : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ), WittVector.coeff 0 n = 0
-- Mathlib.Algebra.Algebra.Basic
instSMulCommClass : ∀ {R : Type u_4} {S : Type u_5} {A : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra S A], SMulCommClass R S A
-- Mathlib.Topology.Defs.Sequences
/-- A topological space is called a *Fréchet-Urysohn space*, if the sequential closure of any set
is equal to its closure. Since one of the inclusions is trivial, we require only the non-trivial one
in the definition.  -/
FrechetUrysohnSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.ε_comp_map_ε : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal] [adj.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (G.map (CategoryTheory.Functor.LaxMonoidal.ε F)) =
    adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.GroupTheory.IsSubnormal
/-- Subnormality is transitive.

This version involves an explicit `subtype`; the version `IsSubnormal.trans` does not.  -/
AddSubgroup.IsSubnormal.trans' : ∀ {G : Type u_1} [inst : AddGroup G] {K : AddSubgroup G} {H : AddSubgroup ↥K},
  H.IsSubnormal → K.IsSubnormal → (AddSubgroup.map K.subtype H).IsSubnormal
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).X₃ = CategoryTheory.Limits.cokernel f
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_def : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m),
  (DirichletCharacter.changeLevel hm) χ = MulChar.ofUnitHom ((MulChar.toUnitHom χ).comp (ZMod.unitsMap hm))
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- The canonical functor from `SimplexCategoryGenRel` to SimplexCategory, which exists as the
simplicial identities hold in `SimplexCategory`.  -/
SimplexCategoryGenRel.toSimplexCategory : CategoryTheory.Functor SimplexCategoryGenRel SimplexCategory
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instDecidableEqOfLawfulBEq : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [LawfulBEq α] → [inst_2 : Hashable α] → [inst_3 : BEq β] → [LawfulBEq β] → DecidableEq (Std.ExtHashMap α β)
-- Mathlib.RingTheory.Ideal.Over
Ideal.primesOver.isPrime : ∀ {A : Type u_2} [inst : CommSemiring A] (p : Ideal A) {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B]
  (Q : ↑(p.primesOver B)), (↑Q).IsPrime
-- Batteries.Tactic.Lint.Simp
/-- Add message `msg` to any errors thrown inside `k`.  -/
Batteries.Tactic.Lint.decorateError : {α : Type} → Lean.MessageData → Lean.MetaM α → Lean.MetaM α
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt64
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan
Real.measurable_arctan : Measurable Real.arctan
-- Mathlib.Algebra.Order.Group.Equiv
symm_ofLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], (ofLexAddEquiv α).symm = toLexAddEquiv α
-- Mathlib.Algebra.GCDMonoid.Nat
Int.coe_lcm : ∀ (i j : ℤ), ↑(i.lcm j) = lcm i j
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- [Lemma 3.8](https://ncatlab.org/nlab/show/injective+object#preservation_of_injective_objects)
 -/
CategoryTheory.EnoughInjectives.of_adjunction : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) [L.PreservesMonomorphisms]
  [L.ReflectsMonomorphisms] [CategoryTheory.EnoughInjectives D], CategoryTheory.EnoughInjectives C
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreOneHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (i : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.combine' : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → optParam (Option ℕ) none → Lean.Grind.CommRing.Poly
-- Init.Internal.Order.Basic
Lean.Order.prod_csup_is_sup : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] (c : α ×' β → Prop)
  (hchain : Lean.Order.chain c), Lean.Order.is_sup c (Lean.Order.prod_csup c hchain)
-- Mathlib.LinearAlgebra.Matrix.Bilinear
mulLeftLinearMap.congr_simp : ∀ {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A] (X X_1 : Matrix l m A),
  X = X_1 → mulLeftLinearMap n R X = mulLeftLinearMap n R X_1
-- Mathlib.Algebra.Prime.Lemmas
prime_isUnit_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {x y : M}, IsUnit x → (Prime (x * y) ↔ Prime y)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- A Liouville number is a Liouville number with any real exponent.  -/
Liouville.liouvilleWith : ∀ {x : ℝ}, Liouville x → ∀ (p : ℝ), LiouvilleWith p x
-- Mathlib.Algebra.Algebra.Equiv
/-- See Note [custom simps projection]  -/
AlgEquiv.Simps.apply : {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₂] → (A₁ ≃ₐ[R] A₂) → A₁ → A₂
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.hom_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs : CategoryTheory.Limits.IsColimit s) {W : C} {k l : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l → k = l
-- Mathlib.Order.Bounded
Set.bounded_gt_Icc : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a b : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Icc a b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.baseIso_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.baseIso e).hom = e.hom.base
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (f g : Polynomial R), IsCoprime f g → f.resultant g ≠ 0
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_mod : ∀ (a b : UInt64), a < 256 → b < 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.Topology.Algebra.Constructions
AddUnits.topology_eq_inf : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M],
  AddUnits.instTopologicalSpaceAddUnits =
    TopologicalSpace.induced AddUnits.val inst ⊓ TopologicalSpace.induced (fun u => ↑(-u)) inst
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_add : ∀ {α : Type u_2} [inst : Add α] {s : Set α}, ∅ + s = ∅
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.tobject : Lean.IR.IRType
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.iUnion_inter_closedBall_nat : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α) (x : α), ⋃ n, s ∩ Metric.closedBall x ↑n = s
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_iff_card_mul_and_disjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [Finite G],
  H.IsComplement' K ↔ Nat.card ↥H * Nat.card ↥K = Nat.card G ∧ Disjoint H K
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toMonoidHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], (RingEquiv.refl R).toMonoidHom = MonoidHom.id R