mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.HSpaces
/-- This is the function on p. 475 of [serre1951], defining a homotopy from a path `γ` to the
product path `e ∧ γ`.  -/
Path.delayReflLeft : {X : Type u} → [inst : TopologicalSpace X] → {x y : X} → ↑unitInterval → Path x y → Path x y
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_neg_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {V : (x : M') → TangentSpace I' x}, VectorField.mpullback I I' f (-V) x = -VectorField.mpullback I I' f V x
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
/-- The equivalence from coherent sheaves on `C` to coherent sheaves on `D`, given a fully faithful
functor `F : C ⥤ D` to an extensive preregular category, which preserves and reflects effective
epimorphisms and satisfies `F.EffectivelyEnough`.
 -/
CategoryTheory.coherentTopology.equivalence' : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.PreservesEffectiveEpis] →
            [inst_3 : F.ReflectsEffectiveEpis] →
              [inst_4 : F.Full] →
                [inst_5 : F.Faithful] →
                  [inst_6 : CategoryTheory.FinitaryExtensive D] →
                    [inst_7 : CategoryTheory.Preregular D] →
                      [inst_8 : CategoryTheory.FinitaryPreExtensive C] →
                        [inst_9 : CategoryTheory.Limits.PreservesFiniteCoproducts F] →
                          [inst_10 : F.EffectivelyEnough] →
                            (A : Type u₃) →
                              [inst_11 : CategoryTheory.Category.{v₃, u₃} A] →
                                [∀ (X : Dᵒᵖ),
                                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op)
                                        A] →
                                  CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌
                                    CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A
-- Init.Data.Ord.Basic
Ordering.isGE_iff_eq_gt_or_eq_eq : ∀ {o : Ordering}, o.isGE = true ↔ o = Ordering.gt ∨ o = Ordering.eq
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_subtypeVal : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {C : SubMulAction G X} {B : Set ↥C},
  MulAction.IsBlock G (Subtype.val '' B) ↔ MulAction.IsBlock G B
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.leftUnitor.match_1.eq_2 : ∀ (motive : AugmentedSimplexCategory → Sort u_1)
  (h_1 : (a : SimplexCategory) → motive (CategoryTheory.WithInitial.of a))
  (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Module.Opposite
/-- Like `Semiring.toModule`, but multiplies on the right.  -/
Semiring.toOppositeModule : {R : Type u_1} → [inst : Semiring R] → Module Rᵐᵒᵖ R
-- Mathlib.FieldTheory.SeparableDegree
/-- If `E` and `K` are isomorphic as `F`-algebras, then they have the same `Field.finSepDegree`
over `F`.  -/
Field.finSepDegree_eq_of_equiv : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), Field.finSepDegree F E = Field.finSepDegree F K
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [inst_2 : CategoryTheory.ComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul X) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.comul)
        (CategoryTheory.MonoidalCategoryStruct.associator X X X).inv)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_smul_right : ∀ {R : Type u_1} {α : 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} [inst : SMul R β] [inst_1 : SMul R γ] (f : α → β → γ) (r : R),
  (∀ (a : α) (b : β), f a (r • b) = r • f a b) →
    ∀ (A : Matrix l m α) (B : Matrix n p β), Matrix.kroneckerMap f A (r • B) = r • Matrix.kroneckerMap f A B
