mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → β → α` of functions between uniform spaces is *uniformly equicontinuous* if,
for all entourages `U ∈ 𝓤 α`, there is an entourage `V ∈ 𝓤 β` such that, whenever `x` and `y` are
`V`-close, we have that, *for all `i : ι`*, `F i x` is `U`-close to `F i y`.  -/
UniformEquicontinuous : {ι : Type u_1} → {α : Type u_6} → {β : Type u_8} → [uα : UniformSpace α] → [uβ : UniformSpace β] → (ι → β → α) → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.prod_fst_snd : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β],
  (MulActionHom.fst M α β).prod (MulActionHom.snd M α β) = MulActionHom.id M
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑s),
  ↑((Equiv.Set.rangeSplittingImageEquiv f s).symm x) = Set.rangeSplitting f ↑x
-- Init.Data.UInt.Bitwise
UInt8.shiftRight_or : ∀ {a b c : UInt8}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Twisting `u` by `fiberPerm h b` yields an inclusion of `A` into `selfProd F X`.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProdPermIncl : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X A : C} →
            {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} →
              {a : (F.obj A).obj} →
                (CategoryTheory.ConcreteCategory.hom (F.map u)) a =
                    CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X →
                  [CategoryTheory.PreGaloisCategory.IsConnected A] →
                    (F.obj A).obj → (A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.shift.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), p.shift n = (p n.succ).curryRight
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.ext.sizeOf_spec : ∀ (ext₁? : Option Lean.Meta.SimpExtension) (ext₂? : Option Lean.Meta.Simp.SimprocExtension)
  (h : (ext₁?.isSome || ext₂?.isSome) = true),
  sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.ext ext₁? ext₂? h) = 1 + sizeOf ext₁? + sizeOf ext₂? + sizeOf h
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mem_support : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) {v : V}, v ∈ H.support ↔ ∃ w, H.Adj v w
-- Init.Data.Nat.Dvd
Nat.dvd_sub_iff_left : ∀ {m n k : ℕ}, k ≤ n → m ∣ k → (m ∣ n - k ↔ m ∣ n)
-- Mathlib.Data.Fin.Rev
Fin.rev_castPred : ∀ {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) (h' : optParam (i.rev ≠ 0) ⋯), (i.castPred h).rev = i.rev.pred h'
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.leftHomologyFunctor C).map φ = CategoryTheory.ShortComplex.leftHomologyMap φ
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn : ∀ {x : ℝ}, 1 < x → DifferentiableAt ℝ (fun z => 1 - AkraBazziRecurrence.smoothingFn z) x
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instStarAddMonoid : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              [inst_5 : StarRing 𝕜] →
                [inst_6 : StarRing A] → [StarModule 𝕜 A] → [NormedStarGroup A] → StarAddMonoid (DoubleCentralizer 𝕜 A)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The universal factorization ring represents
`S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S"`.  -/
Polynomial.UniversalCoprimeFactorizationRing.homEquiv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {n : ℕ} →
            (m k : ℕ) →
              (hn : n = m + k) →
                (p : Polynomial.MonicDegreeEq R n) →
                  (Polynomial.UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) ≃
                    { q // ↑q.1 * ↑q.2 = Polynomial.map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
-- Init.Data.Dyadic.Basic
Dyadic.roundUp.eq_2 : ∀ (prec n k : ℤ) (hn : n % 2 = 1),
  (Dyadic.ofOdd n k hn).roundUp prec =
    match k - prec with
    | Int.ofNat l => Dyadic.ofIntWithPrec (-(-n) >>> l) prec
    | Int.negSucc a => Dyadic.ofOdd n k hn
-- Mathlib.Analysis.CStarAlgebra.Basic
nnnorm_star : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x : E),
  ‖star x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Normed.Group.Uniform
