mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_le_size_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ},
  m.size ≤ (Std.ExtDHashMap.Const.insertMany m l).size
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.neg : ∀ {M₁ : Type u_3} {M₄ : Type u_5} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₄] [inst_3 : AddCommGroup M₄] [ContinuousNeg M₄] {f : M₁ → M₄},
  IsCompactOperator f → IsCompactOperator (-f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- `G` is a commutative group object if and only if the commutator map `(x, y) ↦ x * y * x⁻¹ * y⁻¹`
is constant.  -/
CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommMonObj G ↔
    CategoryTheory.GrpObj.commutator G =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorObj G G))
        CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y},
      CategoryTheory.IsUniversalColimit b →
        ∀ (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S)
          [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] [CategoryTheory.Limits.HasPullback u v]
          {P : ι × ι' → C} {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j},
          (∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) →
            ∀ (d : CategoryTheory.Limits.Cofan P) (hd : CategoryTheory.Limits.IsColimit d),
              autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                  CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit._auto_1 →
                autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                    CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit._auto_3 →
                  CategoryTheory.IsPullback
                    (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p =>
                      CategoryTheory.CategoryStruct.comp (q₁ p.1 p.2) (a.inj p.1))
                    (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p =>
                      CategoryTheory.CategoryStruct.comp (q₂ p.1 p.2) (b.inj p.2))
                    u v
-- Mathlib.Order.Compare
cmp.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] (a b : α), cmp a b = cmpUsing (fun x1 x2 => x1 < x2) a b
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.empty_indep : ∀ {α : Type u_1} (M : Matroid α), M.Indep ∅
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalₗ_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] (x : X) (x_1 : LocallyConstant X Y),
  (LocallyConstant.evalₗ R x) x_1 = x_1 x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter (fun a x => f a) t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = false)
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The setoid of splittings with `N`-conjugacy  -/
AddGroupExtension.IsAddConj.setoid : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] →
        {E : Type u_3} → [inst_2 : AddGroup E] → (S : AddGroupExtension N E G) → Setoid S.Splitting
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.dep_of_ssubset : ∀ {α : Type u_1} {M : Matroid α} {I X Y : Set α}, M.IsBasis I X → I ⊂ Y → Y ⊆ X → M.Dep Y
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.mk.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} (hom hom_1 : (n : ℤ) → X.H n ⟶ X'.H n) (e_hom : hom = hom_1)
  (comm :
    ∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
      CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
        CategoryTheory.CategoryStruct.comp ((hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g)) (X'.δ f g n₀ n₁ hn₁)),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.neg_fdiv_neg : ∀ (a b : ℤ), (-a).fdiv (-b) = a.fdiv b
-- Init.Data.Array.DecidableEq
Array.isEqv_toList : ∀ {α : Type u_1} {r : α → α → Bool} [BEq α] (xs ys : Array α), xs.toList.isEqv ys.toList r = xs.isEqv ys r
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx.mk.inj : ∀ {toConfig toConfig_1 : Lean.Meta.Simp.Config},
  { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)}
  (h : (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a)) h)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- the product of `f : F` assuming `ContinuousMapClass F α γ` and `ContinuousSMul γ β` and
`g : C_c(α, β)` is in `C_c(α, β)`  -/
CompactlySupportedContinuousMap.instSMulOfContinuousSMulOfContinuousMapClass : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : Zero β] →
            [inst_3 : TopologicalSpace γ] →
              [inst_4 : SMulZeroClass γ β] →
                [ContinuousSMul γ β] →
                  {F : Type u_5} →
                    [inst_6 : FunLike F α γ] → [ContinuousMapClass F α γ] → SMul F (CompactlySupportedContinuousMap α β)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.map_N : ∀ {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] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteCoproducts F] (n : ℕ),
  (s.map F).N n = F.obj (s.N n)
