mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices
in `s` not satisfying `pred` are zero.  -/
Finset.affineCombination_filter_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop}
  [inst_3 : DecidablePred pred],
  (∀ i ∈ s, w i ≠ 0 → pred i) → (Finset.affineCombination k ({x ∈ s | pred x}) p) w = (Finset.affineCombination k s p) w
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_of_beq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [inst : BEq β] {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [Std.LawfulEqOrd α] [LawfulBEq β],
  m₁.WF → m₂.WF → Std.DTreeMap.Internal.Impl.Const.beq m₁ m₂ = true → m₁.Equiv m₂
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter : String → Bool → Lean.PrettyPrinter.Formatter
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Mathlib.Order.Basic
LT.lt.false : ∀ {α : Type u_2} [inst : Preorder α] {a : α}, a < a → False
-- Mathlib.Algebra.Lie.Submodule
LieModuleEquiv.ofTop_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] (M : Type u_1) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (x : ↥⊤), (LieModuleEquiv.ofTop R L M) x = ↑x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_smulRight : ∀ {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂),
  ↑(f.smulRight z) = (↑f).smulRight z
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- `@[simp]`-normal form of `locallyRingedSpaceAdjunction_counit_app'`.  -/
AlgebraicGeometry.ΓSpec.toSpecΓ_of : ∀ (R : Type u) [inst : CommRing R],
  AlgebraicGeometry.toSpecΓ (CommRingCat.of R) =
    CommRingCat.ofHom
      (algebraMap R
        ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))
                ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj
          (Opposite.op ⊤)))
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f : ℕ → M` has product `m`, then the partial products `∏ i ∈ range n, f i` converge
to `m`.  -/
HasProd.tendsto_prod_nat : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℕ → M},
  HasProd f m → Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds m)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_union_eq_left : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (∀ a ∈ s₂, a ∉ s₁ → f a = 0) → ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₁, f a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.oneLePart : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Group β] [inst_2 : Lattice β] [ContinuousSup β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x)⁺ᵐ) μ
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
LinearMap.span_singleton_sup_orthogonal_eq_top : ∀ {K : Type u_7} {V : Type u_9} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {B : V →ₗ[K] V →ₗ[K] K}
  {x : V}, (B x) x ≠ 0 → K ∙ x ⊔ Submodule.orthogonalBilin B (K ∙ x) = ⊤
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f], CategoryTheory.Limits.HasPullback g f
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechNerve_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom],
  f.augmentedCechNerve.left = f.cechNerve
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec'.match_1.eq_3 : ∀ {M : Type u_2} (motive : ℕ → M → Sort u_1) (k : ℕ) (m : M) (h_1 : (x : M) → motive 0 x) (h_2 : (m : M) → motive 1 m)
  (h_3 : (k : ℕ) → (m : M) → motive k.succ.succ m),
  (match k.succ.succ, m with
    | 0, x => h_1 x
    | 1, m => h_2 m
    | k.succ.succ, m => h_3 k m) =
    h_3 k m
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff = 0 ↔ p.degree = ⊥
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_sSup : ∀ {X : AlgebraicGeometry.Scheme} (I : Set X.IdealSheafData), (sSup I).support = ⨅ i ∈ I, i.support
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Given a pushout square assembled from a pushout square on the top and
a commuting square on the bottom, the bottom square is a pushout square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPushout.of_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂)
      h₃₁ →
    CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁ →
      CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ → CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁
-- Init.Meta.Defs
Lean.Syntax.instCoeOutTSyntaxArrayArray : {k : Lean.SyntaxNodeKinds} → CoeOut (Lean.TSyntaxArray k) (Array Lean.Syntax)
-- Mathlib.Order.SupClosed
LinearOrder.supClosed : ∀ {α : Type u_3} [inst : LinearOrder α] (s : Set α), SupClosed s
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instHasTwoOutOfThreePropertyQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C], (CochainComplex.Plus.quasiIso C).HasTwoOutOfThreeProperty
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.ext_iff : ∀ {x y : Std.Time.WallTime}, x = y ↔ x.val = y.val
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instTopologicalSpaceM : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} → {s : SingularManifold X k I} → TopologicalSpace s.M
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_smul : ∀ {G : Type u_1} {H : Type u_2} {K : Type u_3} [inst : Add G] [inst_1 : AddZeroClass H] {a : G} {b : H}
  [inst_2 : DistribSMul K H] (c : K) (f : AddConstMap G H a b), ⇑(AddConstMap.smul c f) = c • ⇑f
-- Mathlib.Topology.CompactOpen
ContinuousMap.tendsto_nhds_compactOpen : ∀ {α : Type u_1} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {l : Filter α}
  {f : α → C(Y, Z)} {g : C(Y, Z)},
  Filter.Tendsto f l (nhds g) ↔
    ∀ (K : Set Y),
      IsCompact K → ∀ (U : Set Z), IsOpen U → Set.MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, Set.MapsTo (⇑(f a)) K U
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.shift.eq_1 : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : AddMonoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (v h : G),
  p.shift v h =
    if hmem : h ∈ Finset.image (fun x => v + x) p.support then
      have ex := ⋯;
      p.config (Classical.choose ex)
    else default
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Preorder β] {f g : α →ₘ[μ] β}, ↑f ≤ᵐ[μ] ↑g ↔ f ≤ g
-- Batteries.Data.List.Basic
List.all₂.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Bool) (a : α) (as : List α) (b : β) (bs : List β),
  List.all₂ r (a :: as) (b :: bs) = if r a b = true then List.all₂ r as bs else false
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `π` is the "quotient map" of the relation  -/
CategoryTheory.EffectiveEquivalenceRelation.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} → {p₁ p₂ : R ⟶ A} → (self : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂) → A ⟶ self.B
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- The principal ideals of `R` form a submonoid of `Ideal R`.  -/
Ideal.isPrincipalSubmonoid : (R : Type u_1) → [inst : CommRing R] → Submonoid (Ideal R)
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.instInhabitedAliasInfo : Inhabited Batteries.Tactic.Alias.AliasInfo
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleGroup.mk : ∀ {G : Type u_1} [inst : Group G] [toNontrivial : Nontrivial G],
  (∀ (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤) → IsSimpleGroup G
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.Core.toCore : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : Norm E], NormedSpace.Core 𝕜 E → SeminormedSpace.Core 𝕜 E
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) [inst_2 : S.HasLeftHomology] (x : A ⟶ S.X₁)
  (hx : k = CategoryTheory.CategoryStruct.comp x S.f) {Z : C} (h : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k ⋯) (CategoryTheory.CategoryStruct.comp S.leftHomologyπ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.PNat.Prime
PNat.Coprime.factor_eq_gcd_left : ∀ {a b m n : ℕ+}, m.Coprime n → a ∣ m → b ∣ n → a = (a * b).gcd m
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.isSubDPIdeal_iInf : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {ι : Type u_3} {J : ι → Ideal A},
  (∀ (i : ι), hI.IsSubDPIdeal (J i)) → hI.IsSubDPIdeal (I ⊓ ⨅ i, J i)
-- Mathlib.Topology.Category.CompactlyGenerated
/-- The equivalence between isomorphisms in `CompactlyGenerated` and homeomorphisms
of topological spaces.  -/
CompactlyGenerated.isoEquivHomeo : {X Y : CompactlyGenerated} → (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)
-- Std.Data.ByteSlice
/-- Returns a byte slice of a byte array, with the given bounds.

If `start` or `stop` are not valid bounds for a byte slice, then they are clamped to byte array's size.
Additionally, the starting index is clamped to the ending index.
 -/
ByteArray.toByteSlice : (as : ByteArray) → optParam ℕ 0 → optParam ℕ as.size → ByteSlice
-- Mathlib.CategoryTheory.Abelian.Basic
/-- If the coimage-image comparison morphism for a morphism `f` is an isomorphism,
we obtain an image factorisation of `f`.  -/
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          {X Y : C} →
            (f : X ⟶ Y) →
              [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] →
                CategoryTheory.Limits.ImageFactorisation f
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivAt.congr_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' g' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → f' = g' → HasFDerivAt f g' x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸}, DifferentiableWithinAt 𝕜 a s x → ∀ (b : 𝔸), DifferentiableWithinAt 𝕜 (fun y => a y * b) s x
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- The null homotopic maps `Hσ` are compatible with the application of additive functors.  -/
AlgebraicTopology.DoldKan.map_Hσ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (G : CategoryTheory.Functor C D) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ),
  (AlgebraicTopology.DoldKan.Hσ q).f n = G.map ((AlgebraicTopology.DoldKan.Hσ q).f n)
-- Init.Data.List.Erase
List.erase_sublist : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, (l.erase a).Sublist l
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.getCode : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Alt pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.instNonemptySubtypeSetIsBase : ∀ {α : Type u_1} (M : Matroid α), Nonempty { B // M.IsBase B }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Raw.Const.get t x ⋯)).get!
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.add : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] {s t : Finset α},
  s.Nontrivial → t.Nontrivial → (s + t).Nontrivial
-- Mathlib.Analysis.SpecificLimits.Basic
factorial_tendsto_atTop : Filter.Tendsto Nat.factorial Filter.atTop Filter.atTop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isSome = !t.isEmpty
-- Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
AlgebraicGeometry.instDescendsAlongSchemeFormallyUnramifiedMinMorphismPropertySurjectiveFlatQuasiCompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.FormallyUnramified)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.LinearAlgebra.Basis.Cardinality
/-- Over any ring `R`, if `b` is a basis for a module `M`,
and `s` is a maximal linearly independent set,
then the union of the supports of `x ∈ s` (when written out in the basis `b`) is all of `b`.
 -/
union_support_maximal_linearIndependent_eq_range_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [Nontrivial R] [inst_3 : Module R M]
  {ι : Type w} (b : Module.Basis ι R M) {κ : Type w'} (v : κ → M) (ind : LinearIndependent R v),
  ind.Maximal → ⋃ k, ↑(b.repr (v k)).support = Set.univ
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.interior_setOfPred_im_le`. -/
Complex.interior_setOf_im_le : ∀ (a : ℝ), interior {z | z.im ≤ a} = {z | z.im < a}
-- Mathlib.Algebra.Group.Units.Equiv
toAddUnits_val_apply : ∀ {G : Type u_6} [inst : AddGroup G] (x : AddUnits G), toAddUnits ↑x = x
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Matrices with entries in a unital C⋆-algebra form a unital C⋆-algebra.  -/
CStarMatrix.instCStarAlgebra : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [StarOrderedRing A] → {n : Type u_2} → [Fintype n] → [DecidableEq n] → CStarAlgebra (CStarMatrix n n A)
-- Init.Data.Array.Int
Array.prod_replicate_int : ∀ {n : ℕ} {a : ℤ}, (Array.replicate n a).prod = a ^ n
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {ρ : Type v} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ}, (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Mathlib.Order.Category.Preord
Preord.instCoeSortType : CoeSort Preord (Type u)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.uliftEquiv_tmul : ∀ (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : CommSemiring 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] (m : M) (n : N),
  (TensorProduct.AlgebraTensorModule.uliftEquiv R A M N) { down := m ⊗ₜ[R] n } =
    { down := m } ⊗ₜ[ULift.{u_3, uR} R] { down := n }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.im_le_im_mul_exp_dist : ∀ (z w : UpperHalfPlane), z.im ≤ w.im * Real.exp (dist z w)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instEquivLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  OrderAddMonoidIso.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- The fpqc precoverage on the category of schemes is the quasi-compact precoverage
on flat morphisms. The covering families are jointly-surjective, quasi-compact families of
flat morphisms.  -/
AlgebraicGeometry.Scheme.fpqcPrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- For all `n ≤ m`, `inclusion n` factors through `Truncated m`.  -/
SimplexCategory.Truncated.inclCompInclusion : {n m : ℕ} →
  (h : n ≤ m) →
    (SimplexCategory.Truncated.incl n m ⋯).comp (SimplexCategory.Truncated.inclusion m) ≅
      SimplexCategory.Truncated.inclusion n
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `g` is analytic in a neighborhood of `closedBall 0 R`.  -/
Complex.ECanonicalDecomp.analyticOnNhd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.ECanonicalDecomp f g R → AnalyticOnNhd ℂ g (Metric.closedBall 0 R)
-- Plausible.ArbitraryFueled
Plausible.ArbitraryFueled.mk : {α : Type} → (ℕ → Plausible.Gen α) → Plausible.ArbitraryFueled α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₂).size ≤ (↑(m₁.union m₂)).size
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxEntryD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : (a : α) × β a),
  x.maxEntryD x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => r.maxEntryD fallback
