mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- An affine isomorphism between the domains of affine spaces induces an affine isomorphism over
another ring between the two function spaces.  -/
AffineEquiv.congrLeft : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        (R : Type u_10) →
                          {W : Type u_11} →
                            [inst_7 : Ring R] →
                              [inst_8 : AddCommGroup W] →
                                [inst_9 : Module k W] →
                                  [inst_10 : Module R W] →
                                    [inst_11 : SMulCommClass k R W] →
                                      (P₁ ≃ᵃ[k] P₂) →
                                        (Q : Type u_12) → [inst_12 : AddTorsor W Q] → (P₁ →ᵃ[k] Q) ≃ᵃ[R] P₂ →ᵃ[k] Q
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.symm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.run_bind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β},
  (x.bind f).run = do
    let x ← x.run
    (f x).run
-- Init.Data.Int.Lemmas
Int.mul_ne_zero_iff : ∀ {a b : ℤ}, a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
-- Mathlib.Topology.Separation.CompletelyRegular
instT35SpaceForall : ∀ {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)] [ht : ∀ (i : ι), T35Space (X i)],
  T35Space ((i : ι) → X i)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.list_prod_ofFn_of_eq_dProd : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (n : ℕ) (fι : Fin n → ι) (fA : (a : Fin n) → A (fι a)),
  (List.ofFn fun a => (DirectSum.of A (fι a)) (fA a)).prod =
    (DirectSum.of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.supSet : (α : Type u_8) → [h : InfSet α] → SupSet αᵒᵈ
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Sheaf.forgetFaithful : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : TopCat), (TopCat.Sheaf.forget C X).Faithful
-- Mathlib.Analysis.Calculus.Deriv.Pow
/-- Eta-expanded form of `HasDerivAt.pow` -/
HasDerivAt.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasDerivAt f f' x → ∀ (n : ℕ), HasDerivAt (fun i => f i ^ n) (↑n * f x ^ (n - 1) * f') x
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.preimage_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h ⁻¹' ⇑h '' s = s
-- Mathlib.Logic.Equiv.Prod
Equiv.Perm.fst_prodExtendRight : ∀ {α₁ : Type u_9} {β₁ : Type u_10} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (ab : α₁ × β₁),
  ((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.negAddY P Q = -(Q 1 ^ 2 * P 2) * W'.negY P
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) [Algebra.IsAlgebraic R A],
  Function.Injective ⇑f →
    Function.Surjective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Algebra.IsAlgebraic S B
-- Init.Data.Int.DivMod.Lemmas
Int.eq_fdiv_of_mul_eq_right : ∀ {a b c : ℤ}, a ≠ 0 → a * b = c → b = c.fdiv a
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_map : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] (f : S →+ T) (g : R →+ S) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.map f (AddMonoidAlgebra.map g x) = AddMonoidAlgebra.map (f.comp g) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Whiskering right of a `CatCospanTransformMorphism` by a `CatCospanTransform`.  -/
CategoryTheory.Limits.CatCospanTransform.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Polynomial.OfFn
/-- `ofFn n v` has `degree` smaller than `n`.  -/
Polynomial.ofFn_degree_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ} (v : Fin n → R),
  ((Polynomial.ofFn n) v).degree < ↑n
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_one : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E], ⇑1 = id
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_self : ∀ {a : ℤ}, a ≠ 0 → a.fdiv a = 1
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData_i : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).LeftHomologyData),
  (HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h).i =
    CategoryTheory.CategoryStruct.comp h.i (K.extendXIso e hj').inv
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The localization functor from the category `C` to the groupoid `FreeGroupoid C`  -/
CategoryTheory.FreeGroupoid.of : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.FreeGroupoid C)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.TheoremForm.comp.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.TheoremForm.comp = 1
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_nat : ∀ (n : ℕ), Cardinal.preBeth ↑n = ↑((fun x => 2 ^ x)^[n] 0)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.mk.inj : ∀ {A : Type u} {B : Type u_2} {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B} {vars rels : Type}
  {P : Algebra.Presentation A B vars rels} {σ : B →ₐ[A] MvPolynomial vars A ⧸ P.ker ^ 2}
  {h : vars → MvPolynomial vars A} {p : rels → MvPolynomial rels (MvPolynomial vars A)}
  {hphom : ∀ (j : rels), (p j).IsHomogeneous 2}
  {hp : ∀ (j : rels), (MvPolynomial.eval P.relation) (p j) = (MvPolynomial.aeval h) (P.relation j)}
  {q : vars → MvPolynomial rels P.Ring} {hqhom : ∀ (i : vars), (q i).IsHomogeneous 1}
  {hq : ∀ (i : vars), (MvPolynomial.eval P.relation) (q i) = h i - MvPolynomial.X i} {vars_1 rels_1 : Type}
  {P_1 : Algebra.Presentation A B vars_1 rels_1} {σ_1 : B →ₐ[A] MvPolynomial vars_1 A ⧸ P_1.ker ^ 2}
  {h_1 : vars_1 → MvPolynomial vars_1 A} {p_1 : rels_1 → MvPolynomial rels_1 (MvPolynomial vars_1 A)}
  {hphom_1 : ∀ (j : rels_1), (p_1 j).IsHomogeneous 2}
  {hp_1 : ∀ (j : rels_1), (MvPolynomial.eval P_1.relation) (p_1 j) = (MvPolynomial.aeval h_1) (P_1.relation j)}
  {q_1 : vars_1 → MvPolynomial rels_1 P_1.Ring} {hqhom_1 : ∀ (i : vars_1), (q_1 i).IsHomogeneous 1}
  {hq_1 : ∀ (i : vars_1), (MvPolynomial.eval P_1.relation) (q_1 i) = h_1 i - MvPolynomial.X i},
  { vars := vars, rels := rels, P := P, σ := σ, h := h, p := p, hphom := hphom, hp := hp, q := q, hqhom := hqhom,
        hq := hq } =
      { vars := vars_1, rels := rels_1, P := P_1, σ := σ_1, h := h_1, p := p_1, hphom := hphom_1, hp := hp_1, q := q_1,
        hqhom := hqhom_1, hq := hq_1 } →
    vars = vars_1 ∧ rels = rels_1 ∧ P ≍ P_1 ∧ σ ≍ σ_1 ∧ h ≍ h_1 ∧ p ≍ p_1 ∧ q ≍ q_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A finite measure `μ` on `α ⧸ G` satisfying `QuotientMeasureEqMeasurePreimage` has finite