-- Mathlib.Analysis.RCLike.Basic
RCLike.realLinearIsometryEquiv_symm_apply : ∀ {K : Type u_1} [inst : RCLike K] (h : RCLike.I = 0) (a : ℝ),
  (RCLike.realLinearIsometryEquiv h).symm a = (RCLike.realRingEquiv h).invFun a
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.invRotate_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.invRotate.obj₂ = T.obj₁
-- Mathlib.Algebra.Homology.Homotopy
dNext_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι),
  ¬c.Rel i (c.next i) → (dNext i) f = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_map_iff : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ},
  1 < n →
    ∀ {t : Finset β} {f : α ↪ β}, (SimpleGraph.map (⇑f) G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ Finset.map f s = t
-- Mathlib.Combinatorics.Additive.Energy
/-- The additive energy `E[s, t]` of two finsets `s` and `t` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ + b₁ = a₂ + b₂`.

The notation `E[s, t]` is available in scope `Combinatorics.Additive`.  -/
Finset.addEnergy : {α : Type u_1} → [DecidableEq α] → [Add α] → Finset α → Finset α → ℕ
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.rify_simps_proc : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Monotone.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [AddLeftMono α],
  Monotone f → ∀ (a : α), Monotone fun x => a + f x
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β),
  (FrameHom.id β).comp f = f
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.const : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E} {b : F},
  ContDiffPointwiseHolderAt k α (Function.const E b) a
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.iSup_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {α : Type u_1} {Φ Ψ : α → l},
  (∀ (a : α), Lean.Order.PartialOrder.rel (Φ a) (Ψ a)) →
    Lean.Order.PartialOrder.rel (Lean.Order.iSup Φ) (Lean.Order.iSup Ψ)
-- Mathlib.Analysis.InnerProductSpace.Calculus
hasFDerivWithinAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {f' : H →L[𝕜] EuclideanSpace 𝕜 ι} {t : Set H} {y : H}
  [Finite ι],
  HasFDerivWithinAt f f' t y ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => (f x).ofLp i) (PiLp.proj 2 (fun x => 𝕜) i ∘SL f') t y
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Real.list_prod_map_rpow' : ∀ {ι : Type u_1} (l : List ι) (f : ι → ℝ),
  (∀ i ∈ l, 0 ≤ f i) → ∀ (r : ℝ), (List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
-- Batteries.Data.String.Lemmas
String.prev_of_valid : ∀ (cs : List Char) (c : Char) (cs' : List Char),
  String.Pos.Raw.prev (String.ofList (cs ++ c :: cs')) { byteIdx := String.utf8Len cs + c.utf8Size } =
    { byteIdx := String.utf8Len cs }
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.sub : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x - g x) s
-- Mathlib.Order.CompactlyGenerated.Basic
/-- In a compactly generated complete lattice,
every element is the `sSup` of some set of compact elements.  -/
IsCompactlyGenerated.exists_sSup_eq : ∀ {α : Type u_3} {inst : CompleteLattice α} [self : IsCompactlyGenerated α] (x : α),
  ∃ s, (∀ x ∈ s, IsCompactElement x) ∧ sSup s = x
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- If `forget C` preserves terminals and `X` is terminal, then `ToType X` is a
singleton.  -/
CategoryTheory.Limits.Concrete.uniqueOfTerminalOfPreserves : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
              (X : C) → CategoryTheory.Limits.IsTerminal X → Unique (CategoryTheory.ToType X)
-- Mathlib.Order.Irreducible
supPrime_iff_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, SupPrime a ↔ ¬IsMin a
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanQuadrant.ext_iff : ∀ {n : ℕ} {x y : EuclideanQuadrant n}, x = y ↔ ↑x = ↑y
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.isBasis'_iff_indep_encard_eq_of_finite : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, I.Finite → (M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_symm_assoc : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} (f : M₃ →ₛₗ[σ₃₂] M₂)
  [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂], ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.funLike : {E : Type u_3} → [inst : AddGroup E] → FunLike (AddGroupNorm E) E ℝ
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.mk.inj : ∀ {A : Type u} {inst : Ring A} {M : Type v} {inst_1 : AddCommGroup M} {inst_2 : Module A M}
  {toRelations : Module.Relations A} {toSolution : toRelations.Solution M}
  {toIsPresentation : toSolution.IsPresentation} {toRelations_1 : Module.Relations A}
  {toSolution_1 : toRelations_1.Solution M} {toIsPresentation_1 : toSolution_1.IsPresentation},
  { toRelations := toRelations, toSolution := toSolution, toIsPresentation := toIsPresentation } =
      { toRelations := toRelations_1, toSolution := toSolution_1, toIsPresentation := toIsPresentation_1 } →
    toRelations = toRelations_1 ∧ toSolution ≍ toSolution_1
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
instPolishSpaceEReal : PolishSpace EReal
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_hom_ne_zero : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Multiset M},
  s ≠ 0 → ∀ {F : Type u_8} [inst_2 : FunLike F M N] [AddHomClass F M N] (f : F), (Multiset.map (⇑f) s).sum = f s.sum
-- Mathlib.Data.List.Basic
List.head!_mem_self : ∀ {α : Type u} [inst : Inhabited α] {l : List α}, l ≠ [] → l.head! ∈ l
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- **Fundamental theorem of algebra**: the field `ℂ` of complex numbers is algebraically closed.  -/
Complex.isAlgClosed : IsAlgClosed ℂ
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.apply_eq_iff_eq_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂},
  e p₁ = p₂ ↔ p₁ = e.symm p₂
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.homInduction_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} (inl : (x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inl_ C D).map f))
  (inr : (x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inr_ C D).map f)) {x y : C} (f : x ⟶ y),
  CategoryTheory.Sum.homInduction inl inr ((CategoryTheory.Sum.inl_ C D).map f) = inl x y f
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.openCover_f : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J), D.openCover.f i = D.ι i
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.op_pullbackMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)
  [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T)
  [inst_2 : CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
  (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoOpPullback g₁.op g₂.op).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯)
        (CategoryTheory.Limits.pushoutIsoOpPullback f₁.op f₂.op).hom)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_neg' : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f : α → G), s.indicator (-f) = -s.indicator f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α}
  {fallback : β a}, ∅.getD a fallback = fallback
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- A linear operator on a complex inner product space is symmetric precisely when
`⟪T v, v⟫_ℂ` is real for all v.  -/
LinearMap.isSymmetric_iff_inner_map_self_real : ∀ {V : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V),
  T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ) (inner ℂ (T v) v) = inner ℂ (T v) v
-- Mathlib.Order.Ideal
Order.Ideal.toIdeal_le : ∀ {P : Type u_1} [inst : LE P] {I : Set P} (h : Order.IsIdeal I) {J : Order.Ideal P}, h.toIdeal ≤ J ↔ I ⊆ ↑J
-- Lean.Setup
Lean.instToStringImport : ToString Lean.Import
-- Lean.Setup
Lean.instFromJsonImport.fromJson : Lean.Json → Except String Lean.Import
-- Init.Control.ExceptCps
ExceptCpsT.lift.eq_1 : ∀ {m : Type u_1 → Type u_2} {α ε : Type u_1} [inst : Monad m] (x : m α) (x_1 : Type u_1) (k : α → m x_1)
  (x_2 : ε → m x_1), ExceptCpsT.lift x x_1 k x_2 = x >>= k
-- Std.Time.Format.Modifier
/-- `abstractParse` abstracts the parsing logic for any type that has a classify function.
It takes a constructor function to build the `Modifier` and a classify function that maps the pattern length to a specific type.
 -/
_private.Std.Time.Format.Modifier.0.Std.Time.parseMod : {α : Type u_1} → (α → Std.Time.Modifier) → (ℕ → Option α) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.checkMaxSteps : Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The left unitor isomorphism for Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                (F : CategoryTheory.Functor C V) →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
                          (CategoryTheory.MonoidalCategory.tensorRight v)] →
                    [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] →
                      CategoryTheory.MonoidalCategory.DayConvolution.convolution U F ≅ F
-- Mathlib.Tactic.Linter.Whitespace
/-- Produces a `FormatError` from the input data.  It expects
* `ls` to be a "user-typed" string;
* `ms` to be a "pretty-printed" string;
* `msg` to be a custom error message, such as `extra space` or `remove line break`;
* `length` (optional with default `1`), how many characters the error spans.

In particular, it extracts the position information within the string, both as number of characters
and as `String.Pos`.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.mkFormatError : String → String → String → optParam ℕ 1 → Mathlib.Linter.FormatError✝
-- Mathlib.CategoryTheory.Grothendieck
/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration.  -/
CategoryTheory.Grothendieck.grothendieckTypeToCatInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Functor G.Elements (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.dpow_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (self : hI.SubDPIdeal) (n : ℕ),
  n ≠ 0 → ∀ j ∈ self.carrier, hI.dpow n j ∈ self.carrier
-- Mathlib.Data.Int.Log
Int.self_le_zpow_clog : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ (r : R), r ≤ ↑b ^ Int.clog b r
-- Mathlib.Order.Closure
ClosureOperator.closure_iSup₂_closure : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] (c : ClosureOperator α)
  (f : (i : ι) → κ i → α), c (⨆ i, ⨆ j, c (f i j)) = c (⨆ i, ⨆ j, f i j)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_pow_add_le_pow_sup_pow : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R} {n m : ℕ}, (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_v₂₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.v₂₃ = CategoryTheory.ShortComplex.opMap S.v₀₁
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The embedding from `up ℕ` to `up ℤ` which sends `n : ℕ` to `p + n`.  -/
ComplexShape.embeddingUpIntGE : ℤ → (ComplexShape.up ℕ).Embedding (ComplexShape.up ℤ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.inr_ι : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (self : F.PushoutObjObj f₁ f₂), CategoryTheory.CategoryStruct.comp self.inr self.ι = (F.map f₁).app Y₂
-- Init.Data.Nat.Bitwise.Lemmas
Nat.bitwise_mod_two_pow : ∀ {f : Bool → Bool → Bool} {x y n : ℕ},
  autoParam (f false false = false) Nat.bitwise_mod_two_pow._auto_9 →
    Nat.bitwise f x y % 2 ^ n = Nat.bitwise f (x % 2 ^ n) (y % 2 ^ n)
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of `pow_eq_zero_iff`. -/
IsReduced.pow_eq_zero_iff : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀], n ≠ 0 → (a ^ n = 0 ↔ a = 0)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instIsNegApply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}, IsNegApply (ContDiffMapSupportedIn E F n K) E F
-- Mathlib.Tactic.ToDual
le_of_eq_of_le'' : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a = b → c ≤ b → c ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- An arrow starting at the zero object is zero  -/
CategoryTheory.Limits.zero_of_from_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : 0 ⟶ X), f = 0