mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Ultra
/-- In a group with an ultrametric norm, closed balls around 1 of positive radius are open subgroups.
 -/
IsUltrametricDist.closedBall_openSubgroup : (S : Type u_1) → [inst : SeminormedGroup S] → [IsUltrametricDist S] → {r : ℝ} → 0 < r → OpenSubgroup S
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FP`. This is the preferred spelling over `FP.cons'`.  -/
Hindman.FP.cons : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → a.head * m ∈ Hindman.FP a
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instIsIsoτ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.τ₃
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Composition of a map on a product with the exchange of the product factors  -/
ContinuousLinearMap.coprod_comp_prodComm : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] [inst_10 : ContinuousAdd M] (f : M₂ →L[R] M) (g : M₃ →L[R] M),
  f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂) = g.coprod f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.insertMany m l) k =
    (List.findSomeRev?
          (fun x_2 =>
            match x_2 with
            | (a, b) => if (a == k) = true then some b else none)
          l).or
      (Std.DHashMap.Const.get? m k)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_iff_filter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (nhdsWithin x s)
-- Init.Data.Array.Lemmas
Array.append_left_inj : ∀ {α : Type u_1} {xs₁ xs₂ : Array α} (ys : Array α), xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂
-- Init.Data.Int.DivMod.Lemmas
Int.ofNat_dvd_right : ∀ {n : ℕ} {z : ℤ}, z ∣ ↑n ↔ z.natAbs ∣ n
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The natural ring hom from a subsemiring of semiring `R` to `R`.  -/
SubsemiringClass.subtype : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] → [inst_1 : SetLike S R] → [hSR : SubsemiringClass S R] → (s : S) → ↥s →+* R
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_powers : ∀ {M : Type u_1} [inst : Monoid M] (n : M), n ∈ Submonoid.powers n
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  (Submodule.span R s).annihilator = ⨅ g, (LinearMap.toSpanSingleton R M ↑g).ker
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.isoCycles₂ A =
    CategoryTheory.ShortComplex.cyclesMapIso' (groupHomology.isoShortComplexH2 A)
      (HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 2).leftHomologyData
      (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.comp_apply_eq₂ : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁}
  [RingHomInvPair σ σ'] {x : R₂}, σ (σ' x) = x
-- Mathlib.Topology.Algebra.Polynomial
isClosedMap_pow : ∀ (R : Type u_2) [inst : NormedRing R] [IsAbsoluteValue norm] [ProperSpace R] (n : ℕ), IsClosedMap fun x => x ^ n
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive monoid with multiplication `R`, `AddSubmonoid.sumSq R` is the submonoid of sums of
squares in `R`.
 -/
AddSubmonoid.sumSq : (T : Type u_2) → [inst : AddMonoid T] → [Mul T] → AddSubmonoid T
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_mono : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s t : Set M},
  (∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) →
    ChartedSpace.LiftPropOn P g t → s ⊆ t → ChartedSpace.LiftPropOn P g s
-- Mathlib.Algebra.Order.Archimedean.Basic
instIsCodirectedOrder : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R], IsCodirectedOrder R
-- Std.Sync.Mutex
/-- Condition variable, a synchronization primitive to be used with a `BaseMutex` or `Mutex`.

The thread that wants to modify the shared variable must:
1. Lock the `BaseMutex` or `Mutex`
2. Work on the shared variable
3. Call `Condvar.notifyOne` or `Condvar.notifyAll` after it is done. Note that this may be done
   before or after the mutex is unlocked.

If working with a `Mutex` the thread that waits on the `Condvar` can use `Mutex.atomicallyOnce`
to wait until a condition is true. If working with a `BaseMutex` it must:
1. Lock the `BaseMutex`.
2. Do one of the following:
  - Use `Condvar.waitUntil` to (potentially repeatedly wait) on the condition variable until
     the condition is true.
  - Implement the waiting manually by:
    1. Checking the condition
    2. Calling `Condvar.wait` which releases the `BaseMutex` and suspends execution until the
       condition variable is notified.
    3. Check the condition and resume waiting if not satisfied.
 -/
Std.Condvar : Type
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.invOf_fromBlocks_zero₂₁_eq : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α)
  [inst_5 : Invertible A] [inst_6 : Invertible D] [inst_7 : Invertible (Matrix.fromBlocks A B 0 D)],
  ⅟(Matrix.fromBlocks A B 0 D) = Matrix.fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
