mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse_equiv_comp : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {e : M₂ ≃L[R] M₃} {f : M →L[R] M₂}, (↑e ∘SL f).inverse = f.inverse ∘SL ↑e.symm
-- Qq.Match
Qq.Impl.PatternVar.stx : Qq.Impl.PatternVar → Lean.Term
-- Init.Data.String.Length
String.length_toList : ∀ {s : String}, s.toList.length = s.length
-- Mathlib.Order.Hom.Bounded
BotHom.mk : {α : Type u_6} → {β : Type u_7} → [inst : Bot α] → [inst_1 : Bot β] → (toFun : α → β) → toFun ⊥ = ⊥ → BotHom α β
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c)
  [CategoryTheory.Epi f], CategoryTheory.Limits.IsZero c.pt
-- Mathlib.Data.Set.Basic
Set.mem_union_left : ∀ {α : Type u} {x : α} {a : Set α} (b : Set α), x ∈ a → x ∈ a ∪ b
-- Mathlib.Analysis.Normed.Module.Shrink
Shrink.instSeminormedAddCommGroup : {α : Type u_3} → [inst : Small.{v, u_3} α] → [SeminormedAddCommGroup α] → SeminormedAddCommGroup (Shrink.{v, u_3} α)
-- Init.Data.Vector.Lemmas
Vector.mem_ite_empty_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : Vector α 0}, (x ∈ if p then #v[] else xs) ↔ ¬p ∧ x ∈ xs
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Defs.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.Order.Hom.Basic
/-- Construct a bundled monotone map `α →o Π i, π i` from a family of monotone maps
`f i : α →o π i`.  -/
OrderHom.pi : {α : Type u_2} →
  [inst : Preorder α] →
    {ι : Type u_6} →
      {π : ι → Type u_7} → [inst_1 : (i : ι) → Preorder (π i)] → ((i : ι) → α →o π i) → α →o (i : ι) → π i
-- Mathlib.Algebra.Lie.Basic
LieHom.id_apply : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] (x : L₁),
  LieHom.id x = x
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_hom : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] (l : List M) {F : Type u_8}
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F), (List.map (⇑f) l).sum = f l.sum
-- Lean.Meta.Tactic.Grind.PropagatorAttr
_private.Lean.Meta.Tactic.Grind.PropagatorAttr.0.Lean.Meta.Grind.addBuiltin : Lean.Name → Lean.Syntax → Lean.AttrM Unit
-- Mathlib.Algebra.CharP.Two
CharTwo.intCast_cases : ∀ (R : Type u_1) [inst : Ring R] [CharP R 2] (n : ℤ), ↑n = 0 ∨ ↑n = 1
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.term.inj : ∀ {term term_1 : Lean.Term}, Aesop.RuleTerm.term term = Aesop.RuleTerm.term term_1 → term = term_1
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- **Alias** of `RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependent`.

---

