mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Show that `G` preserves right Kan extensions if it maps some right Kan extension to a right
Kan extension.  -/
CategoryTheory.Functor.PreservesRightKanExtension.mk_of_preserves_isRightKanExtension : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (F' : CategoryTheory.Functor C B) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α],
  (F'.comp G).IsRightKanExtension
      (CategoryTheory.CategoryStruct.comp (L.associator F' G).inv (CategoryTheory.Functor.whiskerRight α G)) →
    G.PreservesRightKanExtension F L
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- A functor `PreservesColimit₂ K₁ K₂` if whenever `c₁` is a colimit cocone and `c₂` is a colimit
cocone then `G.mapCocone₂ c₁ c₂` is a colimit cocone. This can be thought of as the data of an
isomorphism
$\mathrm{colim}_{(j_1,j_2)} G(K_1(j_1),K_2(j_2)) \simeq G(\mathrm{colim} K_1,\mathrm{colim} K_2)$.
 -/
CategoryTheory.Limits.PreservesColimit₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    CategoryTheory.Functor J₁ C₁ →
                      CategoryTheory.Functor J₂ C₂ → CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C) → Prop
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_symm_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Cardinal.preAleph.symm (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C),
  CategoryTheory.Abelian.Ext.mapExactFunctor F =
    ⇑CategoryTheory.Abelian.Ext.homEquiv₀.symm ∘ F.map ∘ ⇑CategoryTheory.Abelian.Ext.homEquiv₀
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.inv_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) (X : C), CategoryTheory.inv (e.inv.app X) = e.hom.app X
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
/-- The natural isomorphism of bifunctors `F - ⊗ F - ≅ F (- ⊗ -)`, given that `F` lifts along `L`
to a monoidal functor `G`, where `L` is a monoidal localization functor.
 -/
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (L : CategoryTheory.Functor C D) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [L.IsLocalization W] →
                        [L.Monoidal] →
                          (F : CategoryTheory.Functor D E) →
                            (G : CategoryTheory.Functor C E) →
                              [G.Monoidal] →
                                [W.ContainsIdentities] →
                                  [CategoryTheory.Localization.Lifting L W G F] →
                                    CategoryTheory.MonoidalCategory.curriedTensorPre F ≅
                                      CategoryTheory.MonoidalCategory.curriedTensorPost F
-- Init.GrindInstances.ToInt
Lean.Grind.instAddIntIi : Lean.Grind.ToInt.Add ℤ Lean.Grind.IntInterval.ii
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getElem_sdiv.match_1.eq_4 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_4 ()
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, (∀ (Y : D), F.isDenseAt Y) → F.IsDense
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_cons : ∀ {α : Type u_1} {β : Type u_2} (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β)
  (H : (↑(Finset.cons a s ha)).PairwiseDisjoint f),
  (Finset.cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f ⋯) ⋯
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.one_minus_single_neg_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x y : HahnSeries Γ R} {r : R},
  r * x.leadingCoeff = 1 →
    x = y + (HahnSeries.single x.order) x.leadingCoeff →
      ∀ (oinv : Γ), oinv + x.order = 0 → 1 - (HahnSeries.single oinv) r * x = -((HahnSeries.single oinv) r * y)
-- Lean.Elab.InfoTree.Basic
Lean.Elab.Info.stx : Lean.Elab.Info → Lean.Syntax
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two finite and free modules are isomorphic if and only if they have the same (finite) rank.  -/
FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R]
  [Module.Finite R M] [Module.Finite R M'], Nonempty (M ≃ₗ[R] M') ↔ Module.finrank R M = Module.finrank R M'
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_le_span_singleton : ∀ {α : Type u} [inst : CommSemiring α] {x y : α}, Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x
-- Mathlib.Analysis.Complex.RemovableSingularity
Complex.differentiableOn_dslope : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ}, s ∈ nhds c → (DifferentiableOn ℂ (dslope f c) s ↔ DifferentiableOn ℂ f s)
-- Lean.Meta.Tactic.Grind.Proof
Lean.Meta.Grind.mkEqCongrProof : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.brecOn : ∀ {F : PFunctor.{uA, uB}} {motive : (a : PFunctor.Approx.Path F) → (a_1 : F.M) → PFunctor.M.IsPath a a_1 → Prop}
  {a : PFunctor.Approx.Path F} {a_1 : F.M} (t : PFunctor.M.IsPath a a_1),
  (∀ (a : PFunctor.Approx.Path F) (a_2 : F.M) (t : PFunctor.M.IsPath a a_2),
      PFunctor.M.IsPath.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_of_natDegree_add_eq_zero : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).natDegree = 0 → p.natDegree = q.natDegree
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.

See issue #1571
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallBinders : Bool →
  (Array Lean.Syntax → Bool → Lean.Syntax → Lean.PrettyPrinter.Delaborator.Delab) →
    optParam (Array Lean.Syntax) #[] → optParam Bool false → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Heyting.Basic