-- Init.Data.SInt.Lemmas
Int8.toISize_neg_of_ne : ∀ {x : Int8}, x ≠ -128 → (-x).toISize = -x.toISize
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- The coercion between `GenContFract` happens on the head term
and all numerator-denominator pairs componentwise.  -/
GenContFract.coeFn : {α : Type u_1} → {β : Type u_2} → [Coe α β] → GenContFract α → GenContFract β
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- If x is in `spinGroup Q`, then `involute x` is equal to x.  -/
spinGroup.involute_eq : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → CliffordAlgebra.involute x = x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSlice : (α : Type u_1) → (α → Type u_2) → Type (max u_2 u_1)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff `range 𝓕` is equicontinuous
at `x₀` within `S`, i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀` within `S`.  -/
equicontinuousWithinAt_iff_range : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X} {x₀ : X}, EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt Subtype.val S x₀
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Real.cosh`.  -/
Real.hasSum_cosh : ∀ (r : ℝ), HasSum (fun n => r ^ (2 * n) / ↑(2 * n).factorial) (Real.cosh r)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_apply' : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (k' : o) (j : n' k'),
  Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = if h : k = k' then M k i (cast ⋯ j) else 0
-- Mathlib.Algebra.Ring.Prod
Prod.instNonAssocRing : {R : Type u_1} → {S : Type u_3} → [NonAssocRing R] → [NonAssocRing S] → NonAssocRing (R × S)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (K.iCycles i) = k
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTraceAux.eq_1 : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] (a : K),
  Algebra.normalizedTraceAux✝ F K a =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (Algebra.trace F ↥F⟮a⟯) (IntermediateField.AdjoinSimple.gen F a)
-- Mathlib.Data.Set.Subset
Set.preimage_val_sInter : ∀ {α : Type u_2} {A : Set α} {S : Set (Set α)}, Subtype.val ⁻¹' ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_div_const_iff' : ∀ {α : Type u} {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [ContinuousDiv G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => f x / b) l (nhds (c / b)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv_assoc : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] (X : D)
  (f : CategoryTheory.CostructuredArrow L X) {Z : H} (h : (L.leftKanExtension F).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f)
      (CategoryTheory.CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).inv h) =
    CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom) h)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).left.obj X_1 =
    X.obj
      (match CategoryTheory.WithTerminal.incl.obj X_1 with
      | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
      | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_add_not_infinitePos : ∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The fitted value `A x` minimizes the distance to `y` among points in `A.range`
if and only if the adjoint of `A` sends the residual `y - A x` to zero.  -/
ContinuousLinearMap.norm_eq_iInf_range_iff_adjoint_apply_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (y : F) (x : E),
  ‖y - A x‖ = ⨅ z, ‖y - ↑z‖ ↔ (ContinuousLinearMap.adjoint A) (y - A x) = 0
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk'.inj : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst : Semiring A} {inst_1 : Monoid G}
  {inst_2 : AddCommMonoid V} {inst_3 : AddCommMonoid W} {inst_4 : Module A V} {inst_5 : Module A W}
  {ρ : Representation A G V} {σ : Representation A G W} {toIntertwiningMap : ρ.IntertwiningMap σ} {invFun : W → V}
  {left_inv : autoParam (Function.LeftInverse invFun toIntertwiningMap.toFun) Equiv.left_inv._autoParam}
  {right_inv : autoParam (Function.RightInverse invFun toIntertwiningMap.toFun) Equiv.right_inv._autoParam}
  {toIntertwiningMap_1 : ρ.IntertwiningMap σ} {invFun_1 : W → V}
  {left_inv_1 : autoParam (Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun) Equiv.left_inv._autoParam}
  {right_inv_1 : autoParam (Function.RightInverse invFun_1 toIntertwiningMap_1.toFun) Equiv.right_inv._autoParam},
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
        right_inv := right_inv_1 } →
    toIntertwiningMap = toIntertwiningMap_1 ∧ invFun = invFun_1
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_add_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ⌊a + 1⌋₊ = ⌊a⌋₊ + 1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToBackwardSearcherModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {σ : String.Slice → Type}
  [inst_1 : String.Slice.Pattern.ToBackwardSearcher pat σ]
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id],
  (∀ (s : String.Slice),
      String.Slice.Pattern.Model.IsValidRevSearchFrom pat s.endPos
        (String.Slice.Pattern.ToBackwardSearcher.toSearcher pat s).toList) →
    String.Slice.Pattern.Model.LawfulToBackwardSearcherModel pat
