mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
/-- If a sequence of functions `fₙ` is such that `∑ fₙ (z)` is summable for each `z` in an
open set `s`, and for each `1 ≤ k ≤ m`, the series of `k`-th iterated derivatives
`∑ (iteratedDerivWithin k fₙ s) (z)`
is summable locally uniformly on `s`, and each `fₙ` is `m`-times differentiable, then the `m`-th
iterated derivative of the sum is the sum of the `m`-th iterated derivatives.  -/
iteratedDerivWithin_tsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {s : Set 𝕜} {f : ι → 𝕜 → F} (m : ℕ),
  IsOpen s →
    ∀ {x : 𝕜},
      x ∈ s →
        (∀ t ∈ s, Summable fun n => f n t) →
          (∀ (k : ℕ),
              1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n => iteratedDerivWithin k (fun z => f n z) s) s) →
            (∀ (n : ι) (k : ℕ) (r : 𝕜),
                k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z => f n z) s) r) →
              iteratedDerivWithin m (fun z => ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
-- Init.Prelude
Nat.le_succ_of_le : ∀ {n m : ℕ}, n ≤ m → n ≤ m.succ
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.isTopCompl_iff_isCompl_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E},
  Submodule.IsTopCompl p q ↔ IsCompl p q ∧ IsClosed ↑p ∧ IsClosed ↑q
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.homEquiv.eq_1 : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G},
  Rep.homEquiv = { toFun := Rep.Hom.hom, invFun := Rep.ofHom, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_eq_self_iff : ∀ {α : Type u_1} {M : Matroid α}, M.removeLoops = M ↔ M.Loopless
-- Mathlib.Algebra.Module.SpanRankOperations
Submodule.FG.spanFinrank_baseChange_le : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Submodule R M),
  N.FG → (Submodule.baseChange A N).spanFinrank ≤ N.spanFinrank
-- Mathlib.Algebra.Group.Basic
eq_inv_mul_iff_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = b⁻¹ * c ↔ b * a = c
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj : ∀ {X Y : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).adj =
    (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f.as.unop).toCat
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a finsupp
`x : G →₀ A` satisfying the 1-boundary condition, produces a 1-boundary for the representation
on `A` induced by the `DistribMulAction`.  -/
groupHomology.boundariesOfIsBoundary₁ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              (x : G →₀ A) → groupHomology.IsBoundary₁ x → ↥(groupHomology.boundaries₁ (Rep.ofDistribMulAction k G A))
-- Mathlib.Data.List.DropRight
List.rdropWhile_concat_pos : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α), p x = true → List.rdropWhile p (l ++ [x]) = List.rdropWhile p l
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.unitaryGroup.toLinearEquiv A` is matrix multiplication of vectors by `A`, as a linear
equivalence.  -/
Matrix.UnitaryGroup.toLinearEquiv : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) → (n → α) ≃ₗ[α] n → α
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_eq_one`. -/
SkewMonoidAlgebra.ofFinsupp_eq_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] {a : G →₀ k},
  { coeff := a } = 1 ↔ a = fun₀ | 1 => 1
-- Lean.Util.LeanOptions
Lean.instAppendLeanOptions : Append Lean.LeanOptions
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Raw.Const.toList t)
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_counitIso_hom_app_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A)
  (X_2 : (TopologicalSpace.Opens ↥U)ᵒᵖ),
  (U.sheafEquivOver.counitIso.hom.app X_1).hom.app X_2 = X_1.obj.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.MeasurePreserving.zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [CompactSpace G]
  [DivisibleBy G ℤ] {n : ℤ},
  n ≠ 0 →
    ∀ {X : Type u_2} [inst_8 : MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G},
      MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => n • f x) μ' μ
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding associated to an infinite place extended to an embedding `v.Completion →+* ℂ`.  -/
NumberField.InfinitePlace.Completion.extensionEmbedding : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → v.Completion →+* ℂ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → MDiffAt[s] f₁ x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.map_right : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R),
  (d.map F).right i = F.obj (d.right i)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_zero_injective : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective (Topology.RelCWComplex.openCell 0)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- **Alias** of the forward direction of `Matrix.isDetpBalanced_transpose_iff`. -/