sup_sdiff_left_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a ⊔ b) \ a = b \ a
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsEpimorphisms_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.ReflectsEpimorphisms] [G.ReflectsEpimorphisms], (F.comp G).ReflectsEpimorphisms
-- Mathlib.Data.Finmap
Finmap.union_assoc : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ s₃ : Finmap β}, s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
-- Lean.LibrarySuggestions.Basic
/-- The maximum number of suggestions to return.
 -/
Lean.LibrarySuggestions.Config.maxSuggestions : Lean.LibrarySuggestions.Config → ℕ
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.mk.injEq : ∀ (toElabInfo : Lean.Elab.ElabInfo) (name : Lean.Name) (kind : Lean.Elab.DocElabKind)
  (toElabInfo_1 : Lean.Elab.ElabInfo) (name_1 : Lean.Name) (kind_1 : Lean.Elab.DocElabKind),
  ({ toElabInfo := toElabInfo, name := name, kind := kind } =
      { toElabInfo := toElabInfo_1, name := name_1, kind := kind_1 }) =
    (toElabInfo = toElabInfo_1 ∧ name = name_1 ∧ kind = kind_1)
-- Lean.Parser.Term
Lean.Parser.Term.paren.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteIncidenceSet.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (x : V), G.deleteIncidenceSet x = G.deleteEdges (G.incidenceSet x)
-- Batteries.Data.MLList.Basic
/-- Return the head of a monadic lazy list if it exists, as an `Option` in the monad.  -/
MLList.head? : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → m (Option α)
-- Mathlib.Algebra.Group.Commute.Basic
/-- **Alias** of the reverse direction of `AddCommute.neg_left_iff`. -/
AddCommute.neg_left : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → AddCommute (-a) b
-- Mathlib.Algebra.Notation.Prod
Prod.instInv : {G : Type u_8} → {H : Type u_9} → [Inv G] → [Inv H] → Inv (G × H)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (a a_1 : List α),
  List.MergeSort.Internal.mergeTR.go✝ le [] a a_1 = a_1.reverseAux a
-- Mathlib.Topology.Instances.Matrix
instIsTopologicalSemiringMatrix : ∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Fintype n] [inst_2 : NonUnitalNonAssocSemiring R]
  [IsTopologicalSemiring R], IsTopologicalSemiring (Matrix n n R)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSigma.match_3.splitter : (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.sum f) → Sort u_1) →
  (n : ℕ) →
    (f : Fin n → ℕ) →
      (x : Fin (Fin.sum f)) →
        ((x : Fin 0 → ℕ) → (val : ℕ) → (h : val < Fin.sum x) → motive 0 x ⟨val, h⟩) →
          ((n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.sum f) → motive n.succ f ⟨x, hx⟩) → motive n f x
-- Mathlib.Data.Finset.Sum
Finset.mem_toLeft : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α}, a ∈ u.toLeft ↔ Sum.inl a ∈ u
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- Two multilinear maps from finitely supported functions are equal if they agree on the
generators.

