mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.adaptExcept.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) →
        ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'},
  Std.Internal.List.replaceEntry k v (⟨k', v'⟩ :: l) =
    bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: Std.Internal.List.replaceEntry k v l
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_div : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  sSup (s / t) = sSup s / sInf t
-- Mathlib.Analysis.Normed.Ring.Basic
Units.norm_pos : ∀ {α : Type u_2} [inst : NormedRing α] [Nontrivial α] (x : αˣ), 0 < ‖↑x‖
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.tateNorm_comp_d : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  CategoryTheory.CategoryStruct.comp M.tateNorm ((groupCohomology.inhomogeneousCochains M).d 0 1) = 0
-- Lean.Parser.Command
Lean.Parser.Command.optNamedPrio.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.BitVec.Lemmas
BitVec.toInt_setWidth'_of_lt : ∀ {m n : ℕ} (p : m < n) {x : BitVec m}, (BitVec.setWidth' ⋯ x).toInt = ↑x.toNat
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Checks if `type` is an application of (or forall with return type which is an application of) a
`Decidable*` constant. Specifically, checks if the constant is one of:
- `Decidable`
- `DecidablePred`
- `DecidableRel`
- `DecidableEq`
- `DecidableLE`
- `DecidableLT`

Ignores metadata and cleans up annotations.
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.isDecidableVariant : Lean.Expr → Bool
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
ContinuousMap.addRight.congr_simp : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : SeparatelyContinuousAdd X] (x x_1 : X),
  x = x_1 → ContinuousMap.addRight x = ContinuousMap.addRight x_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_apply_le_norm_cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) ⦃x : 𝕜⦄,
  x ∈ spectrum 𝕜 a →
    autoParam (ContinuousOn f (spectrum 𝕜 a)) norm_apply_le_norm_cfc._auto_1 →
      autoParam (p a) norm_apply_le_norm_cfc._auto_3 → ‖f x‖ ≤ ‖cfc f a‖
-- Mathlib.RepresentationTheory.Intertwining
/-- The `Equiv` between representations induced from `TensorProduct.lid`.  -/
Representation.TensorProduct.lid : (A : Type u_1) →
  {G : Type u_2} →
    {W : Type u_4} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → (σ : Representation A G W) → ((Representation.trivial A G A).tprod σ).Equiv σ
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.hasSubobjectClassifier_iff_isRepresentable`.

---

A category has a subobject classifier if and only if the subobjects functor is representable.  -/
CategoryTheory.isRepresentable_hasClassifier_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.HasSubobjectClassifier C ↔ (Subobject.presheaf C).IsRepresentable
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {V W : CoalgCat R} → (↑V.toModuleCat →ₗc[R] ↑W.toModuleCat) → V.Hom W
-- Mathlib.Analysis.MellinInversion
mellinInv.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (σ : ℝ) (f : ℂ → E) (x : ℝ),
  mellinInv σ f x = (1 / (2 * Real.pi)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * Complex.I)) • f (↑σ + ↑y * Complex.I)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α), G.ediam = ⨆ u, G.eccent u
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.isIso_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Mono
          (R₁.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
        CategoryTheory.Mono
            (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
              CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
          CategoryTheory.IsIso
              (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
            CategoryTheory.Mono
                (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
              CategoryTheory.IsIso
                (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2)
-- Mathlib.Algebra.CharP.Defs
ringChar.eq_iff : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ}, ringChar R = p ↔ CharP R p
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ SingleObj G ⥤ V` preserves the colimit of some `K : J ⥤ C` if it does
evaluated at `SingleObj.star G`.  -/
_private.Mathlib.CategoryTheory.Action.Limits.0.Action.SingleObj.preservesColimit : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J] (K : CategoryTheory.Functor J C),
  CategoryTheory.Limits.PreservesColimit K
      (F.comp ((CategoryTheory.evaluation (CategoryTheory.SingleObj G) V).obj (CategoryTheory.SingleObj.star G))) →
    CategoryTheory.Limits.PreservesColimit K F
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.searchTacticSuggestions : LeanSearchClient.SearchServer → Lean.Syntax → Lean.TSyntax `str → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Order.InitialSeg
InitialSeg.isMin_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} [inst_1 : PartialOrder α] (f : α ≤i β),
  IsMin (f a) ↔ IsMin a
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The ring tactic result carried by a certificate.  -/
Mathlib.Tactic.Determinant.CertResult : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Q(«$α») → Type
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {A B : CommAlgCat R} {hom' hom'_1 : ↑A →ₐ[R] ↑B},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Order.WellFoundedSet
/-- `s.PartiallyWellOrderedOn r` indicates that the relation `r` is `WellQuasiOrdered` when
restricted to `s`.

A set is partially well-ordered by a relation `r` when any infinite sequence contains two elements
where the first is related to the second by `r`. Equivalently, any antichain (see `IsAntichain`) is
finite, see `Set.partiallyWellOrderedOn_iff_finite_antichains`.

TODO: rename this to `WellQuasiOrderedOn` to match `WellQuasiOrdered`.  -/
Set.PartiallyWellOrderedOn : {α : Type u_2} → Set α → (α → α → Prop) → Prop
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x - y, y)` preserves the measure `μ × ν`.  -/
MeasureTheory.measurePreserving_sub_prod : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 - z.2, z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Order.Sublattice
Sublattice.comap_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L M : Sublattice β) (f : LatticeHom α β),
  Sublattice.comap f (L ⊓ M) = Sublattice.comap f L ⊓ Sublattice.comap f M
