mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_3.splitter : {α : Type u_1} →
  (γ : Type u_1) →
    (Pl : α → γ → ForInStep γ → Prop) →
      (next : α) →
        (acc : γ) →
          (motive : Subtype (Pl next acc) → Sort u_2) →
            (__do_lift : Subtype (Pl next acc)) →
              ((acc' : γ) → (h' : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', h'⟩) →
                ((acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩) →
                  motive __do_lift
-- Mathlib.Data.ZMod.IntUnitsPower
ZMod.smul_units_def : ∀ (z : ZMod 2) (au : Additive ℤˣ), z • au = z.val • au
-- Lean.Elab.MutualInductive
/-- Whether the command supports creating inductive types that can be polymorphic across both `Prop` and `Type _`.
If false, then either the universe must be `Prop` or it must be of the form `Type _`.  -/
Lean.Elab.Command.InductiveView.allowSortPolymorphism : Lean.Elab.Command.InductiveView → Bool
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.homeomorphOfUnit_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (T : (M₁ →L[R₁] M₁)ˣ) (a : M₁), (ContinuousLinearMap.homeomorphOfUnit T) a = ↑T a
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_mono : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {s t : Set P},
  s ⊆ t → asymptoticCone k s ⊆ asymptoticCone k t
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- **Turán's theorem**, forward direction.

Any `r + 1`-cliquefree Turán-maximal graph on `n` vertices is isomorphic to `turanGraph n r`.  -/
SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  G.IsTuranMaximal r → Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSymAux.eq_jacobiSym : ∀ {a b : ℕ} {flip : Bool} {ha0 : a > 0},
  b % 2 = 1 → b > 1 → fastJacobiSymAux✝ a b flip ha0 = if flip = true then -jacobiSym (↑a) b else jacobiSym (↑a) b
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_zero : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R],
  HahnSeries.SummableFamily.hsum 0 = 0
-- Mathlib.Data.Fintype.Fin
Fin.Iio_last_eq_map : ∀ {n : ℕ}, Finset.Iio (Fin.last n) = Finset.map Fin.castSuccEmb Finset.univ
-- Mathlib.Data.List.Intervals
List.Ico.map_add : ∀ (n m k : ℕ), List.map (fun x => k + x) (List.Ico n m) = List.Ico (n + k) (m + k)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.lengthParity_simple : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.evenOdd_map_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (n : ZMod 2),
  Submodule.map CliffordAlgebra.reverse (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α}, k ∈ Std.ExtHashMap.map f m → k ∈ m
-- Lean.Elab.Match
/-- Ensure that there are no metavariables in free variables and patterns of the `lhss`.
 -/
Lean.Elab.Term.instantiateAltLHSs : Array Lean.Meta.Match.AltLHS → Lean.Elab.TermElabM (List Lean.Meta.Match.AltLHS)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentSyncOptions : Lean.FromJson Lean.Lsp.TextDocumentSyncOptions
-- Mathlib.Data.Sigma.Interval
Sigma.instLocallyFiniteOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [DecidableEq ι] →
      [inst : (i : ι) → Preorder (α i)] → [(i : ι) → LocallyFiniteOrder (α i)] → LocallyFiniteOrder ((i : ι) × α i)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  (F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C),
  (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).obj F =
    F.mapCommMon.obj (CategoryTheory.CommMon.trivial (CategoryTheory.Discrete PUnit.{u + 1}))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso_inv_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).inv
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.image.ι f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι (F.map f)) h
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ext_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Trident.ext._auto_1),
  (CategoryTheory.Limits.Trident.ext i w).inv = CategoryTheory.Limits.Trident.mkHom i.inv ⋯