Matrix.IsDetpBalanced.of_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 b : R}, A.transpose.IsDetpBalanced a b → A.IsDetpBalanced a b
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed additive group.  -/
IsUltrametricDist.norm_add_eq_max_of_norm_ne_norm : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] {x y : S}, ‖x‖ ≠ ‖y‖ → ‖x + y‖ = max ‖x‖ ‖y‖
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- Given a t-structure `t` on a pretriangulated category `C`, the property `t.IsLE X n`
holds if `X : C` is `≤ n` for the t-structure.  -/
CategoryTheory.Triangulated.TStructure.IsLE : {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] → CategoryTheory.Triangulated.TStructure C → C → ℤ → Prop
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow.eq_1 : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A) (y : ℝ), CFC.rpow a y = cfc (fun x => x ^ y) a
-- Mathlib.Order.PiLex
Pi.toColex_monotone : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι],
  Monotone ⇑toColex
-- Mathlib.Order.Filter.Basic
Filter.eventually_inf : ∀ {α : Type u} {f g : Filter α} {p : α → Prop}, (∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instAddSubmonoidClass : ∀ (M : Type u_1) [inst : AddZeroClass M], AddSubmonoidClass (SaturatedAddSubmonoid M) M
-- Lean.Meta.AppBuilder
Lean.Meta.mkNoConfusion : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.case : Lean.Name → Lean.IR.VarId → Lean.IR.IRType → Array Lean.IR.Alt → Lean.IR.FnBody
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_lt_of_lt : ∀ {a b c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → a < c → b < c → a + b < c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrp_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.AddGrp C} (ψ : G ⟶ H) (Y : Cᵒᵖ),
  (CategoryTheory.yonedaAddGrp.map ψ).app Y =
    AddGrpCat.ofHom (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMon.map ψ.hom).app Y))
-- Mathlib.LinearAlgebra.Lagrange
/-- The vanishing polynomial on a multiplicative subgroup is of the form X ^ n - 1.  -/
Lagrange.nodal_subgroup_eq_X_pow_card_sub_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (G : Subgroup Rˣ) [inst_2 : Fintype ↥G],
  Lagrange.nodal (↑G).toFinset Units.val = Polynomial.X ^ Fintype.card ↥G - 1
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Given an `R`-algebra `S` and an `S`-algebra `T` with submersive presentations,
this is the canonical submersive presentation of `T` as an `R`-algebra.  -/
Algebra.SubmersivePresentation.comp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                {T : Type u_1} →
                  {ι' : Type u_2} →
                    {σ' : Type u_3} →
                      [inst_4 : CommRing T] →
                        [inst_5 : Algebra R T] →
                          [inst_6 : Algebra S T] →
                            [IsScalarTower R S T] →
                              [inst_8 : Finite σ'] →
                                Algebra.SubmersivePresentation S T ι' σ' →
                                  Algebra.SubmersivePresentation R S ι σ →
                                    Algebra.SubmersivePresentation R T (ι' ⊕ ι) (σ' ⊕ σ)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {s : Subsemiring R}
  {t : Subsemiring S} {p : R × S}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Topology.Algebra.Module.Star
continuous_selfAdjointPart : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A],
  Continuous ⇑(selfAdjointPart R)
-- Init.Data.String.Lemmas.Pattern.Basic
/-- The predicate that says which strings match the pattern.  -/
String.Slice.Pattern.Model.PatternModel.Matches : {ρ : Type} → (pat : ρ) → [self : String.Slice.Pattern.Model.PatternModel pat] → String → Prop
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
Matrix.charpoly_mulVecLin : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  A.mulVecLin.charpoly = A.charpoly
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₂_id : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₅] {σ₂₃ : R₂ →+* R₃}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M]
  [inst_8 : Module R₂ N] [inst_9 : Module R₃ P] [inst_10 : Module R₅ P] [inst_11 : SMulCommClass R₃ R₅ P]
  {σ₁₅ : R →+* R₅} (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P), h.compl₂ LinearMap.id = h
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeightOfEPs.eq_1 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : V → V → R) {i j : V},
  Quiver.Path.addWeightOfEPs w = Quiver.Path.addWeight fun {i j} x => w i j
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β),
  FreeGroup.freeGroupCongr e =
    { toFun := ⇑(FreeGroup.map ⇑e), invFun := ⇑(FreeGroup.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.ready.injEq : ∀ (numCases : ℕ) (isRec tryPostpone : Bool) (numCases_1 : ℕ) (isRec_1 tryPostpone_1 : Bool),
  (Lean.Meta.Grind.SplitStatus.ready numCases isRec tryPostpone =
      Lean.Meta.Grind.SplitStatus.ready numCases_1 isRec_1 tryPostpone_1) =
    (numCases = numCases_1 ∧ isRec = isRec_1 ∧ tryPostpone = tryPostpone_1)
-- Mathlib.RingTheory.PicardGroup
instInvertibleCarrierOutModuleCatValSkeleton : ∀ (R : Type u) [inst : CommRing R] (M : (CategoryTheory.Skeleton (ModuleCat R))ˣ),
  Module.Invertible R ↑(Quotient.out ↑M)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.add_tprodCoeff' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (z₁ z₂ : R) (f : (i : ι) → s i),
  PiTensorProduct.tprodCoeff R z₁ f + PiTensorProduct.tprodCoeff R z₂ f = PiTensorProduct.tprodCoeff R (z₁ + z₂) f
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.finSuccEquiv_comp_C : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ},
  (MvPowerSeries.finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp MvPowerSeries.C) =
    MvPowerSeries.C
-- Mathlib.Geometry.Euclidean.Volume.Measure
Submodule.measurableEquivProd_apply : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : Submodule ℝ V) (p q : P),
  (s.measurableEquivProd p) q = (s.orthogonalProjectionOnto (q -ᵥ p), sᗮ.orthogonalProjectionOnto (q -ᵥ p))
