mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)),
  (CategoryTheory.PreOneHypercover.cylinder f g).p₂ k =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
          (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
            (F.toPullback p.snd))
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯)
            (F.toPullback q.snd))
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯))
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g q.snd))
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.norm_integral_le_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f : ↥(α →₁ₛ[μ] E)), ‖MeasureTheory.L1.SimpleFunc.integral f‖ ≤ ‖f‖
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.hi? : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval → Option Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Mathlib.Algebra.Order.Group.Synonym
toColex_neg : ∀ {α : Type u_1} [inst : Neg α] (a : α), toColex (-a) = -toColex a
-- Mathlib.CategoryTheory.Category.Preorder
/-- Express an inequality as a morphism in the corresponding preorder category.  -/
LE.le.hom : {X : Type u_1} → [inst : Preorder X] → {x y : X} → x ≤ y → (x ⟶ y)
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.rightOp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Dᵒᵖ C} (a : F.rightOp ⊣ G),
  a.rightOp.unit = CategoryTheory.NatTrans.unop a.counit
-- Mathlib.Data.List.GetD
List.getI_append_right : ∀ {α : Type u} [inst : Inhabited α] (l l' : List α) (n : ℕ), l.length ≤ n → (l ++ l').getI n = l'.getI (n - l.length)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- If a model with corners has full range, the `convex_range'` condition is satisfied.  -/
ModelWithCorners.ofTargetUniv : (𝕜 : 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] →
              (φ : PartialEquiv H E) →
                φ.source = Set.univ → φ.target = Set.univ → Continuous ↑φ → Continuous ↑φ.symm → ModelWithCorners 𝕜 E H
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv_eq.match_1.eq_3 : ∀ (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, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_3 ()
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Vector.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The universal cover of the classifying space of `G` as a simplicial set, augmented by the map
from `Fin 1 → G` to the terminal object in `Type u`, has an extra degeneracy.  -/
classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmented : (G : Type u) → [inst : Monoid G] → (classifyingSpaceUniversalCover.compForgetAugmented G).ExtraDegeneracy
-- Mathlib.Algebra.Homology.Single
/-- Morphisms from a single object cochain complex with `X` concentrated in degree 0
to an `ℕ`-indexed cochain complex `C`
are the same as morphisms `f : X ⟶ C.X 0` such that `f ≫ C.d 0 1 = 0`.  -/
CochainComplex.fromSingle₀Equiv : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : CochainComplex V ℕ) →
          (X : V) → ((CochainComplex.single₀ V).obj X ⟶ C) ≃ { f // CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0 }
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.squareToSnd_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {i : CategoryTheory.Arrow C} {f : X ⟶ Y}
  {g : Y ⟶ Z} (sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)),
  (CategoryTheory.Arrow.squareToSnd sq).right = CategoryTheory.Arrow.Hom.right sq
-- Init.Data.List.TakeDrop
List.take_set : ∀ {α : Type u_1} {l : List α} {i j : ℕ} {a : α}, List.take i (l.set j a) = (List.take i l).set j a
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_uIcc_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.uIcc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.uIcc a b, f i.castSucc
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.toAddSubgroup_closure : ∀ {G : Type u_1} [inst : Group G] (S : Set G),
  Subgroup.toAddSubgroup (Subgroup.closure S) = AddSubgroup.closure (⇑Additive.toMul ⁻¹' S)
-- Mathlib.Analysis.Convex.Join
convexJoin_segment_singleton : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (a b c : E),
  convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜) {a, b, c}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  t.WF →
    Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.map f t) k fallback =
      (Option.map (f k) (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_connected : ∀ {n : ℕ}, (SimpleGraph.cycleGraph (n + 1)).Connected
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_one' : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] [IsCancelMulZero S] {R : Type u_6} [inst_3 : Semiring R]
  [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv], abv 1 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `G` preserves colimits,
we have an isomorphism from the image of a coproduct to the coproduct of the images.
 -/
CategoryTheory.Limits.PreservesCoproduct.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [inst_2 : CategoryTheory.Limits.HasCoproduct f] →
                [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] →
                  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] →
                    G.obj (∐ f) ≅ ∐ fun j => G.obj (f j)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_4 : ∀ (f fs : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal (f.cons fs) = fun k v =>
    Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.cons₁ fs v k) v
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instModule : {k : Type u_1} →
  {G : Type u_2} →
    {S : Type u_3} → [inst : Semiring S] → [inst_1 : AddCommMonoid k] → [Module S k] → Module S (SkewMonoidAlgebra k G)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ne_ones_iff : ∀ {n : ℕ} {c : Composition n}, c ≠ Composition.ones n ↔ ∃ i ∈ c.blocks, 1 < i
-- Init.Data.Rat.Lemmas
Rat.lt_iff_le_and_ne : ∀ {a b : ℚ}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Lift a functor `F : C ⥤ D` to `WithTerminal C ⥤ D`.  -/
CategoryTheory.WithTerminal.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → F.obj x ⟶ Z) →
              (∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) →
                CategoryTheory.Functor (CategoryTheory.WithTerminal C) D
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A symmetric bilinear form is characterized by the values it takes on the diagonal.  -/
LinearMap.BilinForm.ext_iff_of_isSymm : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_8} [inst_1 : Field R] [NeZero 2] [inst_3 : Module R M]
  {B C : LinearMap.BilinForm R M}, B.IsSymm → C.IsSymm → (B = C ↔ ∀ (x : M), (B x) x = (C x) x)
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The line derivative as a continuous linear map.  -/
LineDeriv.lineDerivOpCLM : (R : Type u_4) →
  {V : Type u_5} →
    (E : Type u_6) →
      {F : Type u_7} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module R E] →
              [inst_3 : AddCommGroup F] →
                [inst_4 : Module R F] →
                  [inst_5 : TopologicalSpace E] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : AddCommGroup V] →
                        [inst_8 : LineDeriv V E F] →
                          [LineDerivAdd V E F] → [LineDerivSMul R V E F] → [ContinuousLineDeriv V E F] → V → E →L[R] F
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Another name for the identity function `G → G`, to help type checking.  -/
_private.Mathlib.GroupTheory.FreeGroup.NielsenSchreier.0.IsFreeGroupoid.symgen : {G : Type u} → [inst : CategoryTheory.Groupoid G] → G → Quiver.Symmetrify (IsFreeGroupoid.Generators G)
-- Mathlib.Data.Set.Semiring
SetSemiring.down_imageHom : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (s : SetSemiring α),
  SetSemiring.down ((SetSemiring.imageHom f) s) = ⇑f '' SetSemiring.down s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeArrowLeftFuncOfHasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : LinearOrder J]
  [CategoryTheory.Limits.HasIterationOfShape J C],
  CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J CategoryTheory.Arrow.leftFunc
-- Init.Data.Order.FactoriesExtra
Std.compare_eq_gt : ∀ {α : Type u} [inst : Ord α] [inst_1 : LT α] [inst_2 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderLT α] {a b : α},
  compare a b = Ordering.gt ↔ b < a
-- Mathlib.Data.ENat.Lattice
/-- If `a ≠ 0`, then right multiplication by `a` maps infimum to infimum.
See also `ENat.iInf_mul` that assumes `[Nonempty ι]` but does not require `a ≠ 0`.  -/
ENat.mul_iInf_of_ne : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, a ≠ 0 → a * ⨅ i, f i = ⨅ i, a * f i
-- Init.Data.List.Lemmas
List.foldr_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β},
  List.foldr (fun x1 x2 => f x1 ++ x2) l' l = (List.map f l).flatten ++ l'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_mul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_mul._auto_1 →
    autoParam (ContinuousOn g (spectrum R a)) cfc_mul._auto_3 → cfc (fun x => f x * g x) a = cfc f a * cfc g a
-- Mathlib.Topology.Compactness.Lindelof
/-- The intersection of a closed set and a Lindelöf set is a Lindelöf set.  -/
IsLindelof.inter_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof t → IsClosed s → IsLindelof (s ∩ t)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `b` is odd, then `J(2 | b)` is given by `χ₈ b`.  -/
jacobiSym.at_two : ∀ {b : ℕ}, Odd b → jacobiSym 2 b = ZMod.χ₈ ↑b
-- Mathlib.Topology.Order.LeftRightLim
tendsto_leftLim_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [h'α : OrderTopology α] {f : α → β} {a : α},
  (∃ y, Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y)) →
    Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds (Function.leftLim f a))
-- Mathlib.Algebra.Ring.ULift
ULift.addMonoidWithOne : {R : Type u} → [AddMonoidWithOne R] → AddMonoidWithOne (ULift.{u_1, u} R)
-- Mathlib.Combinatorics.Colex
Finset.Colex.insert_lt_insert : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} [inst_1 : DecidableEq α],
  a ∉ s → b ∉ s → (toColex (insert a s) < toColex (insert b s) ↔ a < b)
-- Mathlib.Algebra.Category.Grp.Colimits
AddEquiv.ofBijective.congr_simp : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f f_1 : F) (e_f : f = f_1) (hf : Function.Bijective ⇑f),
  AddEquiv.ofBijective f hf = AddEquiv.ofBijective f_1 ⋯
-- Mathlib.Topology.UniformSpace.Basic
IsOpen.relImage : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsOpen s → ∀ {t : Set α}, IsOpen (s.image t)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
/-- Club sets in regular cardinals correspond one to one with normal functions.  -/
Order.isNormal_enum_iff_isClub : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s}, Order.IsNormal (Subtype.val ∘ ⇑(Order.enum s hs)) ↔ IsClub s
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_sum_map : ∀ {𝕜 : 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] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞} {E' : Type u_17} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_18} [inst_10 : TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'}
  {N : Type u_20} {N' : Type u_21} [inst_11 : TopologicalSpace N] [inst_12 : TopologicalSpace N']
  [inst_13 : ChartedSpace H' N] [inst_14 : ChartedSpace H' N'] {f : M → N} {g : M' → N'},
  ContMDiff I J n (Sum.map f g) ↔ ContMDiff I J n f ∧ ContMDiff I J n g
-- Init.Prelude
/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`)  -/
SMul : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_zero : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  MonoidAlgebra.map f 0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂)[k]! = t₁[k]!
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.fst_comp_quotientMulEquivQuotientProd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J),
  (RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.Functor.mapShortComplex_obj : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C), F.mapShortComplex.obj S = S.map F
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (q : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h q).support = u :: q.support
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.ext_iff : ∀ {n : ℕ} {x y : CompositionAsSet n}, x = y ↔ x.boundaries = y.boundaries
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.toListRev_append : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β},
  (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_hom_right : ∀ {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} (α : F ≅ G) {X : C} {Y : D} (g g' : Y ⟶ F.obj X),
  CategoryTheory.CategoryStruct.comp g (α.hom.app X) = CategoryTheory.CategoryStruct.comp g' (α.hom.app X) ↔ g = g'
-- Mathlib.Logic.Equiv.Defs
Equiv.surjective_comp : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower' : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsScalarTower R (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.shape_R : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S : J.Cover X), S.shape.R = S.Relation
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.yoneda_obj_isGeneratedBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.PresheafIsGeneratedBy (CategoryTheory.yoneda.obj X) fun x => CategoryTheory.CategoryStruct.id X
-- Init.Data.SInt.Lemmas
instAssociativeInt32HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.Dual.order : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L] [Finite P]
  [Finite L],
  Configuration.ProjectivePlane.order (Configuration.Dual L) (Configuration.Dual P) =
    Configuration.ProjectivePlane.order P L
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isLocallyFull' : ∀ {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} (J : CategoryTheory.GrothendieckTopology C)
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D}
  [self : CategoryTheory.Functor.IsDenseSubsite J K G], G.IsLocallyFull K