This is a multilinear version of `DFinsupp.lhom_ext'`.  -/
MultilinearMap.dfinsupp_ext : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [Finite ι]
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_2 : AddCommMonoid N]
  [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_4 : Module R N] [inst_5 : (i : ι) → DecidableEq (κ i)]
  ⦃f g : MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DFinsupp.lsingle (p i)) = g.compLinearMap fun i => DFinsupp.lsingle (p i)) →
    f = g
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_neg_atBot_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.Tendsto Neg.neg Filter.atBot Filter.atTop
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) (L⟦a⟧) n`.  -/
CochainComplex.HomComplex.Cocycle.shift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.Cocycle K L n →
            (a : ℤ) →
              CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
                ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv_apply : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] [inst_6 : (i : ι) → DecidableEq (M i)] (f : (i : ι) → κ i →₀ M i)
  (p : (i : ι) → κ i),
  (PiTensorProduct.ofFinsuppEquiv ((PiTensorProduct.tprod R) fun i => f i)) p = ⨂ₜ[R] (i : ι), (f i) (p i)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.uniqueAlgEquiv_symm_monomial : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Unique σ] {d : σ →₀ ℕ} {r : R},
  (MvPolynomial.uniqueAlgEquiv R σ).symm ((Polynomial.monomial (d default)) r) = (MvPolynomial.monomial d) r
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.toReal_prod : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal), (∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_eq_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α] {x : α} (hx : 0 ≤ x),
  ⟨x, hx⟩ = 1 ↔ x = 1
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsCobounded.closedBall_compl_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  Bornology.IsCobounded s → ∀ (c : α), ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapM.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {β' : Type u_1} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) none)
  (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨none, hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_1 hf
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote'.go.induct_unfolding : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (motive : Lean.Grind.CommRing.Mon → α → α → Prop),
  (∀ (acc : α), motive Lean.Grind.CommRing.Mon.unit acc acc) →
    (∀ (acc : α) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        motive m (acc * Lean.Grind.CommRing.Power.denote ctx p)
            (Lean.Grind.CommRing.Mon.denote'.go ctx m (acc * Lean.Grind.CommRing.Power.denote ctx p)) →
          motive (Lean.Grind.CommRing.Mon.mult p m) acc
            (Lean.Grind.CommRing.Mon.denote'.go ctx m (acc * Lean.Grind.CommRing.Power.denote ctx p))) →
      ∀ (m : Lean.Grind.CommRing.Mon) (acc : α), motive m acc (Lean.Grind.CommRing.Mon.denote'.go ctx m acc)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial.exists_val_nontrivial : ∀ {R : Type u_3} {Γ₀ : Type u_4} {inst : Ring R} {inst_1 : LinearOrderedCommMonoidWithZero Γ₀} {v : Valuation R Γ₀}
  [self : v.IsNontrivial], ∃ x, v x ≠ 0 ∧ v x ≠ 1
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Whether the rewrite introduces a new metavariable in the replacement expression.  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.makesNewMVars : Mathlib.Tactic.LibraryRewrite.Rewrite → Bool
-- Mathlib.RingTheory.TensorProduct.Finite
Module.exists_surjective_quotient_of_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Nontrivial M], ∃ I f, I ≠ ⊤ ∧ Function.Surjective ⇑f
-- Mathlib.Algebra.DirectSum.Ring
/-- A direct sum of copies of a `Ring` inherits the multiplication structure.  -/
Ring.directSumGRing : (ι : Type u_1) → {R : Type u_2} → [inst : AddMonoid ι] → [inst_1 : Ring R] → DirectSum.GRing fun x => R
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_of_le : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc) (SimplexCategoryGenRel.σ j.succ) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j) (SimplexCategoryGenRel.δ i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.chainComplex.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X X_1 : SSet),
  X = X_1 → ∀ (R R_1 : C), R = R_1 → X.chainComplex R = X_1.chainComplex R_1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.sum_ofWithBot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [inst : AddCommMonoid M]
  (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I)
  (pairwise_disjoint : (↑boxes).Pairwise Disjoint) (f : BoxIntegral.Box ι → M),
  ∑ J ∈ (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes, f J =
    ∑ J ∈ boxes, Option.elim' 0 f J
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0),
  AdjoinRoot.liftAlgHom p i x h = { toRingHom := AdjoinRoot.lift i.toRingHom x h, commutes' := ⋯ }
-- Init.Data.Hashable
instHashable : (P : Prop) → Hashable P
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.iff_orderOf : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k ↔ orderOf ζ = k
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_one : ∀ {α : Type u_3} [inst : DivisionSemiring α], ↑1 = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} {fallback : β}, (a == b) = true → m.getD a fallback = m.getD b fallback
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → ∀ {t : Set E}, s ∈ nhdsWithin x t → DifferentiableWithinAt 𝕜 f t x
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift all suprema and infima along a Galois insertion  -/
GaloisInsertion.liftCompleteLattice : {α : Type u} →
  {β : Type v} →
    {l : α → β} →
      {u : β → α} → [inst : PartialOrder β] → [inst_1 : CompleteLattice α] → GaloisInsertion l u → CompleteLattice β
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.coe_algebraMapCoeffs : ∀ {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)),
  ⇑(Module.Basis.algebraMapCoeffs A b h) = ⇑b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRcoSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Rco.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RcoSlice α β)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The difference `log (1-z)⁻¹ - z` is bounded by `‖z‖^2/(2*(1-‖z‖))` when `‖z‖ < 1`.  -/
Complex.norm_log_one_sub_inv_sub_self_le : ∀ {z : ℂ}, ‖z‖ < 1 → ‖Complex.log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
-- Mathlib.CategoryTheory.Localization.Prod
/-- The lifting of a functor `F : C₁ × C₂ ⥤ E` inverting `W₁.prod W₂` to a functor
`W₁.Localization × W₂.Localization ⥤ E`  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {E : Type u₅} →
              [inst_2 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor (C₁ × C₂) E) →
                  (W₁.prod W₂).IsInvertedBy F →
                    [W₁.ContainsIdentities] →
                      [W₂.ContainsIdentities] → CategoryTheory.Functor (W₁.Localization × W₂.Localization) E
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.comp_left_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : T} (h : Z.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left g) h)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_diff_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Init.Data.List.Lemmas
List.filter_flatten : ∀ {α : Type u_1} {p : α → Bool} {L : List (List α)}, List.filter p L.flatten = (List.map (List.filter p) L).flatten
-- Mathlib.CategoryTheory.Whiskering
/-- If `α : G ⟶ H` then `whiskerLeft F α : F ⋙ G ⟶ F ⋙ H` has components `α.app (F.obj X)`.  -/
CategoryTheory.Functor.whiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) → {G H : CategoryTheory.Functor D E} → (G ⟶ H) → (F.comp G ⟶ F.comp H)
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)}
  (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p),
  ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩) =
    ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯).symm
        ⟨Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q, ⋯⟩)
-- Aesop.Forward.State
Aesop.RawHyp.fvarId.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, Aesop.RawHyp.fvarId fvarId = Aesop.RawHyp.fvarId fvarId_1 → fvarId = fvarId_1
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_ratCast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (q : ℚ), CauSeq.Completion.ofRat ↑q = ↑q
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.ι_normNoninc : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  {f g : NormedAddGroupHom V W}, (NormedAddGroupHom.Equalizer.ι f g).NormNoninc