-- Mathlib.RepresentationTheory.Basic
Representation.coeff_of_leftRegular_of_generator : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) →
    ∀ (x : MonoidAlgebra k G), ((Representation.leftRegular k G) g) x = x → ∀ (γ : G), x.coeff γ = x.coeff g
-- Lean.Elab.InfoTree.Main
Lean.Elab.PartialTermInfo.format : Lean.Elab.ContextInfo → Lean.Elab.PartialTermInfo → Std.Format
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.extrinsicFix₃.eq_1 : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
  (F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c)
  (a : α) (b : β a) (c : γ a b),
  WellFounded.extrinsicFix₃ R F a b c =
    WellFounded.extrinsicFix R (fun x G => F x.fst x.snd.fst x.snd.snd fun a b c => G ⟨a, ⟨b, c⟩⟩) ⟨a, ⟨b, c⟩⟩
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformGroup_sInf : ∀ {G : Type u_1} [inst : Group G] {us : Set (UniformSpace G)}, (∀ u ∈ us, IsUniformGroup G) → IsUniformGroup G
-- Mathlib.Algebra.Group.Basic
nsmul_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α) (n : ℕ), n • (a - b) = n • a - n • b
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Symm.comap`. -/
Symmetric.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Symm r] (f : α → β), Std.Symm (Function.onFun r f)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.smul_continuousOn_of_subset : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {A K : Set X} {𝕜 : Type u_9} [inst_4 : NormedRing 𝕜]
  [inst_5 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SecondCountableTopologyEither X E] {f : X → 𝕜},
  MeasureTheory.IntegrableOn f A μ →
    ∀ {g : X → E},
      ContinuousOn g K → MeasurableSet A → IsCompact K → A ⊆ K → MeasureTheory.IntegrableOn (fun x => f x • g x) A μ
-- Mathlib.Data.List.TakeDrop
List.takeD_left' : ∀ {α : Type u} {l₁ l₂ : List α} {n : ℕ} {a : α}, l₁.length = n → List.takeD n (l₁ ++ l₂) a = l₁
-- Batteries.Data.Vector.Lemmas
Vector.scanrM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → β → m β) (init : β)
  (as : Vector α n), Vector.scanrM f init as = Vector.scanrM.loop f as init n ⋯ (Vector.cast ⋯ #v[])
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
SSet.Subcomplex.mem_op_obj_iff : ∀ {X : SSet} (A : X.Subcomplex) {d : SimplexCategoryᵒᵖ} (x : X.op.obj d), x ∈ A.op.obj d ↔ SSet.opObjEquiv x ∈ A.obj d
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafFunctor_obj : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] (A : C),
  (skyscraperPresheafFunctor p₀).obj A = skyscraperPresheaf p₀ A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeOp.eq_1 : ∀ {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}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Functor.mapCoconeOp G t =
    CategoryTheory.Limits.Cone.extInv (CategoryTheory.Iso.refl (G.mapCocone t).op.pt) ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.notMem_span : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {i : ι} [Nontrivial R], LinearIndepOn R v s → i ∈ s → v i ∉ Submodule.span R (v '' (s \ {i}))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {k : α}, t.contains k = true ↔ k ∈ t
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.symm_mk_zero : ∀ {M : Type u_1} [inst : Zero M], DomAddAct.mk.symm 0 = 0
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- A compactly supported continuous function gives rise to a bounded continuous function.  -/
CompactlySupportedContinuousMap.toBoundedContinuousFunction : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    {β : Type u_6} →
      [inst_1 : PseudoMetricSpace β] →
        [inst_2 : Zero β] → CompactlySupportedContinuousMap α β → BoundedContinuousFunction α β
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.of_precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} {ι' : Type u_6}
  {g : ι' → ι}, Function.Surjective g → ProbabilityTheory.iIndepSet (s ∘ g) μ → ProbabilityTheory.iIndepSet s μ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} [inst_2 : SizeOf C] (toPrepathObject : HomotopicalAlgebra.PrepathObject A)
  (weakEquivalence_ι :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam),
  sizeOf { toPrepathObject := toPrepathObject, weakEquivalence_ι := weakEquivalence_ι } =
    1 + sizeOf toPrepathObject + sizeOf weakEquivalence_ι
-- Mathlib.Data.Set.Lattice
Set.sInter_union : ∀ {α : Type u_1} (S T : Set (Set α)), ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.support_toPOUFun_subset : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι),
  Function.support (f.toPOUFun i) ⊆ Function.support ⇑(f i)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.toAddSubmonoidClass : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonAssocSemiring R} {inst_1 : SetLike S R}
  [self : SubsemiringClass S R], AddSubmonoidClass S R
-- Mathlib.Order.Filter.Pointwise
Filter.isCentralVAdd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [inst_1 : VAdd αᵃᵒᵖ β] [IsCentralVAdd α β], IsCentralVAdd α (Filter β)
-- Mathlib.Order.Monotone.Defs
StrictMonoOn.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, StrictMonoOn g t → StrictMonoOn f s → Set.MapsTo f s t → StrictMonoOn (g ∘ f) s
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_rat_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ q, x ≤ ↑q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_zero : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : Algebra R S] [inst_7 : Algebra R F] [inst_8 : Algebra S F] [inst_9 : IsScalarTower R S F]
  [inst_10 : Algebra R K] [inst_11 : Algebra S K] [inst_12 : IsScalarTower R S K] (f : F →ₐ[S] K),
  (WeierstrassCurve.Affine.Point.map f) 0 = 0
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hom_ext_iff : ∀ {R S : BoolRing} {f g : R ⟶ S}, f = g ↔ BoolRing.Hom.hom f = BoolRing.Hom.hom g
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum : ∀ {X : Type u} [inst : TopologicalSpace X] [CompletelyRegularSpace X],
  Cardinal.mk X < Cardinal.continuum → TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Mathlib.Lean.Meta.Simp
Lean.Meta.Simp.instToFormatSimpTheorems_mathlib : Std.ToFormat Lean.Meta.SimpTheorems
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.isPrefixOf.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (x = [] → False) →
    (match x, [] with
      | [], x => h_1 x
      | x, [] => h_2 x
      | a :: as, b :: bs => h_3 a as b bs) =
      h_2 x
-- Std.Do.Triple.SpecLemmas
List.Cursor.pos_mk : ∀ {α : Type u_1} {l pre suff : List α} (h : pre ++ suff = l),
  { «prefix» := pre, suffix := suff, property := h }.pos = pre.length
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `f : X → Z` is a surjective Borel measurable map from a standard Borel space
to a countably separated measurable space,
then for any measurable space `α` and `g : Z → α`, the composition
`g ∘ f` is measurable if and only if `g` is measurable.  -/
Measurable.measurable_comp_iff_of_surjective : ∀ {X : Type u_3} {Z : Type u_5} {β : Type u_6} [inst : MeasurableSpace X] [StandardBorelSpace X]
  [inst_2 : MeasurableSpace β] [inst_3 : MeasurableSpace Z] [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → ∀ {g : Z → β}, Measurable (g ∘ f) ↔ Measurable g
-- Mathlib.Util.CompileInductive
_private.Mathlib.Util.CompileInductive.0.Mathlib.Util.addAndCompile' : Lean.Declaration → Lean.CoreM Unit
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermEtaStructMode.evalTerm : Lean.Term → Lean.Elab.TermElabM (Lean.Meta.EtaStructMode × Lean.Expr)
-- Mathlib.Data.Finset.Prod
Finset.product_image_snd : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq β],
  s.Nonempty → Finset.image Prod.snd (s ×ˢ t) = t
-- Mathlib.Data.List.Intervals
List.Ico.eq_empty_iff : ∀ {n m : ℕ}, List.Ico n m = [] ↔ m ≤ n
-- Mathlib.Order.CompleteLattice.Basic
biSup_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {p q : ι → Prop},
  (∀ (i : ι), p i → q i) → ⨆ i, ⨆ (_ : p i), f i ≤ ⨆ i, ⨆ (_ : q i), f i
-- Mathlib.RingTheory.WittVector.Frobenius
/-- The rational polynomials that give the coefficients of `frobenius x`,
in terms of the coefficients of `x`.
These polynomials actually have integral coefficients,
see `frobeniusPoly` and `map_frobeniusPoly`.  -/
WittVector.frobeniusPolyRat : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial ℕ ℚ
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.coe_iSup_of_directed : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → AddSubmonoid M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roc : ∀ {m n i : ℕ}, (m<...=n).toList[i]! = if i < n - m then m + 1 + i else 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.lift_obj_toComma : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {C : Type u_4} [inst_5 : CategoryTheory.Category.{v_4, u_4} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom)
  (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) (X : C),
  ((CategoryTheory.MorphismProperty.Comma.lift F hP hQ hW).obj X).toComma = F.obj X
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.Monadic.step.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (next : α) → motive (some next)),
  (match none with
    | none => h_1 ()
    | some next => h_2 next) =
    h_1 ()
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.differentiable_completedHurwitzZetaOdd : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.completedHurwitzZetaOdd a)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.H1Cotangent.map.eq_1 : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Type u_2)
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (T : Type w) [inst_5 : CommRing T] [inst_6 : Algebra R T]
  [inst_7 : Algebra S T] [inst_8 : IsScalarTower R S T] [inst_9 : Algebra S' T] [inst_10 : IsScalarTower R S' T],
  Algebra.H1Cotangent.map R S S' T =
    Algebra.Extension.H1Cotangent.map
      ((Algebra.Generators.self R S').defaultHom (Algebra.Generators.self S T)).toExtensionHom
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
be promoted to an oplax functor from `LocallyDiscrete I` to `B`.
 -/
CategoryTheory.Functor.toOplaxFunctor' : {I : Type u_1} →
  {B : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} I] →
      [inst_1 : CategoryTheory.Bicategory B] →
        [inst_2 : CategoryTheory.Bicategory.Strict B] →
          CategoryTheory.Functor I B → CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete I) B
-- Mathlib.Order.DirectedInverseSystem
/-- A natural partial family of bijections to `piLT` satisfying a compatibility condition.  -/
InverseSystem.PEquivOn : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        (⦃i j : ι⦄ → i ≤ j → F j → F i) →
          [inst_1 : SuccOrder ι] →
            (⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i) → Set ι → Type (max (max u_6 u_7) u_8)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.getVert_cycle : ∀ {n m : ℕ}, m ≤ n + 3 → (SimpleGraph.cycleGraph.cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
/-- Every comonoid object in a Cartesian monoidal category is equivalent to
the canonical comonoid structure on the underlying object.
 -/
CategoryTheory.isoCartesianComon : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (A : CategoryTheory.Comon C) → A ≅ (CategoryTheory.cartesianComon C).obj A.X
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_filterMapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β}
  {f : (a : α) → β a → Option (δ a)},
  (Std.DHashMap.Internal.toListModel (↑(m.filterMapₘ f)).buckets).Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd))
      (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap : ∀ {R : Type u} [inst : CommRing R] {M N P : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] [inst_7 : Coalgebra R M]
  [inst_8 : Coalgebra R N] [inst_9 : Coalgebra R P],
  (CategoryTheory.MonoidalCategoryStruct.associator (CoalgCat.of R M) (CoalgCat.of R N)
            (CoalgCat.of R P)).hom.toCoalgHom'.toLinearMap =
    ↑(TensorProduct.assoc R M N P)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq_append : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → s.copy = t₁ ++ t₂