mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioo_of_Ioo : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α},
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioo (a i) (b i)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.brecOn.go : {motive : Nat.Partrec.Code → Sort u} →
  (t : Nat.Partrec.Code) →
    ((t : Nat.Partrec.Code) → Nat.Partrec.Code.below t → motive t) → motive t ×' Nat.Partrec.Code.below t
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.insertIfNew a b = m_1.insertIfNew a b_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_0_of_two_eq_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F], 2 = 0 → WeierstrassCurve.ofJ 0 = WeierstrassCurve.ofJ0 F
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_toInt64 : ∀ (x : ISize), x.toInt64.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Topology.ClusterPt
/-- If `x` is not an isolated point of a topological space, then `{x}ᶜ` is dense in the whole
space.  -/
dense_compl_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot], Dense {x}ᶜ
-- Lean.Elab.DocString
/-- An expander for directives in docstrings.
 -/
Lean.Doc.DocDirectiveExpander : Type
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of
a partition of unity from a collection of “bump” functions.  -/
Finset.prod_one_sub_ordered : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommRing R] [inst_1 : LinearOrder ι] (s : Finset ι) (f : ι → R),
  ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_hom_app : ∀ {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)
  (X₁ X₂ X₃ : C),
  (CategoryTheory.MonoidalCategoryStruct.associator
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₁)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₂)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₃)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Localization.Monoidal.μ L W ε X₁ X₂).hom
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₃)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Localization.Monoidal.μ L W ε (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) X₃).hom
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
            (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Localization.Monoidal.μ L W ε X₁
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃)).inv
            (CategoryTheory.MonoidalCategoryStruct.tensorHom
              (CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X₁))
              (CategoryTheory.Localization.Monoidal.μ L W ε X₂ X₃).inv))))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instNullSingletonClassMixedSpaceVolume : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], MeasureTheory.NullSingletonClass MeasureTheory.volume
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_apply : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α),
  (thickenedIndicator δ_pos E) x = (thickenedIndicatorAux δ E x).toNNReal
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.mk : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂},
  (∀ (x y : M), f (x + y) = f x + f y) → (∀ (c : R) (x : M), f (c • x) = c • f x) → IsLinearMap R f
