mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_map_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  {X Y : CategoryTheory.StructuredArrow f.right F} (φ : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).map φ).right.right =
    CategoryTheory.StructuredArrow.Hom.right φ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.left = Y
-- Mathlib.Analysis.Normed.Group.Basic
norm_toNNReal' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E}, ‖a‖.toNNReal = ‖a‖₊
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMapM.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m] [inst_2 : MonadAttach m]
  (f : β → m (Option γ)) (it : Std.Iter β), Std.Iter.filterMapM f it = Std.IterM.filterMapM f it.toIterM
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_eq_zero : ∀ {p : ℝ}, Real.binEntropy p = 0 ↔ p = 0 ∨ p = 1
-- Mathlib.Analysis.Complex.Harmonic.Poisson
/-- **Poisson integral formula** for harmonic functions on arbitrary disks in the complex plane,
formulated with the real part of the Herglotz–Riesz kernel of integration.
 -/
InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul : ∀ {f : ℂ → ℝ} {c w : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicContOnCl f (Metric.ball c R) →
    w ∈ Metric.ball c R → Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w • f) c R = f w
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.w : Std.Tactic.BVDecide.BVPred.ExprPair → ℕ
-- Mathlib.Algebra.GroupWithZero.Divisibility
dvd_zero : ∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), a ∣ 0
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The sum of two linear maps is linear.  -/
LinearMap.instAdd : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → Add (M →ₛₗ[σ₁₂] M₂)
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_sub_string : ∀ {p : String.Pos.Raw} {s : String}, (p - s).byteIdx = p.byteIdx - s.utf8ByteSize
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ReflexiveCofork.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} {X : C}
  (π : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ X)
  (h :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) π =
      CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) π),
  (CategoryTheory.Limits.ReflexiveCofork.mk π h).pt = X
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommMonoid : {α : Type u_2} → [inst : Small.{v, u_2} α] → [CommMonoid α] → CommMonoid (Shrink.{v, u_2} α)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable.  -/
ConditionallyCompleteLinearOrder.toDecidableLT : {α : Type u_5} → [self : ConditionallyCompleteLinearOrder α] → DecidableLT α
-- Mathlib.Topology.Algebra.ConstMulAction
smul_mem_nhds_self : ∀ {G : Type u_4} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G},
  g • s ∈ nhds g ↔ s ∈ nhds 1
-- Lean.Meta.Match.MatcherInfo
/-- Information about the parameter structure for the alternative of a matcher or splitter.
 -/
Lean.Meta.Match.AltParamInfo : Type
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) [inst : Fintype ↑(G'.neighborSet v)],
  G'.degree v = Fintype.card ↑(G'.neighborSet v)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_zero : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M},
  (s.indicator f = fun x => 0) ↔ Disjoint (Function.support f) s
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.json.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.json✝ = 1
-- Mathlib.Data.ENat.Basic
ENat.lift_eq_toNat_of_lt_top : ∀ {x : ℕ∞} (hx : x < ⊤), x.lift hx = x.toNat
-- Init.Data.Int.Basic
/-- Decides whether two integers are equal. Usually accessed via the `DecidableEq Int` instance.

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `show (7 : Int) = (3 : Int) + (4 : Int) by decide`
* `if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"`
* `(¬ (6 : Int) = (3 : Int)) = true`
 -/
Int.decEq : (a b : ℤ) → Decidable (a = b)
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'}
  {h' h₂' y : 𝕜'},
  HasDerivWithinAt h₂ h₂' s' y →
    HasDerivWithinAt h h' s x → Set.MapsTo h s s' → y = h x → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
-- Mathlib.Order.CompleteLattice.Basic
Monotone.sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] {s : Set (α → β)},
  (∀ f ∈ s, Monotone f) → Monotone (sSup s)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderBaseChangeAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong g] [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.HasPullbacksAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderBaseChange]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg :
    autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Over.pullbackComp._auto_1)
  (X_1 : P.Over Q Z),
  ((CategoryTheory.MorphismProperty.Over.pullbackComp f g fg hfg).hom.app X_1).left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.map X_1.hom fg X_1.hom (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.id X_1.left) (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
      (CategoryTheory.Limits.pullbackLeftPullbackSndIso X_1.hom g f).inv
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f g : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) →
        ∀ {t : Set α}, MeasurableSet t → μ t ≠ ⊤ → f =ᵐ[μ.restrict t] g
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α] (w : ℕ)
  (vec : aig.BinaryRefVec w) (cin : aig.Ref),
  sizeOf { w := w, vec := vec, cin := cin } = 1 + sizeOf w + sizeOf vec + sizeOf cin
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelp.fromJson : Lean.Json → Except String Lean.Lsp.SignatureHelp
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.prependNode.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.Node α β → Sort u_3) →
      (node : Lean.PersistentHashMap.Node α β) →
        ((es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
            motive (Lean.PersistentHashMap.Node.entries es)) →
          ((keys : Array α) →
              (vals : Array β) →
                (hsz : keys.size = vals.size) → motive (Lean.PersistentHashMap.Node.collision keys vals hsz)) →
            motive node
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_injective : ∀ (o : Ordinal.{u_1}), Function.Injective (Ordinal.veblen o)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is equal to the normalizer of the image of a bijective
function.  -/
AddSubgroup.map_normalizer_eq_of_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : G →+ N},
  Function.Bijective ⇑f → AddSubgroup.map f (AddSubgroup.normalizer ↑H) = AddSubgroup.normalizer ↑(AddSubgroup.map f H)
