mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SingularSet
/-- The functor associating the *singular simplicial set* to a topological space.

Let `X : TopCat.{u}` be a topological space.
Then the singular simplicial set of `X`
has as `n`-simplices the continuous maps `ULift.{u} (stdSimplex ℝ (Fin (n + 1))) → X`.
Here, `stdSimplex ℝ (Fin (n + 1))` is the standard topological `n`-simplex,
defined as `{ f : Fin (n + 1) → ℝ // (∀ i, 0 ≤ f i) ∧ ∑ i, f i = 1 }` with its subspace topology.  -/
TopCat.toSSet : CategoryTheory.Functor TopCat SSet
-- Mathlib.Topology.Ultrafilter
clusterPt_iff_ultrafilter : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f : Filter X}, ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ nhds x
-- Mathlib.RingTheory.Congruence.Basic
RingCon.toCon_eq_top : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c : RingCon R}, c.toCon = ⊤ ↔ c = ⊤
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateMData!Impl : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E] (z : ℂ),
  DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
      z ∈ Complex.HadamardThreeLines.verticalStrip 0 1 → ‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖
-- Lean.DocString.Parser
/-- Construct a “fake” atom with the given string content and source information.

Normally, atoms are always substrings of the original input; however, Verso's concrete syntax
is different enough from Lean's that this isn't always a good match.
 -/
Lean.Doc.Parser.fakeAtom : String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.Parser.ParserFn
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csSup_empty : sSup ∅ = 0
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopInverse_map : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V c.symm} (f : X ⟶ Y),
  (HomologicalComplex.unopInverse V c).map f = Quiver.Hom.op { f := fun i => (f.f i).op, comm' := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.mk.injEq : ∀ (n : ℕ) (value : BitVec n) (n_1 : ℕ) (value_1 : BitVec n_1),
  ({ n := n, value := value } = { n := n_1, value := value_1 }) = (n = n_1 ∧ value ≍ value_1)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.isSymmetricAlgebra_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsSymmetricAlgebra (SymmetricAlgebra.ι R M)
-- Mathlib.Data.List.SplitLengths
List.length_splitLengths_getElem_eq : ∀ {α : Type u_1} (l : List α) (sz : List ℕ) {i : ℕ} (hi : i < sz.length),
  (List.take (i + 1) sz).sum ≤ l.length → (sz.splitLengths l)[i].length = sz[i]
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
/-- The degree-sum formula.  This is also known as the handshaking lemma, which might
more specifically refer to `SimpleGraph.even_card_odd_degree_vertices`.  -/
SimpleGraph.sum_degrees_eq_twice_card_edges : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  ∑ v, G.degree v = 2 * G.edgeFinset.card
-- Init.Grind.Injective
Lean.Grind.leftInvUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.Order.Hom.Esakia
OrderIsoClass.toPseudoEpimorphismClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β], PseudoEpimorphismClass F α β
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.smul_map_volume_mul_right : ∀ {a : ℝ},
  a ≠ 0 → ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun x => x * a) MeasureTheory.volume = MeasureTheory.volume
-- Mathlib.Algebra.Group.Finsupp
Finsupp.nsmul_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] (n : ℕ) (f : ι →₀ M) (x : ι), (n • f) x = n • f x
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.instHasBinaryProductsOfOrderTop : ∀ {α : Type u} [inst : SemilatticeInf α] [OrderTop α], CategoryTheory.Limits.HasBinaryProducts α
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.ColimitType.AddGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → AddGroup (RingCat.Colimits.ColimitType F)
-- Init.Grind.ToInt
Lean.Grind.IntInterval.mem : Lean.Grind.IntInterval → ℤ → Prop
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.image : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A]
  [SMulCommClass S A A] [IsScalarTower R S A], QuasispectrumRestricts a f → f '' quasispectrum S a = quasispectrum R a
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Reflexive-transitive closure of `Red.Step`  -/
FreeGroup.Red : {α : Type u} → List (α × Bool) → List (α × Bool) → Prop
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.h : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.exists_comap_galRestrict_eq : ∀ (R : Type u_1) (K : Type u_2) (L : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [inst_7 : Algebra S L] [inst_8 : Algebra K L] [inst_9 : Algebra R L] [inst_10 : IsScalarTower R S L]
  [inst_11 : IsScalarTower R K L] [inst_12 : IsIntegralClosure S R L] [FiniteDimensional K L] [IsDedekindDomain R]
  [inst_15 : IsGalois K L] {p : Ideal R} {P₁ P₂ : Ideal S},
  P₁ ∈ p.primesOver S → P₂ ∈ p.primesOver S → ∃ σ, Ideal.comap ((galRestrict R K L S) σ) P₁ = P₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DHashMap.map f m).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) m.toList)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Taking the affine span of a set, adding a point and taking the span again produces the same
