mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_comp_includeLeftRingHom : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D),
  (↑(Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeLeftRingHom =
    Algebra.TensorProduct.includeLeftRingHom.comp ↑f
-- Batteries.Data.Char.Basic
Char.ofNatAux.hcongr_2 : ∀ (n n' : ℕ), n = n' → ∀ (h : n.isValidChar) (h' : n'.isValidChar), h ≍ h' → Char.ofNatAux n h ≍ Char.ofNatAux n' h'
-- Mathlib.Data.Multiset.UnionInter
Multiset.Nodup.inter_right : ∀ {α : Type u_1} {t : Multiset α} [inst : DecidableEq α] (s : Multiset α), t.Nodup → (s ∩ t).Nodup
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffWithinAt_extChartAt_symm_range_self : ∀ {𝕜 : 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] {n : WithTop ℕ∞} (x : M),
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A vector added to the second point lies in the affine span of two points if and only if it is
a multiple of their difference.  -/
vadd_right_mem_affineSpan_pair : ∀ {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₂ : P} {v : V}, v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_sliceFrom : ∀ {s : String} {p₀ p : s.Pos} {h : p₀ ≤ p}, String.Pos.ofSliceFrom (p₀.sliceFrom p h) = p
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.mul_add_cmod_le_iff : ∀ {a k b : ℤ}, k > 0 → (a * k + Int.Internal.Linear.cmod b k ≤ 0 ↔ a ≤ 0)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.push : Lean.Expr → Lean.Meta.FunIndInfo → Array Lean.Expr → Lean.Meta.FunInd.SeenCalls → Lean.MetaM Lean.Meta.FunInd.SeenCalls
-- Init.Data.Dyadic.Basic
Dyadic.pow_succ : ∀ (x : Dyadic) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
isLittleO_log_rpow_rpow_atTop : ∀ {s : ℝ} (r : ℝ), 0 < s → (fun x => Real.log x ^ r) =o[Filter.atTop] fun x => x ^ s
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.termF₀ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf_w : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf_w._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf_w._auto_3),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂)
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀
            n₁ n₂ hn₁' hn₁ hn₂).inv)
      ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).d pq' pq'') =
    0
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.zsmul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (n : ℤ), CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.forM_eq_forM_toList : ∀ {α : Type u} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst : Monad m']
  [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f ↑m = (Std.DHashMap.Raw.Const.toList ↑m).forM fun a => f a.1 a.2
-- Mathlib.Tactic.Tauto
/-- Report places where `tauto` can be replaced by `grind`.  -/
linter.tacticAnalysis.tautoToGrind : Lean.Option Bool
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instLinearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (WithZero α)
-- Mathlib.Data.Finset.Sups
Finset.powerset_infs_powerset_self : ∀ {α : Type u_2} [inst : DecidableEq α] (s : Finset α), s.powerset ⊼ s.powerset = s.powerset
-- Lean.DocString.Extension
Lean.docStringExt : Lean.MapDeclarationExtension String
-- Mathlib.Data.Set.SymmDiff
Set.symmDiff_union_subset : ∀ {α : Type u} {s t u : Set α}, symmDiff s (t ∪ u) ⊆ symmDiff s t ∪ symmDiff s u
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.ext : ∀ {T : Type u_1} {N : Type u_2} {x y : ContextFreeRule T N}, x.input = y.input → x.output = y.output → x = y
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`.  -/
mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' : ∀ {𝕜 : 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] [IsManifold I 1 M] {x y : M},
  y ∈ (extChartAt I x).source →
    mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y =
      ContinuousLinearMap.id 𝕜 (TangentSpace I y)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_add_eq_left_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.natDegree < p.natDegree → (p + q).natDegree = p.natDegree
-- Mathlib.Order.Lattice
/-- A `SemilatticeInf` is a meet-semilattice, that is, a partial order
with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation
`⊓` which is the greatest element smaller than both factors.  -/
SemilatticeInf : Type u → Type u
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_comap : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] [inst_7 : AddCommGroup V₃]
  [inst_8 : Module k V₃] [inst_9 : AddTorsor V₃ P₃] (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃),
  AffineSubspace.comap f (AffineSubspace.comap g s) = AffineSubspace.comap (g.comp f) s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation equals relation, defined as `x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x`.  -/
ValuativeRel.veq : {R : Type u_1} → [inst : Semiring R] → [ValuativeRel R] → R → R → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.cache : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {w : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.Return aig w) → Std.Tactic.BVDecide.BVExpr.Cache (↑self.result).aig
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instSMul : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {M₂ : Type w₂} →
      [inst : (i : ι) → AddCommMonoid (M₁ i)] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] →
            [inst_3 : TopologicalSpace M₂] →
              {R' : Type u_1} →
                {A : Type u_3} →
                  [inst_4 : Semiring A] →
                    [inst_5 : (i : ι) → Module A (M₁ i)] →
                      [inst_6 : Module A M₂] →
                        [inst_7 : DistribSMul R' M₂] →
                          [ContinuousConstSMul R' M₂] →
                            [SMulCommClass A R' M₂] → SMul R' (ContinuousMultilinearMap A M₁ M₂)
-- Init.Data.Iterators.Combinators.ULift
/-- Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
Std.Iterators.Types.ULiftIterator.modifyStep : {α β : Type u} → Std.IterStep (Std.Iter β) β → Std.IterStep (Std.Iter (ULift.{v, u} β)) (ULift.{v, u} β)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_sdiff : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet]
  [inst_2 : DecidableEq V], (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.getEntry?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (k : α) (v : β k)
  (l : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match ⟨k, v⟩ :: l with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_2 k v l
-- Lean.Declaration
Lean.ConstantInfo.axiomInfo.injEq : ∀ (val val_1 : Lean.AxiomVal), (Lean.ConstantInfo.axiomInfo val = Lean.ConstantInfo.axiomInfo val_1) = (val = val_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_of_projective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)], K.IsKProjective
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.uniqueDiffOn_preimage : ∀ {𝕜 : 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) {s : Set H},
  IsOpen s → UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ Set.range ↑I)
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.instBEqExprPtr : BEq Lean.Meta.Sym.ExprPtr
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_zero : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] [Nontrivial n],
  Matrix.adjugate 0 = 0
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α], Monotone WithTop.pred
-- Mathlib.Geometry.Euclidean.Incenter
/-- The existence of the excenter opposite a vertex (in two or more dimensions), expressed in
terms of `ExcenterExists`.  -/
Affine.Simplex.excenterExists_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.ExcenterExists {i}
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.coe_back : ∀ {M : Type u_1} [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] (x : X),
  CategoryTheory.ActionCategory.back ⟨(), x⟩ = x
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- This definition provides a convenient way to show that a multicofork is a colimit.  -/
CategoryTheory.Limits.Multicofork.IsColimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        (K : CategoryTheory.Limits.Multicofork I) →
          (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) →
            (∀ (E : CategoryTheory.Limits.Multicofork I) (i : J.R),
                CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i) →
              (∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt),
                  (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E) →
                CategoryTheory.Limits.IsColimit K
-- Mathlib.Probability.BrownianMotion.Basic
/-- A stochastic process `X` with independent increments and such that for all `t`, `X t`
has law `gaussianReal 0 t` is a pre-Brownian motion.  -/
ProbabilityTheory.HasIndepIncrements.isPreBrownianReal_of_hasLaw : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  (∀ (t : NNReal), ProbabilityTheory.HasLaw (X t) (ProbabilityTheory.gaussianReal 0 t) P) →
    ProbabilityTheory.HasIndepIncrements X P → ProbabilityTheory.IsPreBrownianReal X P
-- Lean.Parser.Types
/-- Set to the precedence of the preceding (not surrounding) parser by `runLongestMatchParser`
for the use of `checkLhsPrec` in trailing parsers.
Note that with chaining, the preceding parser can be another trailing parser:
in `1 * 2 + 3`, the preceding parser is '*' when '+' is executed.  -/
Lean.Parser.ParserState.lhsPrec : Lean.Parser.ParserState → ℕ
-- Mathlib.Algebra.DualQuaternion
Quaternion.imI_snd_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.snd q.imI
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction is right adjoint to pushforward.  -/
AlgebraicGeometry.Scheme.Modules.restrictAdjunction : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      AlgebraicGeometry.Scheme.Modules.restrictFunctor f ⊣ AlgebraicGeometry.Scheme.Modules.pushforward f
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
PrimeSpectrum.toPiLocalization.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R],
  PrimeSpectrum.toPiLocalization R = Algebra.ofId R (PrimeSpectrum.PiLocalization R)
-- Mathlib.Algebra.MvPolynomial.Comap
/-- Given an algebra hom `f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R`
and a variable evaluation `v : τ → R`,
`comap f v` produces a variable evaluation `σ → R`.
 -/
MvPolynomial.comap : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_4} → [inst : CommSemiring R] → (MvPolynomial σ R →ₐ[R] MvPolynomial τ R) → (τ → R) → σ → R
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftEq R l l' h).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piEquivSucc.congr_simp : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι] [inst_1 : SuccOrder ι]
  (equiv equiv_1 : (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j),
  equiv = equiv_1 →
    ∀ (e e_1 : F (Order.succ i) ≃ F i × X i),
      e = e_1 →
        ∀ (hi : ¬IsMax i) (j : ↑(Set.Iic (Order.succ i))),
          InverseSystem.piEquivSucc equiv e hi j = InverseSystem.piEquivSucc equiv_1 e_1 hi j
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.liftRingHom.eq_1 : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m),
  AdicCompletion.liftRingHom I f hf =
    { toFun := fun x => ⟨fun n => (Submodule.factor ⋯) ((f n) x), ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ }
-- Init.Data.List.Basic
/-- Returns `true` if `l₁` and `l₂` are permutations of each other. `O(|l₁| * |l₂|)`.

The relation `List.Perm` is a logical characterization of permutations. When the `BEq α` instance
corresponds to `DecidableEq α`, `isPerm l₁ l₂ ↔ l₁ ~ l₂` (use the theorem `isPerm_iff`).
 -/
List.isPerm : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_pred_of_lt : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : p < i), p.succAbove (i.pred ⋯) = i
-- Mathlib.Algebra.Notation.Defs
/-- The notation typeclass for heterogeneous additive actions.
This enables the notation `a +ᵥ b : γ` where `a : α`, `b : β`.
 -/
HVAdd : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Data.List.Rotate
List.zipWith_rotate_one : ∀ {α : Type u} {β : Type u_1} (f : α → α → β) (x y : α) (l : List α),
  List.zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: List.zipWith f (y :: l) (l ++ [x])
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_list_iff : ∀ {l l' : List String.Slice}, (l == l') = true ↔ List.map String.Slice.copy l = List.map String.Slice.copy l'
-- Mathlib.Data.Tree.Basic
_private.Mathlib.Data.Tree.Basic.0.BinaryTree.traverse.match_1.eq_2 : ∀ {α : Type u_1} (motive : BinaryTree α → Sort u_2) (a : α) (l r : BinaryTree α) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (a : α) → (l r : BinaryTree α) → motive (BinaryTree.node a l r)),
  (match BinaryTree.node a l r with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node a l r => h_2 a l r) =
    h_2 a l r
-- Lean.Meta.Eqns
/-- Returns `some declName` if `thmName` is an equational theorem for `declName`.
 -/
Lean.Meta.isEqnThm? : Lean.Name → Lean.CoreM (Option Lean.Name)
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.adjunction_unit : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P],
  (CompHausLike.LocallyConstant.adjunction P hs).unit = CompHausLike.LocallyConstant.unit P hs
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.natIsoLift_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D}
  (τ : (CategoryTheory.Quotient.functor r).comp F ≅ (CategoryTheory.Quotient.functor r).comp G),
  (CategoryTheory.Quotient.natIsoLift r τ).inv = CategoryTheory.Quotient.natTransLift r τ.inv
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- `x.fst : R` is invertible when `x : tzre R M` is.  -/
TrivSqZeroExt.invertibleFstOfInvertible : {R : Type u} →
  {M : Type v} →
    [inst : AddCommGroup M] →
      [inst_1 : Semiring R] →
        [inst_2 : Module Rᵐᵒᵖ M] → [inst_3 : Module R M] → (x : TrivSqZeroExt R M) → [Invertible x] → Invertible x.fst
-- Mathlib.Data.Erased
Erased.map_out : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} (a : Erased α), (Erased.map f a).out = f a.out
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_add_mod_mul : ∀ {w x : Ordinal.{u_4}}, w < x → ∀ (y z : Ordinal.{u_4}), (x * y + w) % (x * z) = x * (y % z) + w
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBoundP?.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (t : RBTree.RBSet α cmp) (cut : α → Ordering),
  t.upperBoundP? cut = RBTree.RBNode.upperBound? cut ↑t
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_add_right : ∀ (m n k : ℕ), m.gcd (m * k + n) = m.gcd n
-- Mathlib.Algebra.Notation.Defs
ite_sub : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a b c : α),
  (if P then a else b) - c = if P then a - c else b - c
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_zero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N], AdicCompletion.map I 0 = 0
-- Mathlib.Geometry.Manifold.Bordism
/-- The manifold `M` is a charted space over `H`.  -/
SingularManifold.chartedSpace : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} → (self : SingularManifold X k I) → ChartedSpace H self.M
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace.mk.sizeOf_spec : ∀ (expandedCoeDecls : List Lean.Name), sizeOf { expandedCoeDecls := expandedCoeDecls } = 1 + sizeOf expandedCoeDecls
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.brecOn.eq : ∀ {motive_1 : Lean.Meta.Match.Pattern → Sort u} {motive_2 : List Lean.Meta.Match.Pattern → Sort u}
  (t : Lean.Meta.Match.Pattern) (F_1 : (t : Lean.Meta.Match.Pattern) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Meta.Match.Pattern) → Lean.Meta.Match.Pattern.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Match.Pattern.brecOn.go t F_1 F_2).2
-- Mathlib.Combinatorics.Additive.Corner.Defs
isCornerFree_singleton : ∀ {G : Type u_1} [inst : AddCommMonoid G] (x : G × G), IsCornerFree {x}
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.bsize.match_1.eq_1 : ∀ (motive : Substring.Raw → Sort u_1) (str : String) (b e : String.Pos.Raw)
  (h_1 : (str : String) → (b e : String.Pos.Raw) → motive { str := str, startPos := b, stopPos := e }),
  (match { str := str, startPos := b, stopPos := e } with
    | { str := str, startPos := b, stopPos := e } => h_1 str b e) =
    h_1 str b e
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_toSubmonoid : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ), S.unop.toSubmonoid = S.unop
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sUnion₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable →
    S.Pairwise (MeasureTheory.AEDisjoint μ) →
      (∀ s ∈ S, MeasureTheory.NullMeasurableSet s μ) → μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.zero_mul_nonneg : ∀ {α : Type u_2} [inst : MulZeroClass α] {g : Filter α}, g.NeBot → 0 ≤ 0 * g
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.maskToThms : Array Lean.Meta.Grind.EMatchTheorem → Array Bool → Array Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.add_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv) (i : ℕ), ↑(f + g) i = ↑f i + ↑g i
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The natural transformation from the composition of restriction and extension of scalars to the
identity functor on `S`-module.
 -/
ModuleCat.ExtendRestrictScalarsAdj.counit : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          (ModuleCat.restrictScalars f).comp (ModuleCat.extendScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat S)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.instInhabited : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.Substructure M)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.eq_orderOf : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → k = orderOf ζ
-- Std.Http.Data.Body.Stream
/-- Iterates over chunks until the channel closes.
 -/
Std.Http.Body.Stream.forIn : {β : Type} → Std.Http.Body.Stream → β → (Std.Http.Chunk → β → Std.Async.Async (ForInStep β)) → Std.Async.Async β