-- Mathlib.Topology.Order.Completion
Order.Fill.instDenselyOrdered : ∀ {α : Type u_1} [inst : LinearOrder α], DenselyOrdered (Order.Fill α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (compare k ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKeyD fallback)).isLE = true
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.noConfusionType : Sort v✝ → Lean.Compiler.LCNF.Purity → Lean.Compiler.LCNF.Purity → Sort v✝
-- Batteries.Util.ProofWanted
instance_wanted.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₂_comp : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20}
  {P : Type u_21} {Q : Type u_22} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  [inst_3 : Semiring R₄] [inst_4 : Semiring R₅] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q]
  [inst_9 : Module R M] [inst_10 : Module R₂ N] [inst_11 : Module R₃ P] [inst_12 : Module R₄ Q] [inst_13 : Module R₅ P]
  [inst_14 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] [inst_15 : SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} {R₆ : Type u_23}
  {Q' : Type u_24} [inst_16 : Semiring R₆] [inst_17 : AddCommMonoid Q'] [inst_18 : Module R₆ Q'] {σ₆₂ : R₆ →+* R₂}
  {σ₆₃ : R₆ →+* R₃} {σ₆₄ : R₆ →+* R₄} [inst_19 : RingHomCompTriple σ₆₂ σ₂₃ σ₆₃]
  [inst_20 : RingHomCompTriple σ₆₄ σ₄₂ σ₆₂] [inst_21 : RingHomCompTriple σ₆₄ σ₄₃ σ₆₃] (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P)
  (g : Q →ₛₗ[σ₄₂] N) (f : Q' →ₛₗ[σ₆₄] Q), h.compl₂ (g ∘ₛₗ f) = (h.compl₂ g).compl₂ f
-- Init.Data.Vector.Lemmas
Vector.all_eq_true_iff_forall_mem : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = true ↔ ∀ x ∈ xs, p x = true
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (N₁ : Type u_4) (N₂ : Type u_5) [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] [inst_3 : Module R N₁] [inst_4 : Module R N₂] [inst_5 : Module (Localization M) N₁]
  [inst_6 : Module (Localization M) N₂] [IsScalarTower R (Localization M) N₁] [IsScalarTower R (Localization M) N₂],
  LinearMap.CompatibleSMul N₁ N₂ (Localization M) R
-- Mathlib.Data.List.Basic
List.replicate_add : ∀ {α : Type u} (m n : ℕ) (a : α), List.replicate (m + n) a = List.replicate m a ++ List.replicate n a
-- Mathlib.Tactic.NormNum.Result
/-- Untyped version of `Result.isNegNNRat`.  -/
Mathlib.Meta.NormNum.Result'.isNegNNRat : Lean.Expr → ℚ → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.ext_iff : ∀ {α : Type u_1} {f : α → α} {x y : IterateMulAct f}, x = y ↔ x.val = y.val
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.stronglyAdapted : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.StronglyAdapted ℱ f
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `iterateFrobenius` as a semilinear map over a subfield `F` of `K`, w.r.t. the
iterated Frobenius homomorphism on `F`.  -/
IsPurelyInseparable.iterateFrobeniusₛₗ : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : IsPurelyInseparable.HasExponent K L] →
              (p : ℕ) →
                [ExpChar K p] →
                  [inst_5 : Field F] →
                    [inst_6 : Algebra F K] →
                      [inst_7 : Algebra F L] →
                        [IsScalarTower F K L] →
                          [inst_9 : ExpChar F p] →
                            {n : ℕ} → IsPurelyInseparable.exponent K L ≤ n → L →ₛₗ[iterateFrobenius F p n] K
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instBot : {α : Type u} → [inst : Group α] → Bot (GroupTopology α)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.ae_comp_of_ae_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {p : β → Prop},
  MeasurableSet {z | p z} → (∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z) → ∀ᵐ (z : β) ∂μ.bind ⇑κ, p z
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.coe_valA' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (p : Subalgebra R A), ⇑p.valA = ⇑p.subtype
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Const.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
/-- The Fontaine's theta map modulo `p^(n+1)`.
It is the composition of the following ring homomorphisms.
`𝕎 R♭ --𝕎(Frob^-n)-> 𝕎 R♭ --𝕎(coeff 0)-> 𝕎(R/p) --gh_n-> R/p^(n+1)`
 -/
WittVector.fontaineThetaModPPow : (R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : Fact ¬IsUnit ↑p] → (n : ℕ) → WittVector p (PreTilt R p) →+* R ⧸ Ideal.span {↑p} ^ (n + 1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f]
  (x : ↥(AlgebraicGeometry.Scheme.Hom.image f)),
  Function.Injective
    ⇑(CategoryTheory.ConcreteCategory.hom
        ((TopCat.Presheaf.stalkFunctor CommRingCat x).map (AlgebraicGeometry.Scheme.Hom.toImage f).c))
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_eq_zero : ∀ (α : Type u) [IsEmpty α], Cardinal.mk α = 0
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.vadd : ∀ {α : Type u_4} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : VAdd α M] [VAddAssocClass α M M] (c : AddCon M)
  (a : α) {w x : M}, c w x → c (a +ᵥ w) (a +ᵥ x)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Standard symmetric relations on types are internal symmetric relations in the category of
types.  -/
TypeCat.SymmetricRelation.ofSymmetric : {X : Type w} →
  {φ : X → X → Prop} → [Std.Symm φ] → CategoryTheory.SymmetricRelation (TypeCat.p₁OfRel φ) (TypeCat.p₂OfRel φ)
-- Mathlib.Algebra.GroupWithZero.Action.Units
/-- Right scalar multiplication as a bijection.  -/
Equiv.smulRight : {α : Type u_4} → {β : Type u_5} → [inst : GroupWithZero α] → [MulAction α β] → {a : α} → a ≠ 0 → β ≃ β
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.op_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), MulOpposite.op ↑n = ↑n
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo : Type
-- Init.System.IO
IO.FileRight.mk.inj : ∀ {user group other user_1 group_1 other_1 : IO.AccessRight},
  { user := user, group := group, other := other } = { user := user_1, group := group_1, other := other_1 } →
    user = user_1 ∧ group = group_1 ∧ other = other_1
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_ofRowLens : ∀ {w : List ℕ} {hw : w.SortedGE} {c : ℕ × ℕ}, c ∈ YoungDiagram.ofRowLens w hw ↔ ∃ (h : c.1 < w.length), c.2 < w[c.1]
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂_toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂),
  (Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) (a : α), (κ.sectL b) a = κ (a, b)
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuous.id` -/
ScottContinuous.fun_id : ∀ {α : Type u_1} [inst : Preorder α], ScottContinuous fun x => x
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.tensorProdEqualizer_ι : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B),
  (CommRingCat.Under.tensorProdEqualizer f g).ι =
    (R.tensorProd S).map ((CommRingCat.toAlgHom f).equalizer (CommRingCat.toAlgHom g)).val.toUnder
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_ex : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {θ : L.BoundedFormula α l.succ}
  {v : α → M} {xs : Fin l → M}, θ.ex.Realize v xs ↔ ∃ a, θ.Realize v (Fin.snoc xs a)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.replace.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (b : β a) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.replace a b x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      bif k == a then Std.DHashMap.Internal.AssocList.cons a b l
      else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.replace a b l)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum'_map_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) {a a' : A} (f : a ⟶ a'),
  (F.sum' G).map ((CategoryTheory.Sum.inl_ A B).map f) = F.map f
-- Mathlib.Data.Holor
Holor.slice_add : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : Add α] (i : ℕ) (hid : i < d) (x y : Holor α (d :: ds)),
  x.slice i hid + y.slice i hid = (x + y).slice i hid
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.mabs : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableInv α] [MeasurableSup₂ α] {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun x => |f x|ₘ) μ
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swap_obj_X : ∀ (X : Bipointed), (Bipointed.swap.obj X).X = X.X
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_nonempty_iff_of_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ} {s : Set α},
  0 < ε → ((Metric.thickening ε s).Nonempty ↔ s.Nonempty)
-- Mathlib.Topology.MetricSpace.Algebra
IsBoundedSMul.toUniformContinuousConstSMul : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β], UniformContinuousConstSMul α β
-- Lean.Meta.Tactic.Grind.AC.Util
_private.Lean.Meta.Tactic.Grind.AC.Util.0.Lean.Meta.Grind.AC.insertOpId : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ) → Lean.Expr → ℕ → Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.integral_rpowIntegrand₀₁_one_pos : ∀ {p : ℝ}, p ∈ Set.Ioo 0 1 → 0 < ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1
-- Mathlib.Analysis.RCLike.Inner
RCLike.mul_wInner_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (c : 𝕜) (w : ι → ℝ)
  (f g : (i : ι) → E i), c * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w]
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.ExceptT.wp_apply_eq : ∀ {m : Type u → Type z} {α ε : Type u} {Pred : Type u_1} {EPred : Type u_2} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] (x : ExceptT ε m α) (post : α → Pred)
  (epost : EPost.Cons✝ (ε → Pred) EPred),
  Std.Internal.Do.wp x post epost =
    Std.Internal.Do.wp x.run (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail
-- Mathlib.RingTheory.DedekindDomain.Different
/-- If the module `I` is spanned by the basis `b`, then its `traceDual` module is spanned by
`b.traceDual`.
 -/
Submodule.traceDual_span_of_basis : ∀ (A : Type u_1) {K : Type u_2} {L : Type u} {B : Type u_4} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L]
  [inst_11 : FiniteDimensional K L] [inst_12 : Algebra.IsSeparable K L] (I : Submodule B L) {ι : Type u_3}
  [inst_13 : Finite ι] [inst_14 : DecidableEq ι] (b : Module.Basis ι K L),
  Submodule.restrictScalars A I = Submodule.span A (Set.range ⇑b) →
    Submodule.restrictScalars A (Submodule.traceDual A K I) = Submodule.span A (Set.range ⇑b.traceDual)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.isMulCommutative : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α], IsMulCommutative α
-- Mathlib.Algebra.MvPolynomial.Equiv
AlgEquiv.ofAlgHom.congr_simp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f f_1 : A₁ →ₐ[R] A₂) (e_f : f = f_1) (g g_1 : A₂ →ₐ[R] A₁)
  (e_g : g = g_1) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁),
  AlgEquiv.ofAlgHom f g h₁ h₂ = AlgEquiv.ofAlgHom f_1 g_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_iSup : ∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_2} {f : ι → Subgroup Mˣ}, (iSup f).ofUnits = ⨆ i, (f i).ofUnits
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.X.match_1.eq_2 : ∀ {ι : Type u_1} (motive : Option ι → Sort u_2) (h_1 : (x : ι) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_sUnion_iff : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {s : Set (Set α)},
  Order.cof α ≠ Cardinal.aleph0 → Cardinal.mk ↑s < Order.cof α → (IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x)
-- Mathlib.Data.List.Sym
List.map_mk_disjoint_sym2 : ∀ {α : Type u_1} (x : α) (xs : List α), x ∉ xs → (List.map (fun y => s(x, y)) xs).Disjoint xs.sym2
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNat_realSqrt : ∀ {x : ℝ} {nx ny : ℕ}, Mathlib.Meta.NormNum.IsNat x nx → ny * ny = nx → Mathlib.Meta.NormNum.IsNat (√x) ny
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The quotient map from the 1-cycles of `A`, as a submodule of `G →₀ A`, to `H₁(G, A)`.  -/
groupHomology.H1π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k ↥(groupHomology.cycles₁ A) ⟶ groupHomology.H1 A
-- Lean.Parser.Term
/-- `+zeta` immediately inlines the `let` value after elaboration (it zeta reduces the `let`).
 -/
Lean.Parser.Term.letOptZeta : Lean.Parser.Parser
-- Lean.Meta.Sym.Pattern
/-- A lightweight structural definitional equality for the symbolic simulation framework.
Unlike the full `isDefEq`, it avoids expensive operations while still supporting Miller pattern unification.
 -/
Lean.Meta.Sym.isDefEqS : Lean.Expr →
  Lean.Expr →
    optParam Bool true →
      optParam Bool true → optParam (Array Lean.MVarId) #[] → optParam (Array Lean.MVarId) #[] → Lean.Meta.Sym.SymM Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_univ : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ}, n ≠ 0 → n • Set.univ = Set.univ
-- Init.Data.BitVec.Lemmas
/-- `rotateLeft` equals the bit fiddling definition of `rotateLeftAux` when the rotation amount is
smaller than the bitwidth.  -/
BitVec.rotateLeft_eq_rotateLeftAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, r < w → x.rotateLeft r = x.rotateLeftAux r
-- Init.Data.List.BasicAux
List.append_cancel_left : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = as ++ cs → bs = cs
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
LinearMap.compLeft.eq_1 : ∀ {R : Type u} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1),
  f.compLeft I = { toFun := fun h => ⇑f ∘ h, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.ProdSpaceFun : Type u → Type v → Type (max u v)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- **Alias** of `Ideal.hasFiniteMulSupport_coe`.

---

For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^(val_v(I))`, regarded as a fractional ideal, is not `(1)`.  -/
Ideal.finite_mulSupport_coe : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    Function.HasFiniteMulSupport fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommGroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α], Colex.instCommGroup = { toGroup := Colex.instGroup, mul_comm := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x ≠ 0 → ∃ u, u • x ∈ NumberField.mixedEmbedding.fundamentalCone K
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instInvolutiveStar : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → InvolutiveStar (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] → InvolutiveStar (DirectLimit G f)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- When `p = ∞`, this lemma does not hold without the additional assumption `Nonempty ι` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.nnnorm_equiv_symm_const'` for a version which exchanges the hypothesis `p ≠ ∞` for
`Nonempty ι`.  -/
PiLp.nnnorm_toLp_const : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ (b : β), ‖WithLp.toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