results as adding the point to the set and taking the span.  -/
affineSpan_insert_affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (ps : Set P), affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Init.Meta.Defs
/-- Converts a name to a string.

- If `escape` is `true`, then escapes name components using `«` and `»` to ensure that
  those names that can appear in source files round trip.
  Names with number components, anonymous names, and names containing `»` might not round trip.
  Furthermore, "pseudo-syntax" produced by the delaborator, such as `_`, `#0` or `?u`, is not escaped.
- The optional `isToken` function is used when `escape` is `true` to determine whether more
  escaping is necessary to avoid parser tokens.
  The insertion algorithm works so long as parser tokens do not themselves contain `«` or `»`.
 -/
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.toStringWithToken : Lean.Name → optParam Bool true → (String → Bool) → String
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
LinearMap.ker_tensorProductMk : ∀ {R : Type u_1} [inst : CommRing R] (Q : Type u_5) [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {I : Ideal R},
  ((TensorProduct.mk R (R ⧸ I) Q) 1).ker = I • ⊤
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_iInf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Injective ⇑f → ∀ (S : ι → AddSubmonoid M), AddSubmonoid.comap f (⨅ i, AddSubmonoid.map f (S i)) = iInf S
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeSubgraph_injective : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), Function.Injective SimpleGraph.Subgraph.coeSubgraph
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.localRingHom_surjective : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  f.SurjectiveOnStalks →
    ∀ (P : Ideal R) [inst_2 : P.IsPrime] (Q : Ideal S) [inst_3 : Q.IsPrime] (e : P = Ideal.comap f Q),
      Function.Surjective ⇑(Localization.localRingHom P Q f e)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The underlying function of `Proj ℬ ⟶ Proj 𝒜` on the level of points.  -/
AlgebraicGeometry.ProjectiveSpectrum.comapFun : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        [inst : CommRing A] →
          [inst_1 : SetLike σ A] →
            [inst_2 : AddSubgroupClass σ A] →
              [inst_3 : CommRing B] →
                [inst_4 : SetLike τ B] →
                  [inst_5 : AddSubgroupClass τ B] →
                    {𝒜 : ℕ → σ} →
                      {ℬ : ℕ → τ} →
                        [inst_6 : GradedRing 𝒜] →
                          [inst_7 : GradedRing ℬ] →
                            (f : 𝒜 →+*ᵍ ℬ) →
                              HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                                ProjectiveSpectrum ℬ → ProjectiveSpectrum 𝒜