Note that it is often more convenient to use `RootPairing.root_add_zsmul_mem_range_iff` than
to invoke this lemma directly.  -/
RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : CommRing R] [CharZero R] [IsDomain R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∃ q ≤ 0, ∃ p ≥ 0, {z | P.root j + z • P.root i ∈ Set.range ⇑P.root} = Set.Icc q p
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.mk.sizeOf_spec : ∀ (arr : Array Batteries.UFNode) (parentD_lt : ∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size)
  (rankD_lt :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr i ≠ i →
        Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)),
  sizeOf { arr := arr, parentD_lt := parentD_lt, rankD_lt := rankD_lt } = 1 + sizeOf arr
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.mk.sizeOf_spec : ∀ (state : Std.Mutex Std.Http.Body.Channel.State✝), sizeOf { state := state } = 1 + sizeOf state
-- Mathlib.Order.Filter.Prod
Filter.prod_map_map_eq : ∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁}
  {m₂ : α₂ → β₂}, Filter.map m₁ f₁ ×ˢ Filter.map m₂ f₂ = Filter.map (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions within domains at points is `C^n`.  -/
ContMDiffWithinAt.comp : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''} (x : M),
  ContMDiffWithinAt I' I'' n g t (f x) →
    ContMDiffWithinAt I I' n f s x → Set.MapsTo f s t → ContMDiffWithinAt I I'' n (g ∘ f) s x
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.hasMFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → s ∈ nhds x → HasMFDerivAt% f x f'
-- Mathlib.Analysis.Complex.AbelLimit
/-- **Abel's limit theorem**. Given a real power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 from the left.  -/
Real.tendsto_tsum_powerSeries_nhdsWithin_lt : ∀ {f : ℕ → ℝ} {l : ℝ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    Filter.Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds l)
-- Mathlib.Logic.IsEmpty.Defs
PProd.isEmpty_right : ∀ {α : Sort u} {β : Sort v} [IsEmpty β], IsEmpty (α ×' β)
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_id : ∀ {V : Type u₁} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), (𝟭q V).mapPath p = p
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R},
  g.IsDistinguishedAt I →
    PowerSeries.constantCoeff h ∉ I → f = ↑g * h → ↑g.natDegree = ((PowerSeries.map (Ideal.Quotient.mk I)) f).order
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {s : Set E}
  {x v : E},
  LineDifferentiableWithinAt 𝕜 f s x v → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → LineDifferentiableWithinAt 𝕜 f₁ s x v
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitπ₃ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₃
-- Init.Data.String.Lemmas.Splits
String.splits_prevn_endPos : ∀ (s : String) (n : ℕ),
  (s.endPos.prevn n).Splits (String.ofList (List.take (s.toList.length - n) s.toList))
    (String.ofList (List.drop (s.toList.length - n) s.toList))
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuousAt_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] {f : OnePoint X → Y},
  ContinuousAt f OnePoint.infty ↔
    ∀ s ∈ nhds (f OnePoint.infty), ∃ t, IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid.eq_1 : unitInterval.sigmoid = Subtype.coind Real.sigmoid unitInterval.sigmoid._proof_1
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_taylor : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R) (r s : R),
  (Polynomial.taylor r) ((Polynomial.taylor s) f) = (Polynomial.taylor (r + s)) f
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeries_summable_aux₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ↑r < p.radius → ∀ (k : ℕ), Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
-- Std.Data.TreeSet.Raw.Basic
/-- Internal implementation detail of the tree map.  -/
Std.TreeSet.Raw.WF.out : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.WF → t.inner.WF
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_mul_of_pos_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), 0 < b → (a * b).tdiv (c * b) = a.tdiv c
-- Mathlib.Topology.Gluing
TopCat.GlueData.π_surjective : ∀ (D : TopCat.GlueData), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom D.π)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstanceSet : Type
-- Mathlib.Algebra.Regular.Basic
/-- An element admitting a right inverse is right-regular.  -/
isRightRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, a * b = 1 → IsRightRegular a
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y),
  hF.homEquiv.symm f = hF.preimage f
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_map_le : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M),
  Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_multiset_prod : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R ≃+* S) (s : Multiset R),
  f s.prod = (Multiset.map (⇑f) s).prod
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  MeasureTheory.addFundamentalFrontier G s ∪ MeasureTheory.addFundamentalInterior G s = s
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.mk.inj : ∀ {lctx : Lean.LocalContext} {stx output : Lean.Syntax} {lctx_1 : Lean.LocalContext} {stx_1 output_1 : Lean.Syntax},
  { lctx := lctx, stx := stx, output := output } = { lctx := lctx_1, stx := stx_1, output := output_1 } →
    lctx = lctx_1 ∧ stx = stx_1 ∧ output = output_1
-- Mathlib.RepresentationTheory.Rep.Res
Rep.coe_res_obj_ρ' : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  (M : Rep.{u_1, u, v1} k G) (h : H), (Rep.res f M).ρ h = M.ρ (f h)
-- Init.Data.Ord.Basic
Ordering.not_isLE_eq_isGT : ∀ {o : Ordering}, (!o.isLE) = o.isGT
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- **Alias** of the forward direction of `hasLineDerivAt_iff_tendsto_slope_zero`. -/
HasLineDerivAt.tendsto_slope_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E},
  HasLineDerivAt 𝕜 f f' x v → Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')
-- Mathlib.RingTheory.Ideal.Pure
Ideal.ker_piRingHom_atPrime_eq_of_pure : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [I.Pure],
  RingHom.ker (RingHom.pi fun p => algebraMap R (Localization.AtPrime (↑p).asIdeal)) = I
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- The quadratic form agrees across the map.  -/
QuadraticMap.Isometry.map_app' : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (self : Q₁ →qᵢ Q₂) (m : M₁),
  Q₂ (self.toFun m) = Q₁ m
-- Mathlib.CategoryTheory.Limits.Fubini
/-- A variant of the Fubini theorem for a functor `G : J × K ⥤ C`,
showing that $\colim_k \colim_j G(j,k) ≅ \colim_j \colim_k G(j,k)$.
 -/
CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] →
                  [inst_5 :
                      CategoryTheory.Limits.HasColimit
                        ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] →
                    CategoryTheory.Limits.colimit
                        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp
                          CategoryTheory.Limits.colim) ≅
                      CategoryTheory.Limits.colimit
                        ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.mk.inj : ∀ {A : Type} {inst : MetricSpace A} {Space : Type} {metric : MetricSpace Space} {embed : A → Space}
  {isom : Isometry embed} {Space_1 : Type} {metric_1 : MetricSpace Space_1} {embed_1 : A → Space_1}
  {isom_1 : Isometry embed_1},
  { Space := Space, metric := metric, embed := embed, isom := isom } =
      { Space := Space_1, metric := metric_1, embed := embed_1, isom := isom_1 } →
    Space = Space_1 ∧ metric ≍ metric_1 ∧ embed ≍ embed_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cone.functorialityEquivalence F e).inverse =
    (CategoryTheory.Limits.Cone.functoriality (F.comp e.functor) e.inverse).comp
      (CategoryTheory.Limits.Cone.postcomposeEquivalence
          (F.associator e.functor e.inverse ≪≫ F.isoWhiskerLeft e.unitIso.symm ≪≫ F.rightUnitor)).functor
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.iff_of_isFractionRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_4)
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : Algebra S K] [IsScalarTower R S K] [FaithfulSMul R S]
  [IsFractionRing S K] {x : S}, IsStronglyTranscendental R x ↔ Transcendental R ((algebraMap S K) x)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.cons_append : ∀ {α : Type u} [inst : DecidableEq α] {a b : α × Bool} (L : List (α × Bool)),
  FreeAddGroup.reduceCyclically (a :: (L ++ [b])) =
    if b.1 = a.1 ∧ (!b.2) = a.2 then FreeAddGroup.reduceCyclically L else a :: L ++ [b]
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits, then `F : C ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Variant of `get?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Internal.Raw₀.Const.get?_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ}
  {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.map f m) k =
    Option.pmap (fun v h' => f (m.getKey k h') v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.mk.inj : ∀ {H : Type u} {inst : TopologicalSpace H} {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6}
  {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace M'} {inst_3 : ChartedSpace H M} {inst_4 : ChartedSpace H M'}
  {toHomeomorph : M ≃ₜ M'}
  {mem_groupoid :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G}
  {toHomeomorph_1 : M ≃ₜ M'}
  {mem_groupoid_1 :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph_1.toOpenPartialHomeomorph.trans c') ∈ G},
  { toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid } =
      { toHomeomorph := toHomeomorph_1, mem_groupoid := mem_groupoid_1 } →
    toHomeomorph = toHomeomorph_1
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.instNorm.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M},
  QuotientAddGroup.instNorm = { norm := ⇑QuotientAddGroup.addGroupSeminorm }
-- Mathlib.Algebra.Algebra.Spectrum.Pi
Pi.quasispectrum_eq : ∀ {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [Nonempty ι] [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalRing (κ i)] [inst_2 : (i : ι) → Module R (κ i)] (a : (i : ι) → κ i),
  quasispectrum R a = ⋃ i, quasispectrum R (a i)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₃.HasTensor X₄] [inst_4 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_5 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) (i₂₃₄ : I) (hi : i₂ + i₃ + i₄ = i₂₃₄),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ i₁)
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁
        (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)) i₁
        i₂₃₄ j ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K L : CochainComplex C ℤ} {n₂ n₃ n₂₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₂₃ : n₂ + n₃ = n₂₃),
  (z₁.comp z₂ ⋯).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_sub_sum_range : ∀ {G : Type u_4} [inst : AddCommGroup G] {f : ℕ → G} {n m : ℕ},
  n ≤ m → ∑ k ∈ Finset.range m, f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m with n ≤ k, f k
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- The sieve generated by `presieveOfCovering U` is a member of the Grothendieck topology.
 -/
TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology : ∀ {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X),
  CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCovering U) ∈ (Opens.grothendieckTopology ↑X) (iSup U)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.nsmul_add_addSubgroupClosure : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G},
  s.Nonempty → ∀ (n : ℕ), n • s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
-- Init.Data.SInt.Lemmas
ISize.toInt.eq_1 : ∀ (i : ISize), i.toInt = i.toBitVec.toInt
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.orderOf_one_add_mul_prime : ∀ {p : ℕ}, Nat.Prime p → p ≠ 2 → ∀ (a : ℤ), ¬↑p ∣ a → ∀ (n : ℕ), orderOf (1 + ↑p * ↑a) = p ^ n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.mk_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (b : CategoryTheory.Bicategory.Adj B), { obj := b.obj } = b
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int64.ofInt 48 = 48`
* `Int64.ofInt (-40_000) = -40_000`
* `Int64.ofInt 2_147_483_648 = 2_147_483_648`
* `Int64.ofInt (-2_147_483_649) = -2_147_483_649`
* `Int64.ofInt 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808`
* `Int64.ofInt (-9_223_372_036_854_775_809) = 9_223_372_036_854_775_807`
 -/
Int64.ofInt : ℤ → Int64
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is a faithfully-flat `A`-algebra, every ideal in `A` is the preimage of some ideal
in `B`.  -/
Ideal.comap_surjective_of_faithfullyFlat : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B], Function.Surjective (Ideal.comap (algebraMap A B))
-- Lean.Meta.Closure
Lean.Meta.Closure.State.visitedExpr : Lean.Meta.Closure.State → Lean.ExprStructMap Lean.Expr
-- Init.Data.UInt.Bitwise
UInt64.neg_one_or : ∀ {a : UInt64}, -1 ||| a = -1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions.mk.injEq : ∀ (toWorkDoneProgressOptions toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions),
  ({ toWorkDoneProgressOptions := toWorkDoneProgressOptions } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1 }) =
    (toWorkDoneProgressOptions = toWorkDoneProgressOptions_1)
-- Mathlib.Topology.Connected.PathConnected
/-- The quotient topology on path components.  -/
ZerothHomotopy.instTopologicalSpace : {X : Type u_1} → [inst : TopologicalSpace X] → TopologicalSpace (ZerothHomotopy X)