mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Basic
/-- Divisibility of integers. `a ∣ b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
 -/
Int.instDvd : Dvd ℤ
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`.  -/
IntermediateField.bot_eq_top_of_rank_adjoin_eq_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  (∀ (x : E), Module.rank F ↥F⟮x⟯ = 1) → ⊥ = ⊤
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (p : MvPolynomial (Option S₁) R),
  ∀ i ≤ p.totalDegree, (((MvPolynomial.optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree
-- Aesop.Stats.Basic
Aesop.Stats.goalStats : Aesop.Stats → Array Aesop.GoalStats
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.mk : Lean.Expr →
  Array Lean.Expr →
    Lean.MVarId →
      Array Lean.Elab.Tactic.ElimApp.Alt → Array Lean.MVarId → Array Lean.Expr → Lean.Elab.Tactic.ElimApp.Result
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_zero_eq_single_zero : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (y : M), Finsupp.cons y 0 = fun₀ | 0 => y
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The sigma type associated to a family of compactly generated spaces is compactly generated.  -/
instUCompactlyGeneratedSpaceSigma : ∀ {ι : Type v} {X : ι → Type w} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), UCompactlyGeneratedSpace (X i)],
  UCompactlyGeneratedSpace ((i : ι) × X i)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- `rpowIntegrand₀₁ p t` is operator concave for all `p ∈ Ioo 0 1` and all `0 < t`.  -/
CFC.concaveOn_cfcₙ_rpowIntegrand₀₁ : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p t : ℝ},
  p ∈ Set.Ioo 0 1 → 0 < t → ConcaveOn ℝ (Set.Ici 0) (cfcₙ (p.rpowIntegrand₀₁ t))
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instContinuousMul : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜], ContinuousMul ↑(Metric.ball 0 1)
-- Mathlib.Probability.Independence.Basic
/-- If `f` is a family of mutually independent random variables (`iIndepFun m f μ`) and `S, T` are
two disjoint finite index sets, then the tuple formed by `f i` for `i ∈ S` is independent of the
tuple `(f i)_i` for `i ∈ T`.  -/
ProbabilityTheory.iIndepFun.indepFun_finset : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
  Disjoint S T →
    ProbabilityTheory.iIndepFun f μ →
      (∀ (i : ι), Measurable (f i)) → ProbabilityTheory.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- The connecting homomorphism in the Jacobi-Zariski sequence.  -/
Algebra.H1Cotangent.δ : (R : Type u₁) →
  (S : Type u₂) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u₃) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] → [IsScalarTower R S T] → Algebra.H1Cotangent S T →ₗ[T] TensorProduct S T Ω[S⁄R]
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.CompatibleSMul.smul_tmul : ∀ {R : Type u_1} {R' : Type u_4} {inst : CommSemiring R} {inst_1 : Monoid R'} {M : Type u_7} {N : Type u_8}
  {inst_2 : AddCommMonoid M} {inst_3 : AddCommMonoid N} {inst_4 : DistribMulAction R' M} {inst_5 : Module R M}
  {inst_6 : Module R N} {inst_7 : DistribMulAction R' N} [self : TensorProduct.CompatibleSMul R R' M N] (r : R') (m : M)
  (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_var : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w idx : ℕ},
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var idx) = BitVec.truncate w (assign.get idx).bv
-- Init.Data.SInt.Lemmas
ISize.add_eq_right : ∀ {a b : ISize}, a + b = b ↔ a = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l l_1 : List ((a : α) × β a)),
  l = l_1 →
    ∀ (fallback fallback_1 : β a),
      fallback = fallback_1 →
        Std.Internal.List.getValueCastD a l fallback = Std.Internal.List.getValueCastD a l_1 fallback_1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_iff_right_of_lt_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀],
  0 < a → a < 1 → (a ^ m ≤ a ^ n ↔ n ≤ m)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_neg_one : ∀ (x : ℝ), x ^ (-1) = x⁻¹
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsMatch.matches_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {endPos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat endPos →
    String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceTo endPos).copy