-- Init.Data.Float.Float32
instNegFloat32 : Neg Float32
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_card_nsmul : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] [AddLeftMono N] (s : Finset ι)
  (f : ι → N) (n : N), (∀ x ∈ s, f x ≤ n) → s.sum f ≤ s.card • n
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add_f_nome : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S), (E.add f).f none = f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₃_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
      _auto_311✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
      _auto_313✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝))
      _auto_315✝),
  (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunctionTrivChar.eq_1 : ∀ (N : ℕ) [inst : NeZero N], DirichletCharacter.LFunctionTrivChar N = DirichletCharacter.LFunction 1
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.conjNeg_symm : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H},
  AddConstMap.conjNeg.symm = AddConstMap.conjNeg
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] {φ : MvPolynomial σ R},
  φ.IsSymmetric → ∀ (f : R →+* S), ((MvPolynomial.map f) φ).IsSymmetric
-- Mathlib.Order.Monotone.Monovary
Monovary.dual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary f g → Antivary f (⇑OrderDual.toDual ∘ g)
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.sub_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f g : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  (hg : CategoryTheory.CategoryStruct.comp g (R.cocomplex.d n m) = 0),
  R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mul_NonnegCoeffs : ∀ {p₁ p₂ : Lean.Grind.CommRing.Poly}, p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul p₂).NonnegCoeffs
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : C) (y : D),
  ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj x).obj y =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y x
-- Init.Data.String.Decode
List.utf8DecodeChar?_utf8Encode_singleton_append : ∀ {b : ByteArray} {c : Char}, ([c].utf8Encode ++ b).utf8DecodeChar? 0 = some c
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsClosedBelow.sInter : ∀ {o : Ordinal.{u_1}} {S : Set (Set Ordinal.{u_1})},
  (∀ C ∈ S, Ordinal.IsClosedBelow C o) → Ordinal.IsClosedBelow (⋂₀ S) o
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprElimAltInfo : Repr Lean.Meta.ElimAltInfo
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.map_comap_le : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (T : CategoryTheory.Subgroupoid D),
  CategoryTheory.Subgroupoid.map φ hφ (CategoryTheory.Subgroupoid.comap φ T) ≤ T
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_copy : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonUInt64 : Lean.FromJson UInt64
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).toList = []
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_inv_base : ∀ (b x : ℝ), Real.logb b⁻¹ x = -Real.logb b x
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.pushImport : Lean.Import → Lean.ParseImports.State → Lean.ParseImports.State
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_refl : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} (f : α → β), f =ᵐ[μ] f
-- Std.Data.HashMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `getElem_insertIfNew`.  -/
Std.HashMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr →
  ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof
-- Batteries.Data.String.Lemmas
String.endPos_eq_zero : ∀ (s : String), s.rawEndPos = 0 ↔ s = ""
-- Init.Data.Array.Lemmas
Array.map_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1},
  Array.map f (Array.replicate n a) = Array.replicate n (f a)
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_add_one : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {f : ι → R} (s : Finset ι),
  ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLastI.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (h_1 : Unit → motive []) (h_2 : (a : α) → motive [a])
  (h_3 : (head b : α) → motive [head, b]) (h_4 : (head head_1 : α) → (l : List α) → motive (head :: head_1 :: l)),
  (match [a] with
    | [] => h_1 ()
    | [a] => h_2 a
    | [head, b] => h_3 head b
    | head :: head_1 :: l => h_4 head head_1 l) =
    h_2 a
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.sSup_apply_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedGT ι] {s : Set (Colex ((i : ι) → α i))} {i : ι} {e : Colex ((i : ι) → α i)},
  (∀ f ∈ s, (∀ j > i, f j = sSup s j) → f i ≤ e i) → sSup s i ≤ e i