-- Mathlib.MeasureTheory.Measure.AEMeasurable
_private.Mathlib.MeasureTheory.Measure.AEMeasurable.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_univ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet Set.univ μ
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.lipschitz : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → LipschitzWith 1 f
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.equivOfIsClopenOfIsConnected.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ) (hconn : ∀ (i : ι), IsConnected (U i)),
  ConnectedComponents.equivOfIsClopenOfIsConnected hclopen hdisj hunion hconn =
    (ConnectedComponents.equivOfIsClopen hclopen hdisj hunion).trans
      (Equiv.sigmaUnique ι fun i => ConnectedComponents ↑(U i))
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vadd_left_image : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, ⋃ a ∈ s, a +ᵥ t = s +ᵥ t
-- Mathlib.Tactic.Ring.Basic
/-- `lift` is the "canonical injection" from `α` to `β`  -/
Mathlib.Tactic.Ring.CSLift.lift : {α : Type u} → {β : outParam (Type u)} → [self : Mathlib.Tactic.Ring.CSLift α β] → α → β
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.isClosed_complement : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M} [T1Space ↥p] (h : p.ClosedComplemented), IsClosed ↑h.complement
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).maxKey? = t.maxKey?
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The canonical function `M → N → M ⊗ N`. The localized notations are `m ⊗ₜ n` and `m ⊗ₜ[R] n`,
accessed by `open scoped TensorProduct`.  -/
TensorProduct.tmul : (R : Type u_1) →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → M → N → TensorProduct R M N
-- Mathlib.Order.Filter.IsBounded
Filter.Tendsto.isBoundedUnder_ge_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] {f : Filter β} {u : β → α},
  Filter.Tendsto u f Filter.atTop → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h : Std.Internal.List.containsKey a (l ++ l') = true} (hl' : Std.Internal.List.containsKey a l' = false),
  Std.Internal.List.getKey a (l ++ l') h = Std.Internal.List.getKey a l ⋯
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum is finite iff all terms are finite.  -/
WithTop.sum_ne_top : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M},
  ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_toHomeomorph_symm : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  ⇑h.toHomeomorph.symm = ⇑h.symm
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.coe_blockTriangularSubsemiring : ∀ {α : Type u_1} {m : Type u_3} (R : Type v) (b : m → α) [inst : LinearOrder α] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : Semiring R], ↑(Matrix.blockTriangularSubsemiring R b) = {M | M.BlockTriangular b}
-- Mathlib.Order.Category.BddLat
_private.Mathlib.Order.Category.BddLat.0.BddLat.Hom.mk : {X Y : BddLat} → BoundedLatticeHom ↑X.toLat ↑Y.toLat → X.Hom Y
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} [inst_1 : SizeOf C] (P : C) (p₀ p₁ : P ⟶ A) (ι : A ⟶ P)
  (ι_p₀ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₀ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam)
  (ι_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₁ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam),
  sizeOf { P := P, p₀ := p₀, p₁ := p₁, ι := ι, ι_p₀ := ι_p₀, ι_p₁ := ι_p₁ } =
    1 + sizeOf P + sizeOf p₀ + sizeOf p₁ + sizeOf ι + sizeOf ι_p₀ + sizeOf ι_p₁
-- Mathlib.AlgebraicGeometry.Group.Smooth
AlgebraicGeometry.smooth_of_grpObj : ∀ {K : Type u} [inst : Field K] {G : AlgebraicGeometry.Scheme} (f : G ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.LocallyOfFiniteType f] [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)]
  [AlgebraicGeometry.GeometricallyReduced f], AlgebraicGeometry.Smooth f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ Std.DTreeMap.Const.unitOfList l cmp},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.unitOfList l cmp) k h = ()
-- Mathlib.Algebra.Ring.CharZero
RingHom.injective_nat : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (f : ℕ →+* R) [CharZero R], Function.Injective ⇑f
-- Mathlib.SetTheory.Ordinal.Basic
/-- The proposition that `r` is a well-ordering for `α`.  -/
WellOrder.wo : ∀ (self : WellOrder), IsWellOrder self.α self.r
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The map from the affine `n`-space over `S` to the integral model `Spec ℤ[n]`.  -/
AlgebraicGeometry.AffineSpace.toSpecMvPoly : (n : Type u) →
  (S : AlgebraicGeometry.Scheme) →
    AlgebraicGeometry.AffineSpace n S ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.mk.inj : ∀ {propagateUp propagateDown : Lean.Meta.Grind.Propagator} {evalTactic : Lean.Meta.Grind.EvalTactic}
  {propagateUp_1 propagateDown_1 : Lean.Meta.Grind.Propagator} {evalTactic_1 : Lean.Meta.Grind.EvalTactic},
  { propagateUp := propagateUp, propagateDown := propagateDown, evalTactic := evalTactic } =
      { propagateUp := propagateUp_1, propagateDown := propagateDown_1, evalTactic := evalTactic_1 } →
    propagateUp = propagateUp_1 ∧ propagateDown = propagateDown_1 ∧ evalTactic = evalTactic_1
-- Batteries.Recycling.RBTree.Basic
/-- Erasing from a well-formed tree yields another well-formed tree.
(See `Ordered.erase` and `Balanced.erase` for the actual proofs.)  -/
RBTree.RBNode.WF.erase : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {cut : α → Ordering},
  RBTree.RBNode.WF cmp t → RBTree.RBNode.WF cmp (RBTree.RBNode.erase cut t)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves the cokernel of `h.f' : S.X₁ ⟶ h.K`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f' : ∀ {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} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {S : CategoryTheory.ShortComplex C} {h : S.LeftHomologyData}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms} [self : h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair h.f' 0) F
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E),
  ⇑(p.comp f) = ⇑p ∘ ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- `@[simp]`-normal form of `multicofork_ι_app_right`.  -/
CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R),
  CategoryTheory.Limits.colimit.ι I.multispan (CategoryTheory.Limits.WalkingMultispan.right b) =
    CategoryTheory.Limits.Multicoequalizer.π I b