MonoidHomClass.uniformContinuous_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ), (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → UniformContinuous ⇑f
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {P : CategoryTheory.MorphismProperty C} →
        {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} →
          {X Y : C} → {x : X ⟶ Y} → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- When `P` ranges over finitely generated submodules of `M`,
the modules of the form `P ⊗[R] N` form a directed system.  -/
Submodule.FG.rTensor.directedSystem : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  DirectedSystem (fun P => TensorProduct R (↥↑P) N) fun ⦃x x_1⦄ h => ⇑(LinearMap.rTensor N (Submodule.inclusion h))
-- Mathlib.Topology.Algebra.ConstMulAction
interior_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → ∀ (s : Set α), interior (c • s) = c • interior s
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_union_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s ≠ ⊤ → μ t ≠ ⊤ → μ (s ∪ t) ≠ ⊤
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  [inst_7 : StarModule R A] →
                    [inst_8 : TopologicalSpace A] →
                      [inst_9 : IsSemitopologicalSemiring A] →
                        [inst_10 : ContinuousConstSMul R A] →
                          [inst_11 : ContinuousStar A] →
                            [T2Space A] →
                              {x : A} → [IsStarNormal x] → NonUnitalCommSemiring ↥(NonUnitalStarAlgebra.elemental R x)
-- Mathlib.Topology.Hom.Open
/-- The type of continuous open maps from `α` to `β`, aka Priestley homomorphisms.  -/
«term_→CO_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_sup_left : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A} {x : A},
  x ∈ S → x ∈ S ⊔ T
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
AddSubgroup.mk.congr_simp : ∀ {G : Type u_3} [inst : AddGroup G] (toAddSubmonoid toAddSubmonoid_1 : AddSubmonoid G)
  (e_toAddSubmonoid : toAddSubmonoid = toAddSubmonoid_1)
  (neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
  { toAddSubmonoid := toAddSubmonoid, neg_mem' := neg_mem' } = { toAddSubmonoid := toAddSubmonoid_1, neg_mem' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.card_aux₂ : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {u : Finset α},
  P.IsEquipartition →
    u ∈ P.parts →
      u.card ≠
          Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
            (Fintype.card α / P.parts.card -
              Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) →
        (4 ^ P.parts.card -
                (Fintype.card α / P.parts.card -
                    Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
                  1)) *
              (Fintype.card α / SzemerediRegularity.stepBound P.parts.card) +
            (Fintype.card α / P.parts.card -
                  Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
                1) *
              (Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1) =
          u.card
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.clm_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] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f s →
      ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun x => g x ∘SL f x) s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- If `f` is a linear map from `M₁` to `M₂` that preserves the quadratic forms, and if it has
a linear retraction `g` that also preserves the quadratic forms, then `CliffordAlgebra.map g`
is a retraction of `CliffordAlgebra.map f`.  -/
CliffordAlgebra.leftInverse_map_of_leftInverse : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁),
  Function.LeftInverse ⇑g ⇑f → Function.LeftInverse ⇑(CliffordAlgebra.map g) ⇑(CliffordAlgebra.map f)
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_comp_of_mem_ball : ∀ {β : Type ub} {V W : SetRel β β} {x y z : β} [V.IsSymm],
  x ∈ UniformSpace.ball z V → y ∈ UniformSpace.ball z W → (x, y) ∈ V.comp W
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp (CochainComplex.mappingCone.snd φ)
      ⋯ =
    CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (f * f') (g * g') l s
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.div_mul_cancel_of_mod_zero : ∀ {a b : ℤ}, a % b = 0 → a / b * b = a
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_inv_assoc : ∀ {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 Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso (α.app X)]
  [inst_3 : CategoryTheory.IsIso (α.app Y)] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app Y)) h)