-- Lean.Environment
Lean.PersistentEnvExtensionDescr.mk : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → (σ → Array α) → Lean.PersistentEnvExtensionDescr α β σ
-- Mathlib.Algebra.Group.End
MulAutMultiplicative_symm_apply_symm_apply : ∀ (G : Type u_3) [inst : AddGroup G] (a : G ≃+ G) (a_1 : Multiplicative G),
  (MulEquiv.symm ((MulAutMultiplicative G).symm a)) a_1 = Multiplicative.ofAdd (a.symm (Multiplicative.toAdd a_1))
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `comapDomain` as an `AddMonoidHom`.  -/
AddMonoidAlgebra.comapDomainAddMonoidHom : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → (f : M → N) → Function.Injective f → AddMonoidAlgebra R N →+ AddMonoidAlgebra R M
-- Mathlib.AlgebraicGeometry.Limits
/-- `S` is the disjoint union of `Xᵢ` if the `Xᵢ` are covering, pairwise disjoint open subschemes
of `S`.  -/
AlgebraicGeometry.nonempty_isColimit_cofanMk_of : ∀ {σ : Type v} [Small.{u, v} σ] {X : σ → AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (f : (i : σ) → X i ⟶ S) [inst : ∀ (i : σ), AlgebraicGeometry.IsOpenImmersion (f i)],
  ⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (f i) = ⊤ →
    Pairwise (Function.onFun Disjoint fun x => AlgebraicGeometry.Scheme.Hom.opensRange (f x)) →
      Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk S f))
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- The infinite version of `Finset.prod_one_add_ordered`.  -/
tprod_one_add_ordered : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] [inst_1 : TopologicalSpace α] {f : ι → α}
  [inst_2 : LinearOrder ι] [inst_3 : LocallyFiniteOrderBot ι] [T2Space α] [ContinuousAdd α],
  (Summable fun i => f i * ∏ j < i, (1 + f j)) →
    (Multipliable fun x => 1 + f x) → ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomTensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z W : C} [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y] [inst_5 : CategoryTheory.AddMonObj Z] [inst_6 : CategoryTheory.AddMonObj W]
  {f : X ⟶ Y} {g : Z ⟶ W} [CategoryTheory.IsAddMonHom f] [CategoryTheory.IsAddMonHom g],
  CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv_right`. -/
AntivaryOn.of_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g⁻¹ s → MonovaryOn f g s
-- Std.Do.PostCond
/-- Implication of postconditions.

This is defined pointwise, as the implication of the assertions about the return value and the
implications of each of the assertions about each potential exception.

While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
postconditions is itself a postcondition.
 -/
Std.Do.«term_→ₚ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.cofan_mk_inj : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P),
  (CategoryTheory.Limits.Cofan.mk P p).inj = p
-- Init.Data.SInt.Lemmas
Int8.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < 2 ^ 7 → b < 2 ^ 7 → (Int8.ofNat a < Int8.ofNat b ↔ a < b)
-- Mathlib.RingTheory.Length
LinearEquiv.length_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.length R M = Module.length R N
-- Init.Data.UInt.Lemmas
instCommutativeUSizeHMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact
instPreservesFiniteColimitsModuleCatRestrictScalars : ∀ {R : Type u} [inst : CommRing R] {R' : Type u'} [inst_1 : CommRing R'] (f : R →+* R'),
  CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
-- Lean.Util.PPExt
Lean.ppFnsRef : IO.Ref Lean.PPFns
-- Mathlib.Algebra.Ring.Rat
Rat.isDomain : IsDomain ℚ
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.smul_def : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits] (ϕ : p.Gal) (x : ↑(p.rootSet E)),
  ϕ • x = (Polynomial.Gal.rootsEquivRoots p E) (ϕ • (Polynomial.Gal.rootsEquivRoots p E).symm x)
-- Init.Data.BitVec.Bitblast
BitVec.extractAndExtendAux.eq_def : ∀ {w : ℕ} (k len : ℕ) (x : BitVec w) (acc : BitVec (k * len)) (hle : k ≤ w),
  BitVec.extractAndExtendAux k len x acc hle =
    match hwi : w - k with
    | 0 => BitVec.cast ⋯ acc
    | n'.succ =>
      have acc' := BitVec.extractAndExtendBit k len x ++ acc;
      BitVec.extractAndExtendAux (k + 1) len x (BitVec.cast ⋯ acc') ⋯
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.pow_subset : ∀ {M : Type u_3} [inst : Monoid M] {s : Set M} {S : Submonoid M} {n : ℕ}, s ⊆ ↑S → s ^ n ⊆ ↑S
-- Mathlib.Data.Multiset.Filter
Multiset.filter_zero : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Multiset.filter p 0 = 0
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β} {it₂ it₂' : Std.Iter γ},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    (Std.Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.skip (Std.Iter.flatMapAfter f it₁ (some it₂')))
-- Lean.Server.InfoUtils
Lean.Elab.Info.range? : Lean.Elab.Info → Option Lean.Syntax.Range
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.comapRight_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) (a : α),
  (κ.comapRight hf) a = MeasureTheory.Measure.comap f (κ a)
-- Mathlib.Algebra.Notation.Defs
ite_add_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a b c d : α),
  ((if P then a else b) + if P then c else d) = if P then a + c else b + d
-- Mathlib.Algebra.Order.Field.Basic
IsGLB.mul_left : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α]
  {s : Set α}, 0 ≤ a → IsGLB s b → IsGLB ((fun b => a * b) '' s) (a * b)