mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.commGroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] [inst_1 : IsCyclic α], IsCyclic.commGroup = inferInstance
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_fst_v'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {Z : C} (h : F.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (i - 1) i)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) h) =
    CategoryTheory.CategoryStruct.comp
      (-CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (i - 1) i ⋯) (F.d i j)) h
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s) (Y'_1 : C) (f_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (hs_1 : W s_1),
  ({ Y' := Y', f := f, s := s, hs := hs } = { Y' := Y'_1, f := f_1, s := s_1, hs := hs_1 }) =
    (Y' = Y'_1 ∧ f ≍ f_1 ∧ s ≍ s_1)
-- Mathlib.CategoryTheory.PEmpty
/-- The equivalence between two empty categories.  -/
CategoryTheory.equivalenceOfIsEmpty : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u') → [inst_1 : CategoryTheory.Category.{v', u'} D] → [IsEmpty C] → [IsEmpty D] → C ≌ D
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_of_X_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W'.addZ P Q = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' fallback : α} {f : β → β},
  (Std.DHashMap.Const.modify m k f).getKeyD k' fallback =
    if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f 1 = 1
-- Init.Data.Vector.Erase
Vector.getElem?_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n) {j : ℕ},
  (xs.eraseIdx i h)[j]? = if j < i then xs[j]? else xs[j + 1]?
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `tangentMap I I' f` is the derivative of `f : M → M'` as a map between the tangent bundles
`TM` and `TM'`.  -/
tangentMap : {𝕜 : 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'] →
                                        (M → M') → TangentBundle I M → TangentBundle I' M'
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.isometry_ofFun_boundedContinuousFunction : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α],
  Isometry (⇑UniformFun.ofFun ∘ DFunLike.coe)
-- Mathlib.ModelTheory.Basic
/-- The homomorphism sends related elements to related elements  -/
FirstOrder.Language.Embedding.map_rel' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Embedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_mem_span : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  {j i : ι}, i ≤ j → InnerProductSpace.gramSchmidt 𝕜 f i ∈ Submodule.span 𝕜 (f '' Set.Iic j)
-- Mathlib.Data.Set.NAry
Set.image2_right : ∀ {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β}, s.Nonempty → Set.image2 (fun x y => y) s t = t
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.restrictScalars_inj : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f g : M ≃ₗ[S] M₂),
  LinearEquiv.restrictScalars R f = LinearEquiv.restrictScalars R g ↔ f = g
-- Mathlib.Order.Concept
subset_upperPolar_iff_subset_lowerPolar : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {t : Set β}, t ⊆ upperPolar r s ↔ s ⊆ lowerPolar r t
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry : Type
-- Init.Data.UInt.Lemmas
UInt32.pos_iff_ne_zero : ∀ {a : UInt32}, 0 < a ↔ a ≠ 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_comp : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_6} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] [inst_7 : TopologicalSpace R₁] [inst_8 : ContinuousSMul R₁ M₂] (f : M₁ →L[R₁] R₁) (g : M₂),
  ContinuousLinearMap.toSpanSingleton R₁ g ∘SL f = f.smulRight g
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The natural transformation `F ⟶ L ⋙ (L.lan).obj G`.  -/
CategoryTheory.Functor.lanUnit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] →
                CategoryTheory.Functor.id (CategoryTheory.Functor C H) ⟶
                  L.lan.comp ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)
-- Init.Data.Int.Gcd
Int.lcm_eq_natAbs_right_iff_dvd : ∀ {a b : ℤ}, a.lcm b = b.natAbs ↔ a ∣ b
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_inter_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.edges_nodup : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsTrail → p.edges.Nodup
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprTransition.repr : Std.Time.TimeZone.Transition → ℕ → Std.Format
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_bot : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊥.unop = ⊥
-- Batteries.Data.List.Basic
List.Forall₂.brecOn : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.Forall₂ R a a_1 → Prop} {a : List α} {a_1 : List β}
  (t : List.Forall₂ R a a_1),
  (∀ (a : List α) (a_2 : List β) (t : List.Forall₂ R a a_2), List.Forall₂.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioi_disjoint_Iio_of_le : ∀ {α : Type v} [inst : Preorder α] {a b : α}, a ≤ b → Disjoint (Set.Ioi b) (Set.Iio a)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.isRed_reverse : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.reverse.isRed = t.isRed
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Additive version of `Prod.nnnorm_mk'`.  -/
Prod.nnnorm_mk : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] (x : E) (y : F),
  ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_zero_of_even : ∀ (R : Type u_1) [inst : CommRing R] {n : ℤ},
  Even n → Polynomial.eval 0 (Polynomial.Chebyshev.T R n) = ↑↑(n / 2).negOnePow
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.mk : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      [inst_2 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- Successor in a linear order. This defines a true successor only when `i` is isolated from above,
i.e. when `i` is not the greatest lower bound of `(i, ∞)`.  -/
LinearLocallyFiniteOrder.succFn : {ι : Type u_1} → [LinearOrder ι] → ι → ι
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_4 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_4 ()
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIcoDiv_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIcoDiv hp a b • p = toIcoMod hp a b
-- Mathlib.Topology.Connected.Basic
Continuous.mapsTo_connectedComponentIn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  Continuous f → ∀ {a : α}, a ∈ s → Set.MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAtFilter_add_const_iff`. -/
HasDerivAtFilter.add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun x => f x + c) f' L
-- Init.Data.Vector.OfFn
Vector.map_ofFn : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} {f : Fin n → α} {g : α → β}, Vector.map g (Vector.ofFn f) = Vector.ofFn (g ∘ f)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivAt.eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  IsSymmSndFDerivAt 𝕜 f x → ∀ (v w : E), ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) w) v
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) The natural transformation used to define the new cocone  -/
CategoryTheory.Comonad.ForgetCreatesColimits'.γ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) → D.comp T.forget ⟶ D.comp (T.forget.comp T.toFunctor)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instBialgebraObjForgetBialgHomCarrier : {R : Type u} → [inst : CommRing R] → {A : CommBialgCat R} → Bialgebra R ((CategoryTheory.forget (CommBialgCat R)).obj A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.isEmpty = true → t.getD a fallback = fallback
-- Mathlib.Data.Finset.Insert
Finset.insertPiProd.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i),
  Finset.insertPiProd f x = (x a ⋯, fun i hi => x i ⋯)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of additive Haar measures**:
Two additive Haar measures on a compact additive group coincide up to a multiplicative factor.  -/
MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [CompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : μ'.IsAddLeftInvariant] [inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ'],
  μ' = μ'.addHaarScalarFactor μ • μ
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk'_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s), (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk''.injEq : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (toContinuousLinearEquiv : V ≃L[R] W)
  (cont : autoParam (Continuous (↑↑toContinuousLinearEquiv).toFun) ContinuousLinearMap.cont._autoParam)
  (isIntertwining' :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont })
  (toContinuousLinearEquiv_1 : V ≃L[R] W)
  (cont_1 : autoParam (Continuous (↑↑toContinuousLinearEquiv_1).toFun) ContinuousLinearMap.cont._autoParam)
  (isIntertwining'_1 :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv_1, cont := cont_1 } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv_1, cont := cont_1 }),
  ({ toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' } =
      { toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := cont_1, isIntertwining' := isIntertwining'_1 }) =
    (toContinuousLinearEquiv = toContinuousLinearEquiv_1)
-- Mathlib.FieldTheory.Normal.Closure
normalClosure_le_iff : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] {K' : IntermediateField F L},
  IntermediateField.normalClosure F K L ≤ K' ↔ ∀ (f : K →ₐ[F] L), f.fieldRange ≤ K'
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.ReflectsEffectiveEpis.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.EffectiveEpi (F.map f) → CategoryTheory.EffectiveEpi f) →
    F.ReflectsEffectiveEpis
-- Mathlib.Algebra.Ring.Defs
/-- A `Ring` is a `Semiring` with negation making it an additive group.  -/
Ring : Type u → Type u
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.mul.injEq : ∀ (a b a_1 b_1 : Nat.Internal.SOM.Expr), (a.mul b = a_1.mul b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.d_eqToHom_assoc : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β}
  (h : y = z) {Z : V} (h_1 : X.X z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp (X.d x z) h_1
-- Mathlib.Data.NNReal.Defs
/-- **Alias** of the reverse direction of `NNReal.coe_pos`. -/
Mathlib.Meta.Positivity.nnreal_coe_pos : ∀ {r : NNReal}, 0 < r → 0 < ↑r
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticStx.injEq : ∀ (stx stx_1 : Lean.Syntax), (Aesop.RuleTacDescr.tacticStx stx = Aesop.RuleTacDescr.tacticStx stx_1) = (stx = stx_1)
-- Mathlib.Data.List.Basic
List.head?.eq_1 : ∀ {α : Type u}, [].head? = none
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.cpolynomialAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F)
  (x : E), CPolynomialAt 𝕜 (⇑f) x
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.deriv_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (fun x => x • f x) MeasureTheory.volume →
      deriv (FourierTransform.fourier f) = FourierTransform.fourier fun x => (-2 * ↑Real.pi * Complex.I * ↑x) • f x
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.

For non-mutual definitions, we omit `sizeOf` when the measure does not depend on
the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.

For mutual definitions, we omit `sizeOf` only when the measure is (at reducible transparency!) of
type `Nat` (else we'd have to worry about differently-typed measures from different functions to
line up).
 -/
Lean.Elab.WF.GuessLex.mayOmitSizeOf : Bool → Array Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Http.Data.Version
Std.Http.Version.ofNat_ctorIdx : ∀ (x : Std.Http.Version), Std.Http.Version.ofNat x.ctorIdx = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_erase!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.erase! k t) k fallback = fallback
-- Mathlib.Algebra.Lie.Free
/-- Note that here we turn the `Mul` coming from the `NonUnitalNonAssocSemiring` structure
on `lib R X` into a `Bracket` on `FreeLieAlgebra`.  -/
FreeLieAlgebra.instLieRing : (R : Type u) → (X : Type v) → [inst : CommRing R] → LieRing (FreeLieAlgebra R X)
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depthLB_le : ∀ (c : RBTree.RBColor) (n : ℕ), n ≤ RBTree.RBNode.depthLB c n
-- Mathlib.Data.Sign.Defs
sign_neg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] {a : α}, a < 0 → SignType.sign a = -1
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij_img : ∀ (d n : ℕ),
  Squarefree n →
    ∀ (f : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hf : f ∈ n.primeFactors.pi fun x => Finset.univ),
      Nat.primeFactorsPiBij✝ d n f hf ∈ d.finMulAntidiag n
-- Mathlib.Analysis.Matrix.Normed
_private.Mathlib.Analysis.Matrix.Normed.0.Matrix.mul_unitOf : ∀ {α : Type u_5} [inst : NormedDivisionRing α] [inst_1 : NormedAlgebra ℝ α] (a : α),
  a * Matrix.unitOf✝ a = (algebraMap ℝ α) ↑‖a‖₊
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_eq_of_le : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a b : A}, a ≤ b → imaginaryPart a = imaginaryPart b
-- Init.Data.Vector.Perm
/-- `Perm as bs` asserts that `as` and `bs` are permutations of each other.

This is a wrapper around `List.Perm`, and for now has much less API.
For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
Vector.Perm : {α : Type u_1} → {n : ℕ} → Vector α n → Vector α n → Prop
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.tokenWithAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.revMatchesAt_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt p pos ↔ ∃ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = true
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C),
  ((CategoryTheory.PreGaloisCategory.functorToContAction F).obj X).obj =
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj X
-- Lean.Data.Json.FromToJson.Basic
Lean.Name.fromJson? : Lean.Json → Except String Lean.Name
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.ordered_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t ↔ List.Pairwise (RBTree.RBNode.cmpLT cmp) t.toList
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.cokernelBiprodInlIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.cokernelBiprodInlIso.hom =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0)
      (CategoryTheory.Limits.biprod.inlCokernelCofork X Y)
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a Haar measure under map of a left additive action is again a Haar measure  -/
MeasureTheory.Measure.isAddHaarMeasure_map_vadd : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] {α : Type u_3} [BorelSpace G] [IsTopologicalAddGroup G]
  [inst_6 : AddGroup α] [inst_7 : AddAction α G] [VAddCommClass α G G] [ContinuousConstVAdd α G] (a : α),
  (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddHaarMeasure
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Set α),
  (MeasureTheory.Measure.dirac a) s = s.indicator 1 a
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_ne_zero : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [Countable G] [MeasureTheory.VAddInvariantMeasure G α μ],
  μ ≠ 0 → MeasureTheory.IsAddFundamentalDomain G s μ → μ s ≠ 0