-- Lean.Environment
Lean.instBEqConstantKind.beq : Lean.ConstantKind → Lean.ConstantKind → Bool
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unzeroD_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithZero α} {a b : α}, (x = 0 → a < b) → (WithZero.unzeroD a x < b ↔ x < ↑b)
-- Mathlib.Analysis.Convex.Join
convexJoin_singletons : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {y : E} (x : E), convexJoin 𝕜 {x} {y} = segment 𝕜 x y
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimit_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ Cᵒᵖ) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.unop.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.unop.comp CategoryTheory.yoneda) ⟶ F) (i : Iᵒᵖ),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitYonedaHomIsoLimit D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (D.obj i)))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.unop.comp CategoryTheory.yoneda) (Opposite.unop i)).app (D.obj i)))
            (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j)
      (HomologicalComplex.singleObjCyclesSelfIso c j B).hom =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom f
-- Mathlib.Order.SuccPred.Archimedean
Succ.rec_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {p : α → Prop},
  (∀ (a : α), p a ↔ p (Order.succ a)) → ∀ {a b : α}, a ≤ b → (p a ↔ p b)
-- Mathlib.Data.PFun
PFun.Preimage_def : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.preimage s = {x | ∃ y ∈ s, y ∈ f x}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeFunctorObjEvaluationOfHasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : LinearOrder J]
  [CategoryTheory.Limits.HasIterationOfShape J C] (K : Type u_1) [inst_3 : CategoryTheory.Category.{v_1, u_1} K]
  (X : K), CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J ((CategoryTheory.evaluation K C).obj X)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil.hcongr_3 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' → ∀ (u : V) (u' : V'), u ≍ u' → SimpleGraph.Walk.nil ≍ SimpleGraph.Walk.nil
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coord.eq_1 : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι), b.coord i = Finsupp.lapply i ∘ₗ ↑b.repr
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint32 : Lean.IR.IRType
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_option_toFinset : ∀ {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β), ⋂ x ∈ o.toFinset, f x = ⋂ x ∈ o, f x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every kernel of `f` induces a kernel of `f ≫ g` if `g` is mono.  -/
CategoryTheory.Limits.isKernelCompMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork f} →
            CategoryTheory.Limits.IsLimit c →
              {Z : C} →
                (g : Y ⟶ Z) →
                  [hg : CategoryTheory.Mono g] →
                    {h : X ⟶ Z} →
                      (hh : h = CategoryTheory.CategoryStruct.comp f g) →
                        CategoryTheory.Limits.IsLimit
                          (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c) ⋯)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The Hecke ring `𝕋 Δ H Z` with coefficients in `Z`: the diagonal Hecke coset module
`HeckeCosetModule Δ H H Z`, the finitely-supported `Z`-linear combinations of double cosets
`H\Δ/H`. The convolution product making it a ring is developed in later files.  -/
HeckeCosetModule.term𝕋 : Lean.ParserDescr
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.algebraMap_mem : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) (x : F),
  (algebraMap F E) x ∈ IntermediateField.adjoin F S
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.R.sound : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (m n : ℕ) (x y : K),
  (⇑(frobenius K p))^[m] x = y → PerfectClosure.mk K p (n, x) = PerfectClosure.mk K p (m + n, y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : Inhabited α] [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.union m₂).getKey! k = m₂.getKey! k
-- Mathlib.Data.Complex.Basic
Complex.reProdIm_eq_empty : ∀ {s t : Set ℝ}, s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Computability.EpsilonNFA
εNFA.stepSet.eq_1 : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α), M.stepSet S a = ⋃ s ∈ S, M.εClosure (M.step s (some a))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval_πs : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}},
  (∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) →
    (Profinite.NobelingProof.πs C o)
        (Profinite.NobelingProof.Products.eval
          (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) l) =
      Profinite.NobelingProof.Products.eval C l
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleMk (-f) h = -CochainComplex.HomComplex.Cochain.toSingleMk f h
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.positionsFrom_endPos : ∀ {s : String.Slice}, String.Slice.Model.positionsFrom s.endPos = []
-- Mathlib.Analysis.Calculus.Deriv.Star
HasDerivAtFilter.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F}
  [TrivialStar 𝕜] {L : Filter (𝕜 × 𝕜)}, HasDerivAtFilter f f' L → HasDerivAtFilter (fun x => star (f x)) (star f') L
-- Lean.LocalContext
Lean.LocalContext.decls : Lean.LocalContext → Lean.PersistentArray (Option Lean.LocalDecl)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_ofReal_nhds_top : ∀ {α : Type u_1} {f : α → ℝ} {l : Filter α},
  Filter.Tendsto (fun x => ENNReal.ofReal (f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.Data.Finsupp.Notation
/-- Implementation detail for `fun₀`, used by both `Finsupp` and `DFinsupp`  -/
Finsupp.Internal.stxSingle₀ : Lean.ParserDescr