-- Mathlib.Analysis.InnerProductSpace.OfNorm
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.InnerProductSpaceable.I_prop : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [InnerProductSpaceable E], InnerProductSpaceable.innerProp'✝ E RCLike.I
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_lt_of_pos' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b < c → 0 < a → b < c + a
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.kerodon.sizeOf_spec : sizeOf Mathlib.CrossRef.Database.kerodon = 1
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.prodMk : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β} {g : α → γ},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun x => (f x, g x)) μ
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.pmul_comm : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f g : ArithmeticFunction R), f.pmul g = g.pmul f
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
/-- The direct sum decomposition of the exterior algebra from the graded algebra structure.  -/
ExteriorAlgebra.instDecompositionNatSubmoduleExteriorPower : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → DirectSum.Decomposition fun n => ⋀[R]^n M
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofBijective_symm_comp : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (hf : Function.Bijective ⇑f), (↑(RingEquiv.ofBijective f hf).symm).comp f = NonUnitalRingHom.id R
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_impl_2 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Sum of a list of elements in an intermediate field is in the intermediate field.  -/
IntermediateField.list_sum_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {l : List L}, (∀ x ∈ l, x ∈ S) → l.sum ∈ S
-- Mathlib.RingTheory.Regular.RegularSequence
/-- The ideal generated by a list of elements.  -/
Ideal.ofList : {R : Type u_1} → [inst : Semiring R] → List R → Ideal R
-- Init.Data.UInt.Lemmas
UInt8.sub_lt : ∀ {a b : UInt8}, 0 < b → b ≤ a → a - b < a
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoalParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- **Alias** of `Submodule.coe_subtypeL`. -/
Submodule.coe_subtypeL' : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), ⇑p.subtypeL = ⇑p.subtype
-- Init.System.Uri
System.Uri.UriEscape.rfc3986ReservedChars : List Char
-- Init.Data.Fin.Lemmas
Fin.fin_one_eq_zero : ∀ (a : Fin 1), a = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.restrict_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : AddSubmonoid M}
  {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N'),
  Function.Injective ⇑f → Function.Injective ⇑(AddMonoidHom.restrict h)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- Condition that a `LocalizerMorphism` induces a fully faithful functor
on the localized categories.  -/
CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop