mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Basic
/-- A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie
module.  -/
LieModule.isNilpotent_toEnd_genWeightSpace_zero : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] (x : L),
  IsNilpotent ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M 0)) x)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_sub_scalar : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (μ : R), (M - (Matrix.scalar n) μ).charpoly = M.charpoly.comp (Polynomial.X + Polynomial.C μ)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
instModuleGradedTensorProduct : (R : Type u_1) →
  {ι : Type u_4} →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → Module R (GradedTensorProduct R 𝒜 ℬ)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `completedCosZeta` as a Dirichlet series in the convergence range
(second version, with sum over `ℕ`).  -/
HurwitzZeta.hasSum_nat_completedCosZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * Real.pi * a * ↑n)) / ↑n ^ s)
      (HurwitzZeta.completedCosZeta (↑a) s)
-- Mathlib.Combinatorics.Matroid.Dual
/-- A coindependent set of `M` is an independent set of the dual of `M✶`. we give it a separate
definition to enable dot notation. Which spelling is better depends on context.  -/
Matroid.Coindep : {α : Type u_1} → Matroid α → Set α → Prop
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₁ → (t₁ ∩ t₂)[k]! = default
-- Init.Data.Order.Classes
Std.IsPartialOrder.le_antisymm : ∀ {α : Type u} {inst : LE α} [self : Std.IsPartialOrder α] (a b : α), a ≤ b → b ≤ a → a = b
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  (x y : (j : J) × F.obj j),
  CategoryTheory.Limits.Types.FilteredColimit.Rel F x y → Relation.EqvGen F.ColimitTypeRel x y
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array ℕ),
  (f.performRupCheck rupHints).1.assignments.size = f.assignments.size
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.apply_eq_zero_of_isEmpty : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [IsEmpty α] (μ : MeasureTheory.VectorMeasure α M) (s : Set α), μ s = 0
-- Mathlib.NumberTheory.MulChar.Basic
/-- **Alias** of `MulChar.domRestrictHom_apply`. -/
MulChar.restrictHom_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {S : Type u_3} [inst_1 : SetLike S R] [inst_2 : SubmonoidClass S R] (T : S)
  (R'' : Type u_4) [inst_3 : CommMonoidWithZero R''] (χ : MulChar R R''),
  (MulChar.domRestrictHom T R'') χ = MulChar.domRestrict T χ
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.isPrime' : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α) [_H : I.IsMaximal], I.IsPrime
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.isIso_Q_map_iff_quasiIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CategoryTheory.IsIso (DerivedCategory.Q.map φ) ↔ QuasiIso φ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.divThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r408 : String
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.connected_induce_iff : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, (SimpleGraph.induce s G).Connected ↔ (⊤.induce s).Connected
-- Mathlib.RingTheory.FreeCommRing
/-- The free commutative ring on a type with one term is isomorphic to `ℤ[X]`.  -/
freeCommRingPUnitEquivPolynomialInt : FreeCommRing PUnit.{u + 1} ≃+* Polynomial ℤ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succ?_eq_of_technicalCondition : ∀ {n : ℕ} {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : LT α]
  [m : HasModel✝ α (BitVec n)] {x : α},
  (∀ (y : α),
      Std.PRange.succ? x = some y ↔
        ¬HasModel.encode✝ x + 1#n = BitVec.Signed.intMinSealed✝ n ∧ HasModel.encode✝ x + 1#n = HasModel.encode✝ y) →
    Std.PRange.succ? x = Std.PRange.succ? x
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k fallback : α}, k ∉ m → l.contains k = false → (m.insertMany l).getD k fallback = fallback
-- Mathlib.Analysis.Complex.Exponential
Real.sum_le_exp_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial ≤ Real.exp x
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanClientCapabilities.mk : Option Bool → Option Bool → Option Lean.Lsp.RpcWireFormat → Lean.Lsp.LeanClientCapabilities
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu.eq_1 : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α],
  IncidenceAlgebra.mu 𝕜 = { toFun := IncidenceAlgebra.muFun✝ 𝕜, eq_zero_of_not_le' := ⋯ }
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_nat_sub : ∀ {α : Type u} [inst : Lean.Grind.Ring α] {x y : ℕ}, x ≥ y → ↑↑(x - y) = ↑x - ↑y
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- A slightly more general version of `Set.smul_set_pi₀`.  -/
Set.smul_set_pi₀' : ∀ {M : Type u_3} {ι : Type u_4} {α : ι → Type u_5} [inst : GroupWithZero M] [inst_1 : (i : ι) → MulAction M (α i)]
  {c : M} {I : Set ι}, c ≠ 0 ∨ I = Set.univ → ∀ (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)
-- Lean.Parser.Basic
Lean.Parser.leadingParserAux : Lean.Name → Lean.Parser.PrattParsingTables → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserFn
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.dvd_eq_le : ∀ {M : Type u_1} [inst : CommMonoid M], (fun x1 x2 => x1 ∣ x2) = fun x1 x2 => x1 ≤ x2
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instNonemptySavedState : Nonempty Lean.Meta.Grind.SavedState
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.toAddGrpObj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {R : C} → [self : CategoryTheory.RingObj R] → CategoryTheory.AddGrpObj R
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.nonPrincipals_eq_empty_iff : ∀ {R : Type u} [inst : Semiring R], Ideal.nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If distinct points `p₂` and `p₃` lie in `s` but `p₁` does not, the three points are affinely
independent.  -/
affineIndependent_of_ne_of_notMem_of_mem_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
  p₂ ≠ p₃ → p₁ ∉ s → p₂ ∈ s → p₃ ∈ s → AffineIndependent k ![p₁, p₂, p₃]
-- Mathlib.Order.Sublattice
Sublattice.prod_mono_left : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L₁ L₂ : Sublattice α} {M : Sublattice β},
  L₁ ≤ L₂ → L₁.prod M ≤ L₂.prod M
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ),
  2 ≤ n →
    p.rightInv i x n =
      -(↑i.symm).compContinuousMultilinearMap
          (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
/-- [Stacks Tag 00FK](https://stacks.math.columbia.edu/tag/00FK) -/
Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ p ∈ minimalPrimes R, ∃ p', p'.IsPrime ∧ Ideal.comap f p' = p
-- Lean.Data.Json.Basic
Lean.Json.setObjVal! : Lean.Json → String → Lean.Json → Lean.Json
-- Init.Internal.Order.Basic
Lean.Order.chain_conj : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] (c P : α → Prop), Lean.Order.chain c → Lean.Order.chain fun x => c x ∧ P x
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κs : ι → ProbabilityTheory.Kernel α β} (I : Finset ι),
  (∀ i ∈ I, ProbabilityTheory.IsSFiniteKernel (κs i)) → ProbabilityTheory.IsSFiniteKernel (∑ i ∈ I, κs i)
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
/-- `PInfty` factors through the normalized Moore complex  -/
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      (X : CategoryTheory.SimplicialObject A) →
        AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.NormalizedMooreComplex.obj X
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C}
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] {a : M}
  (F : CategoryTheory.Functor C D) [inst_7 : F.CommShift M] [F.Additive], CategoryTheory.ShiftedHom.map 0 F = 0
-- Mathlib.Data.Sigma.Interval
Sigma.Iic_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)]
  (i : ι) (a : α i), Finset.Iic ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Iic a)
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall : ∀ (L : FirstOrder.Language) (M : Type w) [inst : Nonempty M] [inst_1 : L.Structure M],
  Small.{max u v, w} ↥⊥.elementarySkolem₁Reduct
-- Mathlib.Order.Atoms
isCoatomic_iff : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderTop α],
  IsCoatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
-- Init.Data.Int.DivMod.Lemmas
Int.zero_tdiv : ∀ (b : ℤ), Int.tdiv 0 b = 0
-- Std.Sync.Broadcast
/-- Unsubscribes a `Receiver` from the `Broadcast` channel.
 -/
Std.Broadcast.Receiver.unsubscribe : {α : Type} → Std.Broadcast.Receiver α → IO Unit
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_zero_right : ∀ (b : Ordinal.{u_1}), Ordinal.CNF.eval b 0 = 0
-- Lean.Environment
/-- Replays the difference between `newEnv` and `oldEnv` onto `dest`: the set of constants in `newEnv`
but not `oldEnv` and the environment extension state for extensions defining `replay?`. If
`skipExisting` is true, constants that are already in `dest` are not added. If `newEnv` and `dest`
are not derived from `oldEnv`, the result is undefined.
 -/
Lean.Environment.replayConsts : Lean.Environment → Lean.Environment → Lean.Environment → optParam Bool false → BaseIO Lean.Environment
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor.sizeOf_spec : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f) = 1 + sizeOf e + sizeOf f
-- ProofWidgets.Component.RefreshComponent
/-- If set, the `RefreshComponent` is no longer displayed in the UI.
The `RefreshToken` should be discarded, and any associated thread should exit.  -/
ProofWidgets.RefreshToken.cancelTk : ProofWidgets.RefreshToken → IO.CancelToken
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.collectConstsWithLevelMVars.go : Lean.Expr → StateRefT' IO.RealWorld (Std.HashSet Lean.Expr) Lean.CoreM Unit
-- Lean.Meta.WHNF
/-- Helper method for `reduceRec`.
We use it to ensure we don't expose `Nat.add` when reducing `Nat.rec`.
We we use the following trick, if `e` can be expressed as an offset `(a, k)` with `k > 0`,
we create a new expression `Nat.succ e'` where `e'` is `a` for `k = 1`, or `a + (k-1)` for `k > 1`.
See issue #3022
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.cleanupNatOffsetMajor : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Heyting.Basic
/-- `p → q → p`  -/
le_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ a
-- Mathlib.RingTheory.DedekindDomain.SInteger
/-- The group of `S`-units is the group of units of the ring of `S`-integers.  -/
Set.unitEquivUnitsInteger : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (S : Set (IsDedekindDomain.HeightOneSpectrum R)) →
        (K : Type v) →
          [inst_2 : Field K] → [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → ↥(S.unit K) ≃* (↥(S.integer K))ˣ
-- Init.Data.UInt.Basic
/-- Converts a `Fin USize.size` into the corresponding `USize`.  -/
USize.ofFin : Fin USize.size → USize
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_iSup_of_directed : ∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subfield K},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.comp_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (g : L.Embedding N P) (f : L.Embedding M N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Formula.equivSentence_inf : ∀ {L : FirstOrder.Language} {α : Type u'} (φ ψ : L.Formula α),
  FirstOrder.Language.Formula.equivSentence (φ ⊓ ψ) =
    FirstOrder.Language.Formula.equivSentence φ ⊓ FirstOrder.Language.Formula.equivSentence ψ
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.sInf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : Set (CategoryTheory.SubmonoidFunctor M)) (x : C), (sInf S).obj x = ⨅ F ∈ S, F.obj x
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- A `rw` suggestion section.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.rw : Mathlib.Tactic.ClickSuggestions.RwInfo →
  Array Mathlib.Tactic.ClickSuggestions.RwLemma → Mathlib.Tactic.ClickSuggestions.Candidates✝
-- Init.Data.SInt.Basic
instToStringISize : ToString ISize
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.rTensorBot_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (a : ↥A), A.rTensorBot.symm a = a ⊗ₜ[R] 1
-- Mathlib.RingTheory.HahnSeries.Cardinal
/-- The `κ`-bounded subring of Hahn series with less than `κ` terms.  -/
HahnSeries.cardSuppLTSubring : (Γ : Type u_1) →
  (R : Type u_2) →
    (κ : Cardinal.{u_1}) →
      [inst : PartialOrder Γ] →
        [inst_1 : AddCommMonoid Γ] →
          [inst_2 : IsOrderedCancelAddMonoid Γ] →
            [inst_3 : Ring R] → [hκ : Fact (Cardinal.aleph0 ≤ κ)] → Subring (HahnSeries Γ R)
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.to_fun_eq_coe : ∀ {μ : YoungDiagram} {T : SemistandardYoungTableau μ}, T.entry = ⇑T
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- `tprodCoeff R r f` with `r : R` and `f : Π i, s i` is the tensor product of the vectors `f i`
over all `i : ι`, multiplied by the coefficient `r`. Note that this is meant as an auxiliary
definition for this file alone, and that one should use `tprod` defined below for most purposes.  -/
PiTensorProduct.tprodCoeff : {ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → R → ((i : ι) → s i) → PiTensorProduct R fun i => s i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty =
        (t.isEmpty || decide (t.size = 1) && Std.DTreeMap.Internal.Impl.contains k t)
-- Mathlib.Data.Nat.PSub
Nat.sub_eq_psub : ∀ (m n : ℕ), m - n = (m.psub n).getD 0
-- Mathlib.Algebra.Group.Hom.Defs
/-- Make a `ZeroHom` inverse from the bijective inverse of a `ZeroHom`  -/
ZeroHom.inverse : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Zero M] → [inst_1 : Zero N] → (f : ZeroHom M N) → (g : N → M) → Function.LeftInverse g ⇑f → ZeroHom N M
-- Aesop.Forward.State
Aesop.instInhabitedForwardState : Inhabited Aesop.ForwardState
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail.aux.eq_2 : ∀ {α : Type u} (fst : α) (s : Stream'.WSeq α), Stream'.WSeq.tail.aux (some (fst, s)) = s.destruct
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitLeft_symm_of_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (g : G i) (m : M),
  (TensorProduct.directLimitLeft f M).symm
      ((Module.DirectLimit.of R ι (fun x => TensorProduct R (G x) M) (fun i j h => LinearMap.rTensor M (f i j h)) i)
        (g ⊗ₜ[R] m)) =
    (Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m
-- Std.Data.HashMap.Lemmas
Std.HashMap.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m[a]?.isSome = true ↔ a ∈ m
-- Mathlib.Combinatorics.Additive.Dissociation
mulDissociated_inv : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α}, MulDissociated s⁻¹ ↔ MulDissociated s
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.isClosed_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M), IsClosed ↑s.topologicalClosure
-- Mathlib.Topology.Order.Lattice
Continuous.finset_inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L},
  (∀ i ∈ s, Continuous (f i)) → Continuous (s.inf f)
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.Iso.mk_inv : ∀ {α β : GrpWithZero} (e : α.carrier ≃* β.carrier),
  (GrpWithZero.Iso.mk e).inv = GrpWithZero.ofHom (MonoidWithZeroHom.ofClass e.symm)
-- Mathlib.Data.Sym.Sym2
/-- Mapping an unordered pair off the diagonal to a finite set produces a finset of size `2`.  -/
Sym2.card_toFinset_of_not_isDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (z : Sym2 α), ¬z.IsDiag → z.toFinset.card = 2
-- Mathlib.Order.Monotone.Basic
strictAnti_int_of_succ_lt : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α}, (∀ (n : ℤ), f (n + 1) < f n) → StrictAnti f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.toArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.homMk_apply : ∀ {X Y : FintypeCat} (f : X.obj → Y.obj) (x : X.obj), (CategoryTheory.ConcreteCategory.hom (FintypeCat.homMk f)) x = f x
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.eq_bot_of_subsingleton : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  [Subsingleton ↥p], p = ⊥
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_eq_top_of_top_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : OrderTop α] {s : Set α}, ⊤ ∈ s → sSup s = ⊤
-- Mathlib.Data.List.Nodup
List.Nodup.filterMap : ∀ {α : Type u} {β : Type v} {l : List α} {f : α → Option β},
  (∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a') → l.Nodup → (List.filterMap f l).Nodup
-- Std.Http.Data.Headers.Name
/-- Standard Authorization header name
 -/
Std.Http.Header.Name.authorization : Std.Http.Header.Name
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff_substInv : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  PowerSeries.constantCoeff P.substInv = 0
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b) (t : ℝ), curveIntegralFun ω γ.symm t = -curveIntegralFun ω γ (1 - t)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.left.injEq : ∀ {J : CategoryTheory.Limits.MulticospanShape} (a a_1 : J.L),
  (CategoryTheory.Limits.WalkingMulticospan.left a = CategoryTheory.Limits.WalkingMulticospan.left a_1) = (a = a_1)
-- Init.Data.UInt.Lemmas
UInt16.ne_of_toBitVec_ne : ∀ {a b : UInt16}, a.toBitVec ≠ b.toBitVec → a ≠ b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.trivial_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C),
  (CategoryTheory.PreOneHypercover.trivial S).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?.eq_go : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (x : Option ((a : α) × β a))
  (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.getEntryLE? k t).or x = Std.DTreeMap.Internal.Impl.getEntryLE?.go k x t
-- Init.Data.Array.MinMax
Array.min_eq_min_toList : ∀ {α : Type u_1} [inst : Min α] {xs : Array α} {h : xs ≠ #[]}, xs.min h = xs.toList.min ⋯
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift D A]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C)
  (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (a b : A) (X : C),
  F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).hom.app X) =
    CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).inv.app X))
          ((i b).inv.app ((s a).obj X))))
-- Init.Core
Option.some.inj : ∀ {α : Type u} {val val_1 : α}, some val = some val_1 → val = val_1