-- Mathlib.RingTheory.IsTensorProduct
_private.Mathlib.RingTheory.IsTensorProduct.0.IsTensorProduct.assocAux.eq_1 : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] (f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g),
  IsTensorProduct.assocAux✝ f hf g hg =
    (((((((TensorProduct.congr (LinearEquiv.refl R M₁) (LinearEquiv.restrictScalars R hg.equiv.symm)).trans
                            (TensorProduct.comm R M₁ (TensorProduct S M₂ M₃))).trans
                        (LinearEquiv.restrictScalars R
                          (TensorProduct.AlgebraTensorModule.congr (TensorProduct.comm S M₂ M₃)
                            (LinearEquiv.refl R M₁)))).trans
                    (LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.assoc R S S M₃ M₂ M₁))).trans
                (LinearEquiv.restrictScalars R (TensorProduct.comm S M₃ (TensorProduct R M₂ M₁)))).trans
            (LinearEquiv.restrictScalars R
              (TensorProduct.congr
                (let __spread.0 := TensorProduct.comm R M₂ M₁;
                { toAddHom := (↑__spread.0).toAddHom, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ })
                (LinearEquiv.refl S M₃)))).trans
        (LinearEquiv.restrictScalars R
          (TensorProduct.congr (AddEquiv.linearEquiv S hf.equiv.toAddEquiv) (LinearEquiv.refl S M₃)))).symm
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.diseq0_to_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Data.Matrix.Mul
dotProduct_comm : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : AddCommMonoid α] [inst_2 : CommMagma α] (v w : m → α),
  v ⬝ᵥ w = w ⬝ᵥ v
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_toAddSubmonoid : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] (a : M)
  (S : AddSubgroup A), (a • S).toAddSubmonoid = a • S.toAddSubmonoid
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_rco : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLT = true))
          t.toList
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.foldEntries : Lean.NameMap Lean.Name → Array (Array (Lean.Name × Lean.Name)) → Lean.NameMap Lean.Name
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap_apply_single : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : SMulCommClass R S S] {M N : Submodule R S} {ι : Type u_5} (m : ι → ↥M)
  (i : ι) (n : ↥N), ((Submodule.mulLeftMap N m) fun₀ | i => n) = ↑(m i) * ↑n
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ {H : Type u_2} [inst_1 : Group H] (ϕ : H →* G), Function.Injective ⇑ϕ → IsPGroup p H
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.closeFence : Lean.Doc.Parser.BlockCtxt → ℕ → ℕ → Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- In a (nontrivial) complex Banach algebra, every element has nonempty spectrum.  -/
spectrum.nonempty : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A),
  (spectrum ℂ a).Nonempty
-- Init.Data.String.Lemmas.Splits
String.splits_singleton_iff : ∀ {s : String} {p : s.Pos} {c : Char} {t : String},
  p.Splits (String.singleton c) t ↔
    ∃ (h : s.startPos ≠ s.endPos), p = s.startPos.next h ∧ s.startPos.get h = c ∧ s = String.singleton c ++ t
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α m β] →
          [Std.Iterators.Finite α m] →
            {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
              Std.Iterators.FinitenessRelation (Std.Iterators.Types.TakeWhile α m β P) m
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.maximalIdeal_le_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (I : Ideal R), IsLocalRing.maximalIdeal R ≤ I.jacobson
-- Lean.Level
Lean.Level.max.inj : ∀ {a a_1 a_2 a_3 : Lean.Level}, a.max a_1 = a_2.max a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.noConfusionType : Sort v✝ → Lean.Meta.Grind.Result✝ → Lean.Meta.Grind.Result✝ → Sort v✝
-- Lean.Compiler.IR.Basic
Lean.IR.instReprArg : Repr Lean.IR.Arg
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.mk.sizeOf_spec : ∀ (nextIdx : ℕ) (lmap : Std.HashMap Lean.LMVarId Lean.Level) (emap : Std.HashMap Lean.MVarId Lean.Expr)
  (mctx : Lean.MetavarContext),
  sizeOf { nextIdx := nextIdx, lmap := lmap, emap := emap, mctx := mctx } =
    1 + sizeOf nextIdx + sizeOf lmap + sizeOf emap + sizeOf mctx
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).m = CategoryTheory.SmallObject.functorObjLeft f πX
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Any function from `α` to `β` extends uniquely to a group homomorphism from the free group over
`α` to the free group over `β`.  -/
FreeGroup.map : {α : Type u} → {β : Type v} → (α → β) → FreeGroup α →* FreeGroup β
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toArray_iter : ∀ {β : Type w} {array : Array β}, array.iter.toArray = array
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaEquivSigma_symm_apply : ∀ {α : Type u_2} (β : α → Type u_1) (a : (i : α) × β i), (Equiv.psigmaEquivSigma β).symm a = ⟨a.fst, a.snd⟩
-- Mathlib.MeasureTheory.PiSystem
piiUnionInter_mono_right : ∀ {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} {S T : Set ι}, S ⊆ T → piiUnionInter π S ⊆ piiUnionInter π T
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k a : α} {v : β k}, (m.insert k v).contains a = (k == a || m.contains a)
-- Init.Data.List.Zip
/-- See also `getElem?_zipWith'` for a variant
using `Option.map` and `Option.bind` rather than a `match`.
 -/
List.getElem?_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} {i : ℕ},
  (List.zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} (h' : a ∈ t), Std.DTreeMap.Raw.Const.get? t a = some (Std.DTreeMap.Raw.Const.get t a h')
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- When the domain is a real normed space, `ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm` can
be tightened to take the supremum over only the `Metric.sphere`.  -/
ContinuousLinearMap.sSup_sphere_eq_nnnorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F), sSup ((fun x => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊
-- Mathlib.Data.Num.Lemmas
PosNum.cast_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : PosNum), ↑(m * n) = ↑m * ↑n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_eq_head!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.minKey! = t.keys.head!
-- Mathlib.Topology.Connected.PathConnected
instCompactSpaceZerothHomotopy : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X], CompactSpace (ZerothHomotopy X)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion : @AlgebraicGeometry.IsSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.IsClosedImmersion
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The cosine of the angle between two vectors is 1 if and only if the angle is 0.  -/
InnerProductGeometry.cos_eq_one_iff_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  Real.cos (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = 0
-- Init.Data.List.Lex
List.instReflLeOfIrreflLt : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Refl fun x1 x2 => x1 ≤ x2
-- Lean.Language.Basic
/-- The messages produced by this step. The union of message logs of all finished snapshots is
reported to the user.  -/
Lean.Language.Snapshot.diagnostics : Lean.Language.Snapshot → Lean.Language.Snapshot.Diagnostics
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P → RingHom.StableUnderCompositionWithLocalizationAwayTarget P
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for the inf of two filters  -/
Filter.Realizer.inf : {α : Type u_1} → {f g : Filter α} → f.Realizer → g.Realizer → (f ⊓ g).Realizer
-- Lean.Util.Path
/-- Find the `.lean` source of a module in a `LEAN_SRC_PATH` search path.  -/
Lean.findLean : Lean.SearchPath → Lean.Name → IO System.FilePath
-- Init.Data.SInt.Lemmas
Int8.toISize_toInt32 : ∀ (n : Int8), n.toInt32.toISize = n.toISize
-- Qq.Simp
/-- A copy of `Meta.Simp.Result` with explicit types.  -/
Lean.Meta.Simp.ResultQ : {u : Lean.Level} → {α : Q(Sort u)} → Q(«$α») → Type
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.apply_mem_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X}, e.IsImage s t → x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)
-- Init.Data.Option.List
Option.mem_toList : ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ o.toList ↔ o = some a
-- Mathlib.Algebra.GroupWithZero.Hom
/-- The trivial homomorphism between monoids with zero, sending 0 to 0 and all other elements to 1.
 -/
MonoidWithZeroHom.one : (M₀ : Type u_7) →
  (N₀ : Type u_8) →
    [inst : MulZeroOneClass M₀] →
      [inst_1 : MulZeroOneClass N₀] →
        [DecidablePred fun x => x = 0] → [Nontrivial M₀] → [NoZeroDivisors M₀] → One (M₀ →*₀ N₀)
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_eq_sum_div_card : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] [inst_2 : Fintype ι] (f : ι → K),
  (Finset.univ.expect fun i => f i) = (∑ i, f i) / ↑(Fintype.card ι)
-- Init.Prelude
/-- Constructs a new empty array with initial capacity `0`.

Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.
 -/
Array.empty : {α : Type u} → Array α
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.span R 0 = ⊥
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The index of the root `α + β` where `α` is the short root and `β` is the long root.  -/
RootPairing.EmbeddedG2.shortAddLong : {ι : 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) → [P.EmbeddedG2] → ι
-- Mathlib.Analysis.Normed.Group.AddTorsor
LipschitzWith.vadd : ∀ {α : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : PseudoEMetricSpace α] {f : α → V} {g : α → P} {Kf Kg : NNReal},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) (f +ᵥ g)
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.FG.pow : ∀ {R : Type u_1} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided] {n : ℕ}, I.FG → (I ^ n).FG
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom h) = h
-- Aesop.Tree.Data
Aesop.MVarCluster.setGoals : Array Aesop.GoalRef → Aesop.MVarCluster → Aesop.MVarCluster