-- Init.Prelude
/-- Auxiliary definition for `panic`.  -/
panicCore : {α : Sort u} → [Inhabited α] → String → α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.im_div_exp_dist_le : ∀ (z w : UpperHalfPlane), z.im / Real.exp (dist z w) ≤ w.im
-- Mathlib.Topology.Algebra.Module.LocallyConvex
locallyConvexSpace_iff_exists_convex_subset : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E],
  LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), ∀ U ∈ nhds x, ∃ S ∈ nhds x, Convex 𝕜 S ∧ S ⊆ U
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_span : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), PrimeSpectrum.zeroLocus ↑(Ideal.span s) = PrimeSpectrum.zeroLocus s
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.domRestrict_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {S : Type u_3}
  [inst_2 : SetLike S R] [inst_3 : SubmonoidClass S R] (T : S) (χ : MulChar R R') (x : ↥T),
  (MulChar.domRestrict T χ) x = if IsUnit x then χ ↑x else 0
-- Mathlib.Data.Set.Insert
Set.inter_insert_of_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ s → s ∩ insert a t = s ∩ t
-- Mathlib.Data.Set.Prod
MonotoneOn.set_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [inst : Preorder α] {f : α → Set β} {g : α → Set γ},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x ×ˢ g x) s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s : Finset α), s.preimage (fun x => -x) ⋯ = -s
-- Mathlib.Order.Atoms.Finite
exists_covby_infinite_Ici_of_infinite_Ici : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [IsStronglyAtomic α],
  (Set.Ici a).Infinite → {x | a ⋖ x}.Finite → ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.diagonal_kroneckerTMul_diagonal : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α] [inst_4 : Module R β]
  [inst_5 : DecidableEq m] [inst_6 : DecidableEq n] (a : m → α) (b : n → β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) (Matrix.diagonal b) =
    Matrix.diagonal fun mn => a mn.1 ⊗ₜ[R] b mn.2
-- Mathlib.Topology.MetricSpace.Gluing
/-- A disjoint union of complete metric spaces is complete.  -/
Metric.Sigma.completeSpace : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] [∀ (i : ι), CompleteSpace (E i)],
  CompleteSpace ((i : ι) × E i)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.atomic : Lean.ParseImports.Parser → Lean.ParseImports.Parser
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
backward direction.

If the expression $\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes.
That is, $\sum_i m_i \otimes n_i = 0$.  -/
TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N},
  TensorProduct.VanishesTrivially R m n → ∑ i, m i ⊗ₜ[R] n i = 0
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Salient.anti : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] {C₁ C₂ : ConvexCone R G}, C₂ ≤ C₁ → C₁.Salient → C₂.Salient
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.extract : ∀ {l m r ml mm mr : List Char} {b e : String.Pos.Raw} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s →
    Substring.Raw.ValidFor ml mm mr { str := String.ofList m, startPos := b, stopPos := e } →
      ∃ l' r', Substring.Raw.ValidFor l' mm r' (s.extract b e)
-- Batteries.Data.HashMap.Basic
/-- Converts the map into an array of key-value pairs.
```
open List
(ofList [("one", 1), ("two", 2)]).toArray.data ~ #[("one", 1), ("two", 2)].data
```
 -/
Batteries.HashMap.toArray : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → Array (α × β)
-- Mathlib.Algebra.Star.TensorProduct
TensorProduct.instStarModule : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : AddCommMonoid B]
  [inst_7 : StarAddMonoid B] [inst_8 : Module R B] [inst_9 : StarModule R B], StarModule R (TensorProduct R A B)
-- Aesop.Util.Basic
Aesop.PersistentHashSet.toArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → Array α
-- Init.Data.String.Basic
String.Pos.ne_of_lt : ∀ {s : String} {p q : s.Pos}, p < q → p ≠ q
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.minus.inj : ∀ {v : Lean.Level} {M : Q(Type v)} {iM iM_1 : Q(Field «$M»)},
  Mathlib.Tactic.FieldSimp.Sign.minus iM = Mathlib.Tactic.FieldSimp.Sign.minus iM_1 → iM = iM_1
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_eq_one_iff : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α},
  MulAction.period m a = 1 ↔ m • a = a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builder.sizeOf_spec : ∀ (b : Aesop.Frontend.DBuilderName), sizeOf (Aesop.Frontend.Feature.builder b) = 1 + sizeOf b
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When the second map `S.g` is zero, this is the left homology data on `S` given
by any colimit cokernel cofork of `S.f`  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.g = 0 →
          (c : CategoryTheory.Limits.CokernelCofork S.f) → CategoryTheory.Limits.IsColimit c → S.LeftHomologyData
-- Lean.Meta.Tactic.Refl
/-- Close given goal using `Eq.refl`.

With (`check := false`), the elaborator does not check if the goal is actually a definitionaly
equality.

See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
backs the `rfl` tactic.
 -/
Lean.MVarId.refl : Lean.MVarId → optParam Bool true → Lean.MetaM Unit
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₄.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.u₄✝ S = FermatLastTheoremForThreeGen.Solution.u₄✝ S_1
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mapIso_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (e : A ≅ B),
  (CategoryTheory.MonoOver.mapIso e).unitIso =
    ((CategoryTheory.MonoOver.mapComp e.hom e.inv).symm ≪≫
        CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.MonoOver.mapId A).symm
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.IsPartition ↔ π.iUnion = ↑I
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `NormedAddGroup.nhds_zero_basis_norm_lt`. -/
NormedAddCommGroup.nhds_zero_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
-- Aesop.Forward.State
/-- Inserts a match. The match `m` is associated with the slot given by its
level (i.e., the maximal slot for which `m` contains a hypothesis) and the
instantiation of `var` given by the map's substitution. Returns `true` if the
match was not previously associated with this slot and instantiation.  -/
Aesop.InstMap.insertMatch : Aesop.InstMap → Aesop.PremiseIndex → Aesop.Match → Aesop.BaseM (Aesop.InstMap × Bool)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.hasStrictDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, AnalyticAt 𝕜 f x → HasStrictDerivAt f (deriv f x) x
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.delayedAssignment.sizeOf_spec : ∀ (da : Lean.DelayedMetavarAssignment), sizeOf (Aesop.EqualUpToIds.MVarValue.delayedAssignment da) = 1 + sizeOf da
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {k a : α} {v : β}, (t.insertIfNew k v)[a]! = if cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]!
-- Init.Data.UInt.Lemmas
UInt64.ofNat_mod_size : ∀ {x : ℕ}, UInt64.ofNat (x % 2 ^ 64) = UInt64.ofNat x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- An instance of `CartesianMonoidalCategory C` bundles an explicit choice of a binary
product of two objects of `C`, and a terminal object in `C`.

Users should use the monoidal notation: `X ⊗ Y` for the product and `𝟙_ C` for
the terminal object.
 -/
CategoryTheory.CartesianMonoidalCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Data.Seq.Parallel
Computation.parallel_congr_left : ∀ {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α},
  (∀ s ∈ S, s.Promises a) →
    Stream'.WSeq.LiftRel Computation.Equiv S T → (Computation.parallel S).Equiv (Computation.parallel T)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instRatCast : {Γ : Type u_1} →
  {R : Type u_3} → [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [RatCast R] → RatCast (HahnSeries Γ R)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenIsoSpec_hom : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).hom = AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f
-- Mathlib.InformationTheory.Hamming
Hamming.instSMulWithZero : {α : Type u_1} →
  {ι : Type u_2} →
    {β : ι → Type u_3} →
      [inst : Zero α] → [inst_1 : (i : ι) → Zero (β i)] → [(i : ι) → SMulWithZero α (β i)] → SMulWithZero α (Hamming β)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instDecidableCmpEqOfTransCmp : {α : Type u_1} → {x y : α} → (cmp : α → α → Ordering) → [Std.TransCmp cmp] → Decidable (RBTree.RBNode.cmpEq cmp x y)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.prime_C_iff : ∀ {R : Type u} [inst : CommRing R] {r : R}, Prime (Polynomial.C r) ↔ Prime r
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.mk : {X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    (R : Type u) →
      [commRing : CommRing R] →
        [domain : IsDomain R] →
          [valuationRing : ValuationRing R] →
            (K : Type u) →
              [field : Field K] →
                [algebra : Algebra R K] →
                  [isFractionRing : IsFractionRing R K] →
                    (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) →
                      (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y) →
                        CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f
                            i₂ →
                          AlgebraicGeometry.ValuativeCommSq f
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_eq_mk_compl_finite_lift : ∀ {α : Type u} {β : Type v} [Finite α] {s : Set α} {t : Set β},
  Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β) →
    Cardinal.lift.{v, u} (Cardinal.mk ↑s) = Cardinal.lift.{u, v} (Cardinal.mk ↑t) →
      Cardinal.lift.{v, u} (Cardinal.mk ↑sᶜ) = Cardinal.lift.{u, v} (Cardinal.mk ↑tᶜ)