covolume.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ]
  [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.covolume G α ν < ⊤
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_zsmul_sub_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a b • p - b = -toIocMod hp a b
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.addOmissionInfo : Lean.SubExpr.Pos →
  Lean.Syntax → Lean.Expr → Lean.PrettyPrinter.Delaborator.OmissionReason → Lean.PrettyPrinter.Delaborator.DelabM Unit
-- Lean.Meta.Eqns
_private.Lean.Meta.Eqns.0.Lean.Meta.getUnfoldEqnFnsRef : IO.Ref (List Lean.Meta.GetUnfoldEqnFn)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDTreeMap.Const.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toIsometryEquiv_symm : ∀ {𝕜 : 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.symm.toIsometryEquiv = e.toIsometryEquiv.symm
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instCoeToTypeElemIio : (o : Ordinal.{u_1}) → Coe o.ToType ↑(Set.Iio o)
-- Std.Http.Internal.LowerCase
_private.Std.Http.Internal.LowerCase.0.Std.Http.Internal.Char.toLower_eq_self_iff : ∀ {c : Char}, c.toLower = c ↔ c.isUpper = false
-- Mathlib.Algebra.GroupWithZero.Indicator
/-- If `g` is everywhere nonzero, then `support (f * g) = support f`.  -/
Function.support_mul_of_ne_zero_right : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) {g : ι → M₀},
  (∀ (x : ι), g x ≠ 0) → (Function.support fun x => f x * g x) = Function.support f
-- Aesop.Search.Expansion.Norm
_private.Aesop.Search.Expansion.Norm.0.Aesop.normSimpCore.addLocalRules : Lean.MVarId →
  Array Aesop.LocalNormSimpRule →
    Lean.Meta.Simp.Context →
      Lean.Meta.Simp.SimprocsArray → Bool → Aesop.NormM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)