-- Mathlib.Data.List.Basic
List.idxOf_eq_zero_iff_eq_nil_or_head_eq : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} (a : α), List.idxOf a l = 0 ↔ l = [] ∨ l.head? = some a
-- Init.Omega.Constraint
Lean.Omega.Constraint.sat'.eq_1 : ∀ (c : Lean.Omega.Constraint) (x y : Lean.Omega.Coeffs), c.sat' x y = c.sat (x.dot y)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts** (vector-valued). Special case of
`intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a derivative also at the endpoints.  -/
intervalIntegral.integral_smul_deriv_eq_deriv_smul : ∀ {a b : ℝ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [CompleteSpace E]
  [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x
-- Std.Data.ExtDTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtDTreeMap.insertMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        {ρ : Type u_1} → [ForIn Id ρ ((a : α) × β a)] → Std.ExtDTreeMap α β cmp → ρ → Std.ExtDTreeMap α β cmp
-- Std.Do.WP.Basic
Std.Do.WP.mk : {m : Type u → Type v} → {ps : outParam Std.Do.PostShape} → ({α : Type u} → m α → Std.Do.PredTrans ps α) → Std.Do.WP m ps
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
/-- The braiding on the localized category as a natural isomorphism of bifunctors.  -/
CategoryTheory.Localization.Monoidal.braidingNatIso : {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) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      [CategoryTheory.BraidedCategory C] →
                        CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε ≅
                          (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε).flip
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.support_bypass_sublist_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.support.Sublist p.support
-- Mathlib.Algebra.Order.Ring.Rat
Rat.instIsOrderedAddMonoid : IsOrderedAddMonoid ℚ
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Algebra.IsIntegral.algebraicIndependent_iff : ∀ {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsIntegral R S], AlgebraicIndependent R x ↔ AlgebraicIndependent S x
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g)
  (a : TensorProduct S T P.toExtension.Cotangent),
  (Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm (a, 0) =
    (LinearMap.liftBaseChange T
        (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom))
      a
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The composition of a polynomial function with a binary polynomial function is polynomial.  -/
WittVector.IsPoly.comp₂ : ∀ {p : ℕ} {g : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R}
  {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R} [hg : WittVector.IsPoly p g]
  [hf : WittVector.IsPoly₂ p f], WittVector.IsPoly₂ p fun x _Rcr x_1 y => g (f x_1 y)
-- Mathlib.Data.Matrix.DMatrix
DMatrix.sub_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → Sub (α i j)] (M N : DMatrix m n α)
  (i : m) (j : n), (M - N) i j = M i j - N i j
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_smul : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul S R] [inst_1 : SMul S A] (s : S) (x : Unitization R A),
  (s • x).toProd.2 = s • x.toProd.2
-- Mathlib.RingTheory.Algebraic.Integral
integralClosure_le_algebraicClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R],
  integralClosure R S ≤ Subalgebra.algebraicClosure R S
-- Batteries.Data.String.Lemmas
String.map_eq : ∀ (f : Char → Char) (s : String), String.Legacy.map f s = String.ofList (List.map f s.toList)
-- Mathlib.Probability.Distributions.Uniform
PMF.support_ofMultiset : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0), (PMF.ofMultiset s hs).support = ↑s.toFinset
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.intervalIntegral_tendsto_integral : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ι → ℝ} {f : ℝ → E},
  MeasureTheory.Integrable f μ →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto b l Filter.atTop →
        Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (nhds (∫ (x : ℝ), f x ∂μ))
-- Mathlib.Topology.Constructions
pi_eq_generateFrom : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)],
  Pi.topologicalSpace = TopologicalSpace.generateFrom {g | ∃ s i, (∀ a ∈ i, IsOpen (s a)) ∧ g = (↑i).pi s}
-- Mathlib.Data.Nat.Totient
/-- Euler's product formula for the totient function.  -/
Nat.totient_eq_prod_factorization : ∀ {n : ℕ}, n ≠ 0 → n.totient = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The simplified form of transitivity used within `IsOrdinal` yields an equivalent definition to
the standard one.  -/
ZFSet.isOrdinal_iff_isTrans : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_nonneg : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), 0 ≤ ‖f‖
-- Init.Data.Vector.Basic
/-- Swaps an element of a vector with a given value using a `Nat` index. Panics if the index is out of
bounds. The original value is returned along with the updated vector.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.swapAt! : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → α → α × Vector α n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Batteries.Data.String.Legacy
/-- Checks whether there is a character in a string for which the Boolean predicate `p` returns `true`.

Short-circuits at the first character for which `p` returns `true`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
 * `"brown".any (·.isLetter) = true`
 * `"brown".any (·.isWhitespace) = false`
 * `"brown and orange".any (·.isLetter) = true`
 * `"".any (fun _ => false) = false`
 -/
String.Legacy.any : String → (Char → Bool) → Bool
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.getElem_buildTable : ∀ {pat : String.Slice} {i : ℕ} {hi : i < pat.utf8ByteSize},
  (String.Slice.Pattern.ForwardSliceSearcher.buildTable pat)[i] =
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat.copy.toByteArray i ⋯
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0_of_finite : ∀ (α : Type u) [Finite α], Cardinal.mk α < Cardinal.aleph0
-- Init.Data.Array.Lemmas
Array.reverse_eq_push_iff : ∀ {α : Type u_1} {xs ys : Array α} {a : α}, xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), Set.uIoc a b = Set.uIoc b a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.mk : Lean.LocalContext → Lean.Expr → ℕ → ℕ → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.SplitDiagInfo
-- Mathlib.Data.List.Iterate
Nat.iterate.eq_1 : ∀ {α : Sort u} (op : α → α) (x : α), op^[0] x = x
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.add_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), a + a = 0
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.degrees_indicator : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Fintype σ] [inst_2 : CommRing K] (c : σ → K),
  (MvPolynomial.indicator c).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent_coe : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s),
  ⇑(SmoothBumpCovering.embeddingPiTangent✝ f) = fun x i => (↑(f.toFun i) x • ↑(extChartAt I (f.c i)) x, ↑(f.toFun i) x)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract_base : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.fract✝ hs (IsProperLinearSet.base✝ hs) = IsProperLinearSet.base✝ hs
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
column positive has nonzero determinant.  -/
Matrix.det_ne_zero_of_sum_col_pos : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
  (Pairwise fun i j => A i j < 0) → (∀ (j : n), 0 < ∑ i, A i j) → A.det ≠ 0
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m ≤ m0),
  (μ.trim hm).toOuterMeasure = μ.trim
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_symm_cancel_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ →ₛₗ[σ₃₂] M₂), ↑e ∘ₛₗ ↑e.symm ∘ₛₗ f = f
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.tensorEquiv_single_tmul_single : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R),
  (MonoidAlgebra.tensorEquiv R) (MonoidAlgebra.single m r₁ ⊗ₜ[R] MonoidAlgebra.single n r₂) =
    MonoidAlgebra.single (m, n) (r₁ * r₂)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_sqrtd : ∀ {d : ℤ}, Zsqrtd.sqrtd.re = 0
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- The image of the `GoodProducts` in `C` is equivalent to the union of `smaller C o'` over all
ordinals `o' < o`.
 -/