-- Mathlib.Logic.Equiv.Basic
Equiv.instAssociativeCoeForallForallArrowCongr : ∀ {α₁ : Type u_11} {β₁ : Type u_12} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.Associative f],
  Std.Associative ((e.arrowCongr (e.arrowCongr e)) f)
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.pow_succ : ∀ (n : ℕ) {S : Type u_5} [inst : MonoidWithZero S] {x : S}, IsNilpotent x → IsNilpotent (x ^ n.succ)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The range of the projection is the span of the first `n` basis elements.  -/
SchauderBasis.range_proj_eq_span : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ),
  (↑(b.proj n)).range = Submodule.span 𝕜 (↑b '' ↑(Finset.range n))
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S =
    CategoryTheory.Limits.Pi.lift fun s => CategoryTheory.Limits.Pi.π f (↑s).as
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.inf_normalizer_le_normalizer_inf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  AddSubgroup.normalizer ↑H ⊓ AddSubgroup.normalizer ↑K ≤ AddSubgroup.normalizer ↑(H ⊓ K)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_rpow_inv : ∀ {x y : ℝ}, 0 ≤ x → y ≠ 0 → (x ^ y) ^ y⁻¹ = x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (snd : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.keys (⟨k, snd⟩ :: l) = k :: Std.Internal.List.keys l
-- Mathlib.Control.ULiftable
instULiftableContTULift : {s : Type u_5} →
  {m : Type u_5 → Type u_6} →
    {m' : Type (max u_5 u_7) → Type u_8} → [ULiftable m m'] → ULiftable (ContT s m) (ContT (ULift.{u_7, u_5} s) m')
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.empty_toList : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ}, Monoid.PushoutI.NormalWord.empty.toList = []
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInL.injEq : ∀ (p p_1 : Mathlib.Tactic.ITauto.Proof), (p.orInL = p_1.orInL) = (p = p_1)
-- Plausible.Gen
Plausible.instInhabitedGenError : Inhabited Plausible.GenError
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.det_coe : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ}, (↑↑(ModularGroup.coe g)).det = 1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f f_1 : α → β)
  (e_f : f = f_1) (hf : Continuous f) (K K_1 : TopologicalSpace.Compacts α),
  K = K_1 → TopologicalSpace.Compacts.map f hf K = TopologicalSpace.Compacts.map f_1 ⋯ K_1
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The full subcategory of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] → [CategoryTheory.Limits.HasInitial C] → Type u
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
/-- The growth of a set generating an infinite group is at least linear.  -/
Finset.add_one_le_card_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G},
  1 ∈ X → (↑(Subgroup.closure ↑X)).Infinite → ∀ (n : ℕ), n + 1 ≤ (X ^ n).card
-- Mathlib.Order.Std
PartialOrder.OfStdArgs.mk : {α : Type u_1} →
  (toPreorderArgs : Preorder.OfStdArgs α) →
    autoParam
        (let this := toPreorderArgs.le;
        Std.IsPartialOrder α)
        PartialOrder.OfStdArgs.isPartialOrder._autoParam →
      PartialOrder.OfStdArgs α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.file.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.file = 1
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an encoded fragment component from raw bytes.
 -/
Std.Http.URI.EncodedFragment.ofByteArray? : ByteArray → Option Std.Http.URI.EncodedFragment
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.exists_eq_const_of_zero : ∀ {n : SimplexCategory} (f : { len := 0 } ⟶ n), ∃ a, f = { len := 0 }.const n a
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.SigmaFinite μ] {f : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) → f =ᵐ[μ] 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_left : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a b : M₀} [MulPosStrictMono M₀],
  0 < a → 1 < b → a < b * a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView : Type
-- Lean.Meta.Tactic.Simp.Main
/-- Auxiliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.doNotVisitOfScientific : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine.inj : ∀ {c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Probability.Moments.Basic
ContinuousLinearEquiv.integral_id_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} [BorelSpace E] [inst_11 : MeasurableSpace F] [BorelSpace F] (L : E ≃L[𝕜] F),
  ∫ (x : F), x ∂MeasureTheory.Measure.map (⇑L) μ = L (∫ (x : E), x ∂μ)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
IsDomain.minimalPrimes_eq_singleton_bot : ∀ (R : Type u_1) [inst : CommSemiring R] [IsDomain R], minimalPrimes R = {⊥}