mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The type of continuous monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousMonoidHom A B)`,
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F)`.

When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `MonoidHomClass`, if needed.  -/
ContinuousMonoidHom : (A : Type u_2) →
  (B : Type u_3) → [Monoid A] → [Monoid B] → [TopologicalSpace A] → [TopologicalSpace B] → Type (max u_2 u_3)
-- Std.Data.ExtDHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDHashMap.getKeyD : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → α → α → α
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_inv_eq_mul_inv_iff : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a b c d : α}, IsUnit b → IsUnit d → (a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b)
-- Mathlib.Analysis.Matrix.LDL
/-- **LDL decomposition**: any positive definite matrix `S` can be
decomposed as `S = LDLᴴ` where `L` is a lower-triangular matrix and `D` is a diagonal matrix.  -/
LDL.lower_conj_diag : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.lower hS * LDL.diag hS * (LDL.lower hS).conjTranspose = S
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.mk_injective : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] (s : Finset ι),
  Function.Injective ⇑(DirectSum.mk β s)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.toConvexCone_injective : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E], Function.Injective PointedCone.toConvexCone
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_comp_d₂₁_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G × G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) x) =
    0
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear maps.  -/
ContDiffWithinAt.laplacianWithin_CLM_comp_left : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} {s : Set E} {l : F →L[ℝ] G},
  ContDiffWithinAt ℝ 2 f s x →
    UniqueDiffOn ℝ s →
      x ∈ s → InnerProductSpace.laplacianWithin (⇑l ∘ f) s x = (⇑l ∘ InnerProductSpace.laplacianWithin f s) x
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_self_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⁅H, H⁆ = ⊥ ↔ IsAddCommutative ↥H
-- Mathlib.RingTheory.Extension.Basic
/-- The action of `R₀` on `P.Cotangent` for an extension `P → S`, if `S` is an `R₀` algebra.  -/
Algebra.Extension.Cotangent.val_smul''' : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ S] (r : R₀) (x : P.Cotangent),
  (r • x).val = P.σ ((algebraMap R₀ S) r) • x.val
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.continuousOn_prod_circle_transform_function : ∀ {R r : ℝ},
  r < R → ∀ {z : ℂ}, ContinuousOn (fun w => (circleMap z R w.2 - w.1)⁻¹ ^ 2) (Metric.closedBall z r ×ˢ Set.univ)
-- Mathlib.Data.Nat.Dist
Nat.dist_tri_right : ∀ (n m : ℕ), m ≤ n + n.dist m
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.instNonemptyStrictMap : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) [P.Nonempty], (P.strictMap F).Nonempty
-- Mathlib.Data.List.TFAE
/-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∃ x, P₁ x) ↔ ... ↔ (∃ x, Pₙ x)`.
Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list
`[(∃ x, P₁ x), ..., (∃ x, Pₙ x)]`, but simply providing a list of underscores with the right
length makes it happier.

Example:
```lean
example (P₁ P₂ P₃ : ℕ → Prop) (H : ∀ n, [P₁ n, P₂ n, P₃ n].TFAE) :
    [∃ n, P₁ n, ∃ n, P₂ n, ∃ n, P₃ n].TFAE :=
  exists_tfae [_, _, _] H
```
 -/
List.exists_tfae : ∀ {α : Type u_1} (l : List (α → Prop)),
  (∀ (a : α), (List.map (fun p => p a) l).TFAE) → (List.map (fun p => ∃ a, p a) l).TFAE
-- Mathlib.Data.Nat.Init
Nat.rec_zero : ∀ {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)), Nat.rec h0 h 0 = h0
-- Lean.DocString.Types
Lean.Doc.Inline.concat.injEq : ∀ {i : Type u} (content content_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Inline.concat content = Lean.Doc.Inline.concat content_1) = (content = content_1)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
_private.Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps.0.ContinuousMap.Homotopy.start_path : ∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁} {q : Path x₂ x₃},
  (∀ (t : ↑unitInterval), f (p t) = g (q t)) → f x₀ = g x₂
-- Init.Data.Option.Lemmas
Classical.choice.congr_simp : ∀ {α : Sort u} (a : Nonempty α), Classical.choice a = Classical.choice a
-- Mathlib.Data.Finset.Defs
Finset.decidableDExistsFinset : {α : Type u_1} →
  {s : Finset α} →
    {p : (a : α) → a ∈ s → Prop} →
      [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] → Decidable (∃ a, ∃ (h : a ∈ s), p a h)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.mk.injEq : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} (I₀ : Type v)
  (X : I₀ → CommRingCat) (f : (j : I₀) → AlgebraicGeometry.Spec (X j) ⟶ S) (idx : ↥S → I₀)
  (covers : ∀ (x : ↥S), x ∈ Set.range ⇑(f (idx x)))
  (map_prop : autoParam (∀ (j : I₀), P (f j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam) (I₀_1 : Type v)
  (X_1 : I₀_1 → CommRingCat) (f_1 : (j : I₀_1) → AlgebraicGeometry.Spec (X_1 j) ⟶ S) (idx_1 : ↥S → I₀_1)
  (covers_1 : ∀ (x : ↥S), x ∈ Set.range ⇑(f_1 (idx_1 x)))
  (map_prop_1 : autoParam (∀ (j : I₀_1), P (f_1 j)) AlgebraicGeometry.Scheme.AffineCover.map_prop._autoParam),
  ({ I₀ := I₀, X := X, f := f, idx := idx, covers := covers, map_prop := map_prop } =
      { I₀ := I₀_1, X := X_1, f := f_1, idx := idx_1, covers := covers_1, map_prop := map_prop_1 }) =
    (I₀ = I₀_1 ∧ X ≍ X_1 ∧ f ≍ f_1 ∧ idx ≍ idx_1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) {X Y : C} (φ : X ⟶ Y),
  ((t.eTriangleLTGE.obj i).map φ).hom₂ = φ
-- Mathlib.Data.Sign.Defs
SignType.neg_le_neg_iff : ∀ {a b : SignType}, -a ≤ -b ↔ b ≤ a
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      {S : Type u_10} →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : IsTopologicalAddGroup W] →
                            [inst_9 : Semiring S] →
                              [inst_10 : Module S W] →
                                [SMulCommClass R S W] → [ContinuousConstSMul S W] → Module S (P →ᴬ[R] W)
-- Mathlib.Order.Grade
grade_toDual : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α] (a : α),
  grade 𝕆ᵒᵈ (OrderDual.toDual a) = OrderDual.toDual (grade 𝕆 a)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given a cardinal `κ` and a type `X`, this is the subtype of `Set X`
consisting of subsets of `X` of cardinality `< κ`.  -/
CategoryTheory.CardinalDirectedPoset.SetCardinalLT : Cardinal.{u} → Type u → Type (max 0 u)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_tsum : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {x : ℕ → PowerSeries R} {a : MvPowerSeries τ S} [inst_3 : UniformSpace R] [DiscreteUniformity R]
  [inst_5 : UniformSpace S] [DiscreteUniformity S],
  Summable x → PowerSeries.HasSubst a → PowerSeries.subst a (∑' (i : ℕ), x i) = ∑' (i : ℕ), PowerSeries.subst a (x i)
-- Mathlib.Order.Filter.Defs
Filter.ext_iff : ∀ {α : Type u_1} {f g : Filter α}, f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_mul_const_field' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {u : 𝕜 → 𝕜'} (v : 𝕜'), (deriv fun x => u x * v) = fun x => deriv u x * v
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instMul.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Mul γ] [inst_3 : ContinuousMul γ],
  MeasureTheory.AEEqFun.instMul = { mul := MeasureTheory.AEEqFun.comp₂ (fun x1 x2 => x1 * x2) ⋯ }
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2}
  (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (F.whiskerIsoMapGenerateCocone U hY).hom.hom = F.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Order.Floor.Semiring
/-- There exists at most one `FloorSemiring` structure on a linear ordered semiring.  -/
subsingleton_floorSemiring : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R], Subsingleton (FloorSemiring R)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOfEquivOfLe_apply_coe : ∀ {G : Type u_7} [inst : Group G] {H K : Subgroup G} (h : H ≤ K) (g : ↥(H.subgroupOf K)),
  ↑((Subgroup.subgroupOfEquivOfLe h) g) = ↑↑g
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
MulEquiv.symm_apply_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (x : M), e.symm (e x) = x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a
-- Init.Data.UInt.Lemmas
USize.not_lt_zero : ∀ {a : USize}, ¬a < 0
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ioc_update_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : DecidableEq ι] {x y : (i : ι) → α i}
  {i₀ : ι} {m : α i₀},
  x i₀ ≤ m →
    (Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i)) =
      {z | m < z i₀} ∩ Set.univ.pi fun i => Set.Ioc (x i) (y i)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTopCoeff_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (β : LieModule.Weight R L M),
  LieModule.chainTopCoeff 0 β = 0
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instMonoidCoeOfSubmonoidClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)],
  RestrictedProduct.instMonoidCoeOfSubmonoidClass R = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false},
      Std.Internal.List.getKey? (Std.Internal.List.minKey l he) l = some (Std.Internal.List.minKey l he)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkHInjectiveTheorem? : Lean.Name → Lean.ConstructorVal → Lean.MetaM (Option Lean.TheoremVal)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsFiniteKernel.add : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η], ProbabilityTheory.IsFiniteKernel (κ + η)
-- Mathlib.Algebra.Notation.Prod
Prod.inv_mk : ∀ {G : Type u_8} {H : Type u_9} [inst : Inv G] [inst_1 : Inv H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)
-- Mathlib.Order.Bounds.Image
AntitoneOn.image_upperBounds_subset_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  AntitoneOn f t → s ⊆ t → f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)
-- Mathlib.Data.ENNReal.Inv
/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.mul_iInf_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.mul_iInf` for the special case assuming `Nonempty ι`.  -/
ENNReal.mul_iInf' : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal},
  (a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0) → (a = 0 → Nonempty ι) → a * ⨅ i, f i = ⨅ i, a * f i
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  (P.reflectionPerm i).symm = P.reflectionPerm i
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.mk.injEq : ∀ (line : Std.Format) (column : ℕ) (tags : List (ℕ × Std.Format)) (line_1 : Std.Format) (column_1 : ℕ)
  (tags_1 : List (ℕ × Std.Format)),
  ({ line := line, column := column, tags := tags } = { line := line_1, column := column_1, tags := tags_1 }) =
    (line = line_1 ∧ column = column_1 ∧ tags = tags_1)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.intEquivalence_unitIso_hom_app_hom_apply : ∀ (X : AlgCat ℤ) (a : ↑X),
  (AlgCat.Hom.hom (AlgCat.intEquivalence.unitIso.hom.app X)) a =
    { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ } a
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- A property is Zariski-local at source if it is local at source in the Zariski topology.  -/
AlgebraicGeometry.IsZariskiLocalAtSource : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → Prop
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_prodMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β),
  Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (Function.minimalPeriod g x.2)
-- Mathlib.Data.ULift
PLift.map_surjective : ∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Surjective (PLift.map f) ↔ Function.Surjective f
-- Batteries.Recycling.MonadSatisfying.Array
Array.size_mapIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (as : Array α)
  (f : ℕ → α → m β), SatisfiesM (fun arr => arr.size = as.size) (Array.mapIdxM f as)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- A morphism of `1`-hypercovers is a morphism of the underlying pre-`1`-hypercovers.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} → J.OneHypercover S → J.OneHypercover S → Type (max (max w w') v)
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_homCartesianLift : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮}
  (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) {a' : F.CoGrothendieck} {φ' : a' ⟶ { base := S, fiber := a }}
  {g : a'.base ⟶ R}
  [inst_1 :
    (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'],
  (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift g
    (CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift f g φ')
-- Mathlib.Algebra.Lie.Extension
/-- The projection homomorphism `L →ₗ⁅R⁆ M`  -/
LieAlgebra.Extension.proj : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (self : LieAlgebra.Extension R N M) → self.L →ₗ⁅R⁆ M
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is `charFunDual_pi` for `PiLp`.
See `charFunDual_pi` for the Banach space version.  -/
MeasureTheory.charFunDual_pi' : ∀ (p : ENNReal) [inst : Fact (1 ≤ p)] {ι : Type u_4} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {E : ι → Type u_5}
  [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → NormedSpace ℝ (E i)]
  {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (L : StrongDual ℝ (PiLp p E)),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (WithLp.toLp p) (MeasureTheory.Measure.pi μ)) L =
    ∏ i,
      MeasureTheory.charFunDual (μ i)
        (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.rotate_zero : ∀ {G : Type u_2} [inst : Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)),
  Equiv.Perm.VectorsProdEqOne.rotate v 0 = v
-- Mathlib.Data.List.Defs
/-- Greedily create a sublist of `a :: l` such that, for every two adjacent elements `a, b`,
`R a b` holds. Mostly used with ≠; for example, `destutter' (≠) 1 [2, 2, 1, 1] = [1, 2, 1]`,
`destutter' (≠) 1, [2, 3, 3] = [1, 2, 3]`, `destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9]`.  -/
List.destutter' : {α : Type u_1} → (R : α → α → Prop) → [DecidableRel R] → α → List α → List α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_eq_zero_iff : ∀ {θ : Real.Angle}, 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.right_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g), h.right.r = h.r.right
-- Mathlib.RingTheory.PicardGroup
CategoryTheory.toSkeleton.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), CategoryTheory.toSkeleton X = ⟦X⟧
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limCompFlipIsoWhiskerLim_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X_1).hom
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).hom
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mdifferentiableAt_mulInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G]
  [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] (v : GroupLieAlgebra I G) {g : G},
  (MDiffAt fun g => ⟨g, mulInvariantVectorField v g⟩) g
-- Mathlib.MeasureTheory.Order.Lattice
OrderDual.instMeasurableSup₂ : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Min M] [MeasurableInf₂ M], MeasurableSup₂ Mᵒᵈ
-- Mathlib.GroupTheory.Transfer
Subgroup.leftTransversals.diff_mul_diff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (R S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  Subgroup.leftTransversals.diff ϕ R S * Subgroup.leftTransversals.diff ϕ S T = Subgroup.leftTransversals.diff ϕ R T
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.nat_lt_continuum : ∀ (n : ℕ), ↑n < Cardinal.continuum
-- Mathlib.Order.Filter.Lift
Filter.lift_const : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, (f.lift fun x => g) = g
-- Lean.Parser.Do
Lean.Parser.Term.doIfLet.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_of_infinite : ∀ (R A : Type u) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A] [Infinite R], Cardinal.mk { x // IsAlgebraic R x } = Cardinal.mk R
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.id`.

---

The identity morphism on a module object.  -/
CategoryTheory.Mod_.id : {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.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → (M : CategoryTheory.Mod D A) → M.Hom M
-- Init.Data.String.Basic
String.ofList_append : ∀ {l₁ l₂ : List Char}, String.ofList (l₁ ++ l₂) = String.ofList l₁ ++ String.ofList l₂
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.yang_baxter_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator Y X Z ≪≫
          CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z) ≪≫
            (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).symm ≪≫
              CategoryTheory.MonoidalCategory.whiskerRightIso (β_ Y Z) X ≪≫
                CategoryTheory.MonoidalCategoryStruct.associator Z Y X =
    CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫
      (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).symm ≪≫
        CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y ≪≫
          CategoryTheory.MonoidalCategoryStruct.associator Z X Y ≪≫
            CategoryTheory.MonoidalCategory.whiskerLeftIso Z (β_ X Y)