-- Mathlib.Computability.Partrec
Nat.rfindOpt_spec : ∀ {α : Type u_1} {f : ℕ → Option α} {a : α}, a ∈ Nat.rfindOpt f → ∃ n, a ∈ f n
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f : M → G} {x₀ : M}, ContMDiffAt I' I n f x₀ → ContMDiffAt I' I n (fun x => (f x)⁻¹) x₀
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4)
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (match Sum.inr (Sum.inr 0) :: l with
    | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
    | Sum.inr (Sum.inr 0) :: l => h_4 l
    | Sum.inr (Sum.inr 1) :: l => h_5 l
    | x => h_6 x) =
    h_4 l
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The property of preserving initial objects expressed in terms of `IsInitial`.  -/
CategoryTheory.Limits.IsInitial.isInitialObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsInitial (G.obj X)
-- Mathlib.Algebra.Order.Group.Nat
StrictMono.nat_pow : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} [inst : Preorder α], n ≠ 0 → StrictMono f → StrictMono fun x => f x ^ n
-- Mathlib.Order.Cover
covBy_iff_lt_iff_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x ⋖ y ↔ ∀ {z : α}, z < y ↔ z ≤ x
-- Mathlib.Geometry.Group.Growth.QuotientInter
Finset.le_card_quotient_mul_sq_inter_subgroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {H : Subgroup G} [inst_2 : DecidablePred fun x => x ∈ H]
  [inst_3 : H.Normal] {A : Finset G},
  A⁻¹ = A → A.card ≤ (Finset.image (⇑(QuotientGroup.mk' H)) A).card * {x ∈ A ^ 2 | x ∈ H}.card
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Init.Data.SInt.Lemmas
Int64.toInt_lt : ∀ (x : Int64), x.toInt < 2 ^ 63
-- Mathlib.Analysis.Calculus.MeanValue
Convex.isLittleO_pow_succ_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
        (f' =o[nhdsWithin x₀ s] fun x => (x - x₀) ^ n) →
          (fun x => f x - f x₀) =o[nhdsWithin x₀ s] fun x => (x - x₀) ^ (n + 1)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The centrality condition that the maps linear maps intertwine one another.  -/
DoubleCentralizer.central : ∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (self : DoubleCentralizer 𝕜 A) (x y : A), self.toProd.2 x * y = x * self.toProd.1 y
-- Mathlib.Data.Finset.Insert
Finset.singleton_injective : ∀ {α : Type u_1}, Function.Injective singleton
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.mk.injEq : ∀ (zonesPaths zonesPaths_1 : Array System.FilePath),
  ({ zonesPaths := zonesPaths } = { zonesPaths := zonesPaths_1 }) = (zonesPaths = zonesPaths_1)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `Ioc` version of `eq_coe_Ico`.  -/
AddCircle.eq_coe_Ioc : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  [Archimedean 𝕜] (a : AddCircle p), ∃ b ∈ Set.Ioc 0 p, ↑b = a
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_inv_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  LipschitzWith K f⁻¹ ↔ LipschitzWith K f
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_toAffineIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toAffineIsometry = ⇑e
-- Mathlib.Data.List.Basic
List.getLast.hcongr_3 : ∀ (α α' : Type u),
  α = α' →
    ∀ (as : List α) (as' : List α'), as ≍ as' → ∀ (a : as ≠ []) (a' : as' ≠ []), a ≍ a' → as.getLast a ≍ as'.getLast a'
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneHSMulConjActGeneralLinearGroup : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ : Subgroup (GL n R)) [Γ.HasDetOne] (g : ConjAct (GL n R)), (g • Γ).HasDetOne
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalRefine : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_id : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R), Ideal.comap (RingHom.id R) I = I
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instSMulCommClass' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] {M : Type u_3} [inst_5 : SMulZeroClass M R]
  [SMulCommClass M R R] [inst_7 : ContinuousConstSMul M R],
  SMulCommClass M (ContinuousMapZero X R) (ContinuousMapZero X R)
-- Mathlib.Data.ENat.Basic
AddMonoidHom.ENatMap_apply : ∀ {N : Type u_2} [inst : AddZeroClass N] (f : ℕ →+ N), ⇑f.ENatMap = ENat.map ⇑f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
lt_of_pow_lt_pow_left' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b : M} (n : ℕ),
  a ^ n < b ^ n → a < b
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring homomorphism `f`, the induced homomorphism
on the quotient by `f`'s kernel has the same image as `f`.  -/
RingCon.rangeS_kerLift : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {f : M →+* P},
  (RingCon.kerLift f).rangeS = f.rangeS
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- The pro-étale precoverage on the small pro-étale site.  -/
AlgebraicGeometry.Scheme.ProEt.precoverage : (S : AlgebraicGeometry.Scheme) → CategoryTheory.Precoverage S.ProEt
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_exists_take_data : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ ∃ i, p.byteIdx = (String.ofList (List.take i s.toList)).utf8ByteSize
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Pons asinorum, oriented vector angle form.  -/
Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, ‖x‖ = ‖y‖ → o.oangle x (x - y) = o.oangle (y - x) y
-- Mathlib.Algebra.Group.Semiconj.Units
/-- `a` semiconjugates `x` to `a + x + -a`.  -/
AddUnits.mk_addSemiconjBy : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M), AddSemiconjBy (↑u) x (↑u + x + ↑(-u))
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const.opObjUnop_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : Cᵒᵖ) (j : Jᵒᵖ),
  (CategoryTheory.Functor.const.opObjUnop X).hom.app j =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X)).obj j)
-- Mathlib.Algebra.Ring.Parity
odd_one : ∀ {α : Type u_2} [inst : Semiring α], Odd 1
-- Batteries.Data.PairingHeap
/-- A predicate says there is no more than one tree.  -/
Batteries.PairingHeapImp.Heap.NoSibling : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → Prop