-- Mathlib.Topology.Constructions
/-- `Pi.mulSingle i x` is continuous in `x`.  -/
continuous_mulSingle : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : (i : ι) → One (A i)]
  [inst_1 : DecidableEq ι] (i : ι), Continuous fun x => Pi.mulSingle i x
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single_embedding : ∀ {n : ℕ} (h : 0 < n) (i : Fin n), ((Composition.single n h).embedding 0) i = i
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreUnitCounit.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (unit : CategoryTheory.Functor.id C ⟶ F.comp G) (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit F)
          (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit)) =
        CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
      CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam)
  (right_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit)
          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight counit G)) =
        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam),
  sizeOf { unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
    1 + sizeOf unit + sizeOf counit + sizeOf left_triangle + sizeOf right_triangle
-- Mathlib.Topology.Germ
/-- Map the germ of functions `X × Y → Z` at `p = (x,y) ∈ X × Y` to the corresponding germ
of functions `Y → Z` at `y ∈ Y`  -/
Filter.Germ.sliceRight : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → {p : X × Y} → (nhds p).Germ Z → (nhds p.2).Germ Z
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The inclusion map from `widePullback s` to `A`
 -/
CategoryTheory.Subobject.widePullbackι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [inst_3 : CategoryTheory.Limits.HasWidePullbacks C] →
          {A : C} → (s : Set (CategoryTheory.Subobject A)) → CategoryTheory.Subobject.widePullback s ⟶ A
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vle_rfl`. -/
ValuativeRel.vle.rfl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x : R}, x ≤ᵥ x
-- Mathlib.Data.Fin.Tuple.Reflection
/-- `Finset.univ.prod` with better defeq for `Fin`.  -/
FinVec.prod : {α : Type u_1} → [Mul α] → [One α] → {m : ℕ} → (Fin m → α) → α
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f g pf : C}
  {η : f ≅ g} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.MonoidalCategory.whiskerLeftIso p η.symm ≪≫ η_f = η_g
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap S (TensorProduct R S T)))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
      h
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.foldM.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (α × Batteries.BinomialHeap.Imp.Heap α) → Sort u_2) (hd : α)
  (tl : Batteries.BinomialHeap.Imp.Heap α) (h_1 : some (hd, tl) = none → motive none)
  (h_2 :
    (hd_1 : α) →
      (tl_1 : Batteries.BinomialHeap.Imp.Heap α) → some (hd, tl) = some (hd_1, tl_1) → motive (some (hd_1, tl_1))),
  (match eq : some (hd, tl) with
    | none => h_1 eq
    | some (hd_1, tl_1) => h_2 hd_1 tl_1 eq) =
    h_2 hd tl ⋯
-- Mathlib.Data.Sym.Basic
Sym.eq_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ} {s : Sym α n}, s = Sym.replicate n a ↔ ∀ b ∈ s, b = a
-- Init.Data.SInt.Lemmas
ISize.toInt64_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Init.Data.Bool
Bool.and_eq_right_iff_imp : ∀ {a b : Bool}, (a && b) = b ↔ b = true → a = true
-- Mathlib.Analysis.Convex.EGauge
le_egauge_prod : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {F : Type u_3} [inst_2 : SMul 𝕜 F] (s : Set E)
  (t : Set F) (a : E) (b : F), max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.unop_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], AddOpposite.unop (OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceDiv : Lean.Meta.Simp.DSimproc
-- Init.Tactics
/-- `-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
 -/
Lean.Parser.Tactic.negConfigItem : Lean.ParserDescr
-- Init.Coe
instCoeOutOfCoeFun : {α : Sort u_1} → {β : Sort u_2} → [CoeFun α fun x => β] → CoeOut α β
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_centralizer_iff : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] {s : Set A} {z : A},
  z ∈ NonUnitalStarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.empty : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α}, Absorbs M s ∅
-- Mathlib.RingTheory.Ideal.Quotient.Over
/-- Given a prime `P` of `R` and an ideal `I` in an `R`-algebra `S`.
Suppose we can find a prime `P'` over `P`, not containing `I`,
then the number of primes of `S / I` over `P`
is strictly less than primes of `S` over `P` (provided they are finite).

The lemma is stated in terms of surjections for syntactic generality.  -/
Ideal.ncard_primesOver_lt_of_not_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
  Function.Surjective ⇑f →
    ∀ (P : Ideal R) (P' : Ideal S) [P'.IsPrime] [P'.LiesOver P],
      ¬RingHom.ker f.toRingHom ≤ P' → (P.primesOver S).Finite → (P.primesOver T).ncard < (P.primesOver S).ncard
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebraClass.coe_subtype : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Star A]
  [inst_3 : Module R A] {S : Type w''} [inst_4 : SetLike S A] [inst_5 : NonUnitalSubsemiringClass S A]
  [hSR : SMulMemClass S R A] [inst_6 : StarMemClass S A] (s : S),
  ⇑(NonUnitalStarSubalgebraClass.subtype s) = Subtype.val
-- Init.Data.ByteArray.Lemmas
ByteArray.emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.ExtTreeMap.unitOfList l cmp).size = l.length
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the signs of two nondegenerate oriented angles between points are negations of each other,
the oriented angles are negations of each other if and only if the unoriented angles are equal.  -/
EuclideanGeometry.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  p₁ ≠ p₂ →
    p₃ ≠ p₂ →
      p₄ ≠ p₅ →
        p₆ ≠ p₅ →
          (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -(EuclideanGeometry.oangle p₄ p₅ p₆).sign →
            (EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ ↔
              EuclideanGeometry.oangle p₁ p₂ p₃ = -EuclideanGeometry.oangle p₄ p₅ p₆)
-- Mathlib.Order.Lattice
lt_inf_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < min b c ↔ a < b ∧ a < c
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.totalSpaceMk_isClosedEmbedding : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [T1Space B] (x : B), Topology.IsClosedEmbedding (Bundle.TotalSpace.mk x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.maxKey?.isNone = t.isEmpty
-- Lean.Parser.Basic
Lean.Parser.termParser : optParam ℕ 0 → Lean.Parser.Parser
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.ruleSets.sizeOf_spec : ∀ (rs : Aesop.Frontend.RuleSets), sizeOf (Aesop.Frontend.Feature.ruleSets rs) = 1 + sizeOf rs
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.coe_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (σ : G → E) (hσ : Function.RightInverse σ ⇑S.rightHom),
  ⇑{ toFun := σ, rightInverse_rightHom := hσ } = σ
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_natTrailingDegree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p * q ≠ 0 → p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
-- Init.Data.UInt.Basic
/-- Convert a `USize` to `BitVec 64`, assuming that the system bit-width is 64.

This operation is intended for proof purposes.
 -/
USize.toBitVec64 : USize → System.Platform.numBits = 64 → BitVec 64
-- Init.System.IO
instMonadLiftBaseIOEIO : {ε : Type} → MonadLift BaseIO (EIO ε)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_unitIso : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B],
  (CategoryTheory.Sum.functorEquiv A A' B).unitIso = CategoryTheory.NatIso.ofComponents (fun F => F.isoSum) ⋯