-- Lean.Data.Lsp.Diagnostics
/-- An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property.  -/
Lean.Lsp.DiagnosticWith.relatedInformation? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option (Array Lean.Lsp.DiagnosticRelatedInformation)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c c' : C) (d : D)
  {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxLeftLinear.μₗ F c
            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
          h))
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.projRight_map : ∀ (A : TopCat) (B : TopCat) (x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))))
  (p : x₀ ⟶ x₁), (FundamentalGroupoidFunctor.projRight A B).map p = Path.Homotopic.projRight p
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.hexagon_forward : ∀ {R : Type u} [inst : CommSemiring R] (X Y Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (X.braiding Z).hom))
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelMonoid α],
  Lex.instAddCancelMonoid = { toAddLeftCancelMonoid := Lex.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instOne.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] [inst_3 : One X], OreLocalization.instOne = { one := OreLocalization.one }
-- Lean.Expr
Lean.Expr.instHashable : Hashable Lean.Expr
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- **Alias** of `Subgroup.dense_xor_cyclic`.

---

In a nontrivial densely linear ordered archimedean topological multiplicative group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions, see `Subgroup.dense_or_cyclic` above.  -/
Subgroup.dense_xor'_cyclic : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G),
  Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β},
  (Std.HashMap.filter f m).getD k fallback = (m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R}, W'.Equation ![1, 1, 0]
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.snoc_castSucc : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubAddAction.ofStabilizer G a)) (i : Fin n), (SubAddAction.ofStabilizer.snoc x) i.castSucc = ↑(x i)
-- Mathlib.GroupTheory.Finiteness
/-- A finitely generated submonoid has a minimal generating set.  -/
AddSubmonoid.FG.exists_minimal_closure_eq : ∀ {M : Type u_1} [inst : AddMonoid M] {P : AddSubmonoid M}, P.FG → ∃ S, Minimal (fun S => AddSubmonoid.closure ↑S = P) S
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.forall_relations : ∀ {P : (n : ℕ) → FirstOrder.Language.order.Relations n → Prop},
  (∀ {n : ℕ} (R : FirstOrder.Language.order.Relations n), P n R) ↔ P 2 FirstOrder.Language.orderRel.le
-- Batteries.Data.Array.Match
/-- Iterator transformer for KMP matcher.  -/
Array.Matcher.Iterator : (σ : Type u_1) →
  (n : Type u_1 → Type u_2) → (α : Type u_1) → [BEq α] → Array.Matcher α → [Std.Iterator σ n α] → Type u_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited γ]
  {f : α → β → Option γ} {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.filterMap f m) k =
        ((Std.DHashMap.Internal.Raw₀.Const.get? m k).bind fun x => f k' x).get!
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a non-unital commutative
ring.

See note [reducible non-instances].  -/
NonUnitalAlgebra.adjoinNonUnitalCommRingOfComm : (R : Type u_3) →
  {A : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] →
              {s : Set A} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → NonUnitalCommRing ↥(NonUnitalAlgebra.adjoin R s)
-- Init.Data.Array.Monadic
Array.foldlM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {P : α → Prop} {xs : Array (Subtype P)}
  {f : β → α → m β} {init : β},
  Array.foldlM f init xs.unattach =
    Array.foldlM
      (fun b x =>
        match x with
        | ⟨x, h⟩ => binderNameHint b f (binderNameHint x (f b) (binderNameHint h () (f b (wfParam x)))))
      init xs
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instSub : {𝕜 : 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] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → Sub (ContMDiffSection I F n V)