-- Mathlib.Topology.Connected.Basic
isPreconnected_range : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [PreconnectedSpace α] {f : α → β},
  Continuous f → IsPreconnected (Set.range f)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.zero_lt_orderTop_of_order : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
  0 < x.order → 0 < x.orderTop
-- Mathlib.Order.Lattice
Prod.instMax_mathlib.eq_1 : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β],
  Prod.instMax_mathlib α β = { max := fun p q => (p.1 ⊔ q.1, p.2 ⊔ q.2) }
-- Mathlib.Data.List.Sigma
List.mem_keys_of_mem_keys_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)},
  a₁ ∈ (List.kerase a₂ l).keys → a₁ ∈ l.keys
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList.eq_1 : ∀ {α : Type u} (f : List α → List α) (invariant : ∀ (l : List α), f l = f [] ++ l),
  { apply := f, invariant := invariant }.toList = f []
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Recursor for `WithOne` using the preferred forms `1` and `↑a`.  -/
WithOne.recOneCoe : {α : Type u} → {motive : WithOne α → Sort u_1} → motive 1 → ((a : α) → motive ↑a) → (n : WithOne α) → motive n
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_obj_map : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) (X_1 : CategoryTheory.Functor J₂ C)
  (X_2 : J₁) {X_3 Y : J₂} (f : X_3 ⟶ Y),
  ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).obj X_1).obj X_2).map f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.obj X_2) (X_1.map f)