Profinite.NobelingProof.GoodProducts.range_equiv : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          Order.IsSuccLimit o →
            Profinite.NobelingProof.contained C o →
              ↑(Profinite.NobelingProof.GoodProducts.range C) ≃
                ↑(⋃ e, Profinite.NobelingProof.GoodProducts.smaller C ↑e)
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- The Lebesgue measure associated to a basis, giving measure `1` to the parallelepiped spanned
by the basis.  -/
Module.Basis.addHaar : {ι : Type u_5} →
  {E : Type u_6} →
    [Fintype ι] →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : MeasurableSpace E] → [BorelSpace E] → Module.Basis ι ℝ E → MeasureTheory.Measure E
-- Mathlib.Logic.Small.Set
small_univ_iff : ∀ {α : Type u1}, Small.{u, u1} ↑Set.univ ↔ Small.{u, u1} α
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Notation for identities up to unitors and associators.  -/
CategoryTheory.MonoidalCategory.«term⊗𝟙» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.Preorder
/-- The equivalence between `X →o Y` and the type of functors `X ⥤ Y` between preorder categories
`X` and `Y`.  -/
OrderHom.equivFunctor : {X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → (X →o Y) ≃ CategoryTheory.Functor X Y
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly.eq_2 : cosPoly✝ 1 = (Polynomial.monomial 1) (-4)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instOne.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β],
  OrderMonoidHom.instOne =
    {
      one :=
        let __src := 1;
        { toMonoidHom := __src, monotone' := ⋯ } }
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.left_triangle_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (e : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.leftZigzag e.unit.hom e.counit.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor e.hom).hom
      (CategoryTheory.Bicategory.rightUnitor e.hom).inv
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_one : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  (TensorProduct.AlgebraTensorModule.rTensor R N) 1 = 1
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates small colimits if it creates colimits of shape `J` for any small `J`.  -/
CategoryTheory.CreatesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.exists_pos_sum_of_countable : ∀ {ε : ENNReal}, ε ≠ 0 → ∀ (ι : Type u_4) [Countable ι], ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
-- Mathlib.Data.Nat.Cast.Defs
Nat.binCast.eq_def : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Add R] (x : ℕ),
  x.binCast =
    match x with
    | 0 => 0
    | n.succ =>
      if (n + 1) % 2 = 0 then ((n + 1) / 2).binCast + ((n + 1) / 2).binCast
      else ((n + 1) / 2).binCast + ((n + 1) / 2).binCast + 1
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_le_dotProduct_of_nonneg_left : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : Fintype n]
  {u v w : n → R}, u ≤ v → 0 ≤ w → w ⬝ᵥ u ≤ w ⬝ᵥ v
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioi_of_strictMonoOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) →
    StrictMonoOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atTop → f '' Set.Ioi a = Set.Ioi (f a)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Elements of `HeckeCosetModule Δ H₁ H₂ Z` are functions `HeckeCoset Δ H₁ H₂ → Z` (finitely
supported).  -/
HeckeCosetModule.instFunLikeHeckeCoset : {G : Type u_1} →
  [inst : Group G] →
    (Δ : Submonoid G) →
      (H₁ H₂ : Subgroup G) →
        (Z : Type u_2) → [inst_1 : Zero Z] → FunLike (HeckeCosetModule Δ H₁ H₂ Z) (HeckeCoset Δ H₁ H₂) Z
-- Mathlib.Algebra.GroupWithZero.Action.Defs
SMulWithZero.mk : {M₀ : Type u_2} →
  {A : Type u_7} →
    [inst : Zero M₀] →
      [inst_1 : Zero A] → [toSMulZeroClass : SMulZeroClass M₀ A] → (∀ (m : A), 0 • m = 0) → SMulWithZero M₀ A
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_forward_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv
      (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).inv Z))