-- Mathlib.Algebra.Group.Subgroup.Order
instIsModularLatticeSubgroup : ∀ {C : Type u_1} [inst : CommGroup C], IsModularLattice (Subgroup C)
-- Mathlib.Algebra.Group.Units.Equiv
AddGroup.addLeft_bijective : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Function.Bijective fun x => a + x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filter_key_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool}, Std.ExtDTreeMap.filter (fun a x => f a) t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = false
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_of_comp_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : CategoryTheory.ShortComplex.QuasiIso φ']
  [hφφ' : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')],
  CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_eq_mk_iff' : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {g₁ g₂ : GL n R},
  Matrix.ProjGenLinGroup.mk g₁ = Matrix.ProjGenLinGroup.mk g₂ ↔ ∃ z ∈ Subgroup.center (GL n R), g₁ * z = g₂
-- Mathlib.Computability.DFA
/-- `M.comap f` pulls back the alphabet of `M` along `f`. In other words, it applies `f` to the input
before passing it to `M`.
 -/
DFA.comap : {α : Type u} → {σ : Type v} → {α' : Type u_1} → (α' → α) → DFA α σ → DFA α' σ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mk.sizeOf_spec : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : SizeOf A] [inst_5 : SizeOf B] (toMonoidHom : A →* B)
  (continuous_toFun : autoParam (Continuous (↑toMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam),
  sizeOf { toMonoidHom := toMonoidHom, continuous_toFun := continuous_toFun } =
    1 + sizeOf toMonoidHom + sizeOf continuous_toFun
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_coe_def : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) (q : ↥(nonZeroDivisors (Polynomial K))),
  RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p q }
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Array (List α) → Sort u_2) (a : α) (t : List α) (acc : Array α)
  (r : Array (List α)) (h_1 : (acc : Array α) → (r : Array (List α)) → motive [] acc r)
  (h_2 : (a : α) → (t : List α) → (acc : Array α) → (r : Array (List α)) → motive (a :: t) acc r),
  (match a :: t, acc, r with
    | [], acc, r => h_1 acc r
    | a :: t, acc, r => h_2 a t acc r) =
    h_2 a t acc r
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive group, if it admits an
injective map that preserves `0` and `+` to an additive group.  -/
Function.Injective.addGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : AddGroup M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → AddGroup M₁
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.mul : {R : Type u_1} → {X : Type u_2} → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X → FreeAlgebra.Pre R X
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isCharTwoJEqZeroNF_of_char_two : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharTwoJEqZeroNF] [CharP F 2],
  W.j = 0
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M' → M} {x : M'}
  {s : Set M'}, ContMDiffWithinAt I' (I.transContinuousLinearEquiv e) n f s x ↔ ContMDiffWithinAt I' I n f s x
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.HasAffineProperty.diagonal_affineProperty_isLocal : ∀ {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [Q.IsLocal], Q.diagonal.IsLocal
-- Init.Data.String.Defs
List.toByteArray_asString : ∀ {l : List Char}, (String.ofList l).toByteArray = l.utf8Encode
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.mem_vanishingIdeal_singleton_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3} (x : σ → K)
  (p : MvPolynomial σ k), p ∈ MvPolynomial.vanishingIdeal k {x} ↔ (MvPolynomial.aeval x) p = 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
Lean.Meta.Grind.Arith.CommRing.addThresholdMessage : Lean.Meta.Grind.Goal → Lean.Grind.Config → Array Lean.MessageData → IO (Array Lean.MessageData)
-- Mathlib.Topology.Sheaves.Stalks
/-- For surjectivity, we are given an arbitrary section `t` and need to find a preimage for it.
We claim that it suffices to find preimages *locally*. That is, for each `x : U` we construct
a neighborhood `V ≤ U` and a section `s : F.obj (op V))` such that `f.app (op V) s` and `t`
agree on `V`.  -/
TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X),
  (∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) →
    (∀ (t : CC (G.obj.obj (Opposite.op U))),
        ∀ x ∈ U,
          ∃ V,
            ∃ (_ : x ∈ V),
              ∃ iVU s,
                (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op V))) s =
                  (CategoryTheory.ConcreteCategory.hom (G.obj.map iVU.op)) t) →
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier : ∀ {R : CommRingCat} [IsDomain ↑R], IrreducibleSpace ↥(AlgebraicGeometry.Spec R)
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_ne_bot : ∀ (x : ENNReal), ↑x ≠ ⊥
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.comp_homologyMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.π
      (CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
          (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom h₂.ι))) =
    CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_div : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Div M] (f g : α → M), ↑(f / g) = ↑f / ↑g
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), ContDiffAt 𝕜 n (fun x => Φ x i) x) → ContDiffAt 𝕜 n Φ x
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_triple : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {x y z : α},
  x ≠ y → y ≠ z → x ≠ z → {x, y, z}.infsep = min (min (dist x y) (dist x z)) (dist y z)
-- Init.Data.BitVec.Lemmas
BitVec.instCommutativeHAnd : ∀ {w : ℕ}, Std.Commutative fun x y => x &&& y