-- Mathlib.Data.Set.Lattice
Set.iInter₂_subset : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
  ⋂ i, ⋂ j, s i j ⊆ s i j
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) (d : δ)
  (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β)
  (h_1 : (d : δ) → motive d Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (d : δ) →
      (a : α) →
        (b : β a) →
          (es : Std.DHashMap.Internal.AssocList α β) → motive d (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match d, Std.DHashMap.Internal.AssocList.cons a b es with
    | d, Std.DHashMap.Internal.AssocList.nil => h_1 d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => h_2 d a b es) =
    h_2 d a b es
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Neg β]
  [inst_3 : ContinuousNeg β] (f : C(α, β)), ⇑(-f) = -⇑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : β → β}, (t.modify k f)[k']? = if cmp k k' = Ordering.eq then Option.map f t[k]? else t[k']?
-- Init.Grind.Order
Lean.Grind.Order.le_eq_false_of_lt_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] (a b : α) (k₁ k₂ : ℤ),
  (k₂ + k₁).ble' 0 = true → a < b + ↑k₁ → (b ≤ a + ↑k₂) = False
-- Mathlib.Algebra.Homology.ComplexShape
/-- A `c : ComplexShape ι` describes the shape of a chain complex,
with chain groups indexed by `ι`.
Typically `ι` will be `ℕ`, `ℤ`, or `Fin n`.

There is a relation `Rel : ι → ι → Prop`,
and we will only allow a non-zero differential from `i` to `j` when `Rel i j`.

There are axioms which imply `{ j // c.Rel i j }` and `{ i // c.Rel i j }` are subsingletons.
This means that the shape consists of some union of lines, rays, intervals, and circles.

Below we define `c.next` and `c.prev` which provide these related elements.
 -/
ComplexShape : Type u_1 → Type u_1
-- Init.Data.Option.Array
Option.forIn_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (o : Option α) (b : β)
  (f : α → β → m (ForInStep β)), forIn o.toArray b f = forIn o b f