mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} [inst : BEq α] (a : α)
  (motive :
    (x : Std.DHashMap.Internal.AssocList α fun x => β) → Std.DHashMap.Internal.AssocList.contains a x = true → Sort u_3)
  (k : α) (v : β) (es : Std.DHashMap.Internal.AssocList α fun x => β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true)
  (h_1 :
    (k : α) →
      (v : β) →
        (es : Std.DHashMap.Internal.AssocList α fun x => β) →
          (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true) →
            motive (Std.DHashMap.Internal.AssocList.cons k v es) h),
  (match Std.DHashMap.Internal.AssocList.cons k v es, h with
    | Std.DHashMap.Internal.AssocList.cons k v es, h => h_1 k v es h) =
    h_1 k v es h
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_trans : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃), ⇑(e.trans e') = ⇑e' ∘ ⇑e
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_exp : ∀ (z : ℂ), (Complex.exp z).arg = toIocMod Real.two_pi_pos (-Real.pi) z.im
-- Mathlib.Topology.GDelta.Basic
/-- To check that `s` is nowhere dense, it suffices to check that no point of `s`
is in the interior of `closure s`.  -/
isNowhereDense_iff_disjoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s ↔ Disjoint s (interior (closure s))
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.smul_kroneckerTMul : ∀ (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : Monoid S] [inst_6 : DistribMulAction S α] [inst_7 : SMulCommClass R S α] (r : S)
  (A : Matrix l m α) (B : Matrix n p β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (r • A) B = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hom_hom_id : ∀ {X : NonemptyFinLinOrd}, LinOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiff.extend_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] [T2Space M]
  [inst_12 : One M'] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M} {f : ↥U → M'},
  HasCompactMulSupport f → ContMDiff I I' n f → ContMDiff I I' n (Function.extend Subtype.val f 1)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.exists_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Nonempty ι]
  [NeZero 2], ∃ i, P.root i ≠ 0
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_inter_Iic : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a b : α}, Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.sum_polar_sub_repr_sq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N)
  (bm : Module.Basis ι R M) (x : M),
  (Finsupp.linearCombination R (QuadraticMap.polarSym2 ⇑Q ∘ Sym2.map ⇑bm)) (bm.repr x).sym2Mul -
      (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) =
    Q x
-- Lean.Meta.Tactic.Grind.PP
/-- Returns `true` if `e` is a support-like application.
Recall that equivalence classes that contain only support applications are displayed in the "others" category.
 -/
Lean.Meta.Grind.isSupportApp : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Pi
/-- A variant of `Module.pi_induction` that assumes `AddCommGroup` instead of `AddCommMonoid`.  -/
Module.pi_induction' : ∀ {ι : Type v} [Finite ι] (R : Type u_1) [inst : Ring R]
  (motive : (N : Type u) → [inst_1 : AddCommGroup N] → [Module R N] → Prop)
  (motive' : (N : Type (max u v)) → [inst_1 : AddCommGroup N] → [Module R N] → Prop),
  (∀ {N : Type u} {N' : Type (max u v)} [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
      [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N') →
    (∀ {N N' : Type (max u v)} [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
        [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N') →
      motive PUnit.{u + 1} →
        (∀ {N : Type u} {N' : Type (max u v)} [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
            [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')) →
          ∀ (M : ι → Type u) [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)],
            (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_cast : ∀ {w v i : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).getMsbD i = x.getMsbD i
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A strongly measurable function is measurable.  -/
MeasureTheory.StronglyMeasurable.measurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β],
  MeasureTheory.StronglyMeasurable f → Measurable f
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_vec2 : ∀ {α : Type u} [inst : Zero α] (a b : α), Matrix.diagonal ![a, b] = !![a, 0; 0, b]
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.has_cokernels : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasCokernels C
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LeapSecond.mk.inj : ∀ {transitionTime correction transitionTime_1 correction_1 : ℤ},
  { transitionTime := transitionTime, correction := correction } =
      { transitionTime := transitionTime_1, correction := correction_1 } →
    transitionTime = transitionTime_1 ∧ correction = correction_1
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.extend.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (n : ℕ),
  IsAdicComplete.StrictMono.extend ha f n = Submodule.factorPow I N ⋯ ∘ₗ f n
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.monotone_iff_Icc : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.supSum.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] {inst_1 : DecidableEq α} [inst_2 : DecidableEq α] (𝒜 𝒜_1 : Finset (Finset α)),
  𝒜 = 𝒜_1 → AhlswedeZhang.supSum 𝒜 = AhlswedeZhang.supSum 𝒜_1
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepSet.iIndepFun_indicator : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [inst : Zero β] [inst_1 : One β]
  {m : MeasurableSpace β} {s : ι → Set Ω},
  ProbabilityTheory.Kernel.iIndepSet s κ μ →
    ProbabilityTheory.Kernel.iIndepFun (fun n => (s n).indicator fun _ω => 1) κ μ
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R n = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R (n - 2)
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_dvd : ∀ (xs : Lean.Omega.IntList) {a : ℤ}, a ∈ xs → ↑xs.gcd ∣ a
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsColimitsOfShape J F]
  [CategoryTheory.Limits.ReflectsColimitsOfShape J G], CategoryTheory.Limits.ReflectsColimitsOfShape J (F.comp G)
-- Mathlib.Algebra.Torsor.Defs
Torsor.mk : {G : outParam (Type u_1)} →
  {P : Type u_2} →
    [inst : Group G] →
      [toMulAction : MulAction G P] →
        [toSDiv : SDiv G P] →
          [nonempty : Nonempty P] →
            (∀ (p₁ p₂ : P), (p₁ /ₛ p₂) • p₂ = p₁) → (∀ (g : G) (p : P), g • p /ₛ p = g) → Torsor G P
-- Init.Control.Lawful.MonadLift.Instances
StateT.instLawfulMonadLift : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {σ : Type u}, LawfulMonadLift m (StateT σ m)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
EisensteinSeries.G2_slash_action : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map 2 γ EisensteinSeries.G2 = EisensteinSeries.G2 - EisensteinSeries.D2 γ
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {p q : Polynomial R},
  p.IsPrimitive → (p ∣ q ↔ Polynomial.map (algebraMap R K) p ∣ Polynomial.map (algebraMap R K) q)
-- Lean.Parser.Extra
Lean.Parser.charLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.assoc_symm_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (m : M) (n : N) (p : P),
  (TensorProduct.assoc R M N P).symm (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = m ⊗ₜ[R] n ⊗ₜ[R] p
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instBot : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Bot (NonUnitalSubsemiring R)
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.inv_nonneg' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ r⁻¹
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_ground : ∀ {α : Type u_1} {M : Matroid α}, M✶.E = M.E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The central point of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.zero : CategoryTheory.Limits.WalkingSpan
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_zero_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []), List.maxIdxOn f xs h = 0 ↔ ∀ x ∈ xs, f x ≤ f (xs.head h)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The map `π₀ X → π₀ Y` induced by a morphism `X ⟶ Y` of simplicial sets.  -/
SSet.mapπ₀ : {X Y : SSet} → (X ⟶ Y) → X.π₀ → Y.π₀
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tprod_nonneg : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α]
  [inst_2 : Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] {f : ι → α},
  (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∏'[L] (x : ι), f x
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace : {ι : Type u_1} → (α : ι → Type u) → [U : (i : ι) → UniformSpace (α i)] → UniformSpace ((i : ι) → α i)
-- Mathlib.MeasureTheory.Group.Arithmetic
Units.instMeasurableConstSMul : ∀ {M : Type u_4} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : Monoid M] [inst_2 : MulAction M β]
  [MeasurableConstSMul M β], MeasurableConstSMul Mˣ β
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.isCycle_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → 2 ≤ l.length → l.formPerm.IsCycle
-- Mathlib.Data.List.Lattice
List.bagInter.eq_def : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : List α),
  x.bagInter x_1 =
    match x, x_1 with
    | [], x => []
    | x, [] => []
    | a :: l₁, l₂ => if List.elem a l₂ = true then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂
-- Init.Data.String.Defs
String.default_eq : default = ""
-- Mathlib.GroupTheory.Commutator.Finite
Subgroup.index_center_le_pow : ∀ (G : Type u_1) [inst : Group G] [Finite ↑(commutatorSet G)] [inst_2 : Group.FG G],
  (Subgroup.center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
-- Init.NotationExtra
Lean.unbracketedExplicitBinders : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.h : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Analysis.Analytic.Composition
/-- Given a formal multilinear series `p`, a composition `c` of `n` and the index `i` of a
block of `c`, we may define a function on `Fin n → E` by picking the variables in the `i`-th block
of `n`, and applying the corresponding coefficient of `p` to these variables. This function is
called `p.applyComposition c v i` for `v : Fin n → E` and `i : Fin c.length`.  -/
FormalMultilinearSeries.applyComposition : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : CommRing 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [inst_7 : IsTopologicalAddGroup E] →
                      [inst_8 : ContinuousConstSMul 𝕜 E] →
                        [inst_9 : IsTopologicalAddGroup F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] →
                            FormalMultilinearSeries 𝕜 E F →
                              {n : ℕ} → (c : Composition n) → (Fin n → E) → Fin c.length → F
-- Mathlib.Topology.Connected.Basic
irreducibleComponent_subset_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, irreducibleComponent x ⊆ connectedComponent x
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_mul_left : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul M M] (a b c : M),
  edist (a * b) (a * c) = edist b c
-- Mathlib.FieldTheory.Differential.Basic
Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1 : ∀ {F : Type u_2} [inst : Field F] [inst_1 : Differential F] [inst_2 : CharZero F] {K : Type u_3} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Differential K] [DifferentialAlgebra F K] (B : IntermediateField F K)
  [inst_7 : FiniteDimensional F ↥B], DifferentialAlgebra (↥B) K
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroTopOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C], ⊤.ContainsZero
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- A two-sided ideal of a ring `R` is a subset of `R` that contains `0` and is closed under addition,
negation, and absorbs multiplication on both sides.
 -/
TwoSidedIdeal : (R : Type u_1) → [NonUnitalNonAssocRing R] → Type u_1
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : τ →₀ ℕ} (c : R) {a : τ},
  a ∈ s.support → a ∉ Set.range f → (MvPolynomial.killCompl hf) ((MvPolynomial.monomial s) c) = 0
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_eq_zero_iff : ∀ {σ : Type u_1} {R : Type u_5} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R]
  (d : σ →₀ R), Finsupp.degree d = 0 ↔ d = 0
-- Mathlib.SetTheory.ZFC.Class
/-- The **Burali-Forti paradox**: ordinals form a proper class.  -/
ZFSet.isOrdinal_notMem_univ : ZFSet.IsOrdinal ∉ Class.univ
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.findIdxNth.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (s : ℕ) (h_1 : (x s : ℕ) → motive [] x s)
  (h_2 : (a : α) → (xs : List α) → (s : ℕ) → motive (a :: xs) 0 s)
  (h_3 : (a : α) → (xs : List α) → (n s : ℕ) → motive (a :: xs) n.succ s),
  (match a :: xs, 0, s with
    | [], x, s => h_1 x s
    | a :: xs, 0, s => h_2 a xs s
    | a :: xs, n.succ, s => h_3 a xs n s) =
    h_2 a xs s
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.instIsStableUnderPrecompCompClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C),
  CategoryTheory.HomRel.IsStableUnderPrecomp (CategoryTheory.HomRel.CompClosure r)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.one_sub_goldenRatio : 1 - Real.goldenConj = Real.goldenRatio
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instFunLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N],
  MonoidHom.instFunLike = { coe := fun f => (↑f).toFun, coe_injective := ⋯ }
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Construct an affine isometry equivalence by verifying the relation between the map and its
linear part at one base point. Namely, this function takes a map `e : P₁ → P₂`, a linear isometry
equivalence `e' : V₁ ≃ᵢₗ[k] V₂`, and a point `p` such that for any other point `p'` we have
`e p' = e' (p' -ᵥ p) +ᵥ e p`.  -/
AffineIsometryEquiv.mk' : {𝕜 : Type u_1} →
  {V₁ : Type u_3} →
    {V₂ : Type u_5} →
      {P₁ : Type u_8} →
        {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' : V₁ ≃ₗᵢ[𝕜] V₂) → (p : P₁) → (∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) → P₁ ≃ᵃⁱ[𝕜] P₂
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'}, MDiffAt (-f) z ↔ MDiffAt f z
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β} {he : (Std.Internal.List.Const.alterKey k f l).isEmpty = false},
      Std.Internal.List.minKey (Std.Internal.List.Const.alterKey k f l) he = k ↔
        (f (Std.Internal.List.getValue? k l)).isSome = true ∧
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Lean.Elab.SyntheticMVars
/-- Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.

The `tacticCode` syntax comprises the whole `by ...` expression.

If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
 -/
Lean.Elab.Term.runTactic : Lean.MVarId → Lean.Syntax → Lean.Elab.Term.TacticMVarKind → optParam Bool true → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_iff_of_iso : ∀ {X Y : SSet} (e : X ≅ Y), X.Finite ↔ Y.Finite
-- Mathlib.Data.Vector.Basic
List.Vector.toList_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α n) (f : α → β),
  (List.Vector.map f v).toList = List.map f v.toList
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Cyclotomic extensions are abelian.  -/
IsCyclotomicExtension.isMulCommutative : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsCyclotomicExtension S A B] [IsDomain B], IsMulCommutative (B ≃ₐ[A] B)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circle average of a continuous function is itself continuous, as a function
of the radius.
 -/
Real.ContinuousOn.circleAverage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {s : Set ℝ} {c : ℂ},
  ContinuousOn f {z | ‖z - c‖ ∈ s} → (∀ r ∈ s, 0 ≤ r) → ContinuousOn (Real.circleAverage f c) s
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.filterTrieM.go : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} →
      [Monad m] →
        [Inhabited σ] →
          (σ → α → m σ) →
            (α → m (ULift.{u_1, 0} Bool)) →
              σ →
                ℕ →
                  Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
                    m (Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) × σ)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
and conversion to normal form on `U` agree at `x`.
 -/
toMeromorphicNFOn_eq_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → toMeromorphicNFOn f U x = toMeromorphicNFAt f x x
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_bot : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊥ = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- An effective epi which has a kernel pair is a regular epi.  -/
CategoryTheory.regularEpiOfEffectiveEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B X : C} →
      (f : X ⟶ B) →
        [CategoryTheory.Limits.HasPullback f f] → [CategoryTheory.EffectiveEpi f] → CategoryTheory.RegularEpi f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h' : k ∈ Std.ExtDTreeMap.filterMap f t), (f k (t.get k ⋯)).isSome = true
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsCondKernelCDF (ProbabilityTheory.stieltjesOfMeasurableRat f ⋯) κ ν
-- Mathlib.Algebra.GroupWithZero.Center
Set.zero_mem_centralizer : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {s : Set M₀}, 0 ∈ s.centralizer
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.Hom.inhabited : {J : Type w} → Inhabited (CategoryTheory.Limits.WidePullbackShape.Hom none none)