mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Representation isomorphism `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, where the right-hand representation is
defined pointwise by the left regular representation on `k[G]`. The map sends
`single (g₀, ..., gₙ) a ↦ single (g₀⁻¹g₁, ..., gₙ₋₁⁻¹gₙ) (single g₀ a)`.  -/
Rep.diagonalSuccIsoFree : (k G : Type u) →
  [inst : Group G] → [inst_1 : CommRing k] → (n : ℕ) → Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G)
-- Lean.Util.Trace
/-- Convert an `Except` result to a `TraceResult`.
`Except.error` always maps to `.error`.
For `Bool`, `.ok false` maps to `.failure`. For `Option`, `.ok none` maps to `.failure`.  -/
Lean.ExceptToTraceResult : Type → Type → Type
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [toIsFilteredOrEmpty : CategoryTheory.IsFilteredOrEmpty C]
  [nonempty : Nonempty C], CategoryTheory.IsFiltered C
-- Init.Data.UInt.Bitwise
UInt32.toUSize_or : ∀ (a b : UInt32), (a ||| b).toUSize = a.toUSize ||| b.toUSize
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein.probability : ∀ (n : ℕ) (x : ↑unitInterval), ∑ k, (bernstein n ↑k) x = 1
-- Init.Prelude
instDecidableEqUInt32 : DecidableEq UInt32
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_roo : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LT α] [inst_3 : DecidableLT α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roo α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The quotient by a congruence relation preserving addition and scalar multiplication.  -/
ModuleCon.Quotient : {S : Type u_2} → (M : Type u_3) → [inst : Add M] → [inst_1 : SMul S M] → ModuleCon S M → Type u_3
-- Mathlib.Util.Delaborators
/-- Since pi notation and forall notation are interchangeable, we can
parse it by simply using the pre-existing forall parser.  -/
PiNotation.replacePiNotation : Lean.Macro
-- Mathlib.Data.List.Lookmap
List.lookmap_map_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option α) (g : α → β),
  (∀ (a b : α), b ∈ f a → g a = g b) → ∀ (l : List α), List.map g (List.lookmap f l) = List.map g l
-- Mathlib.ModelTheory.PartialEquiv
/-- For two countably generated structure `M` and `N`, if any PartialEquiv
between finitely generated substructures can be extended to any element in the domain and to
any element in the codomain, then there exists an equivalence between `M` and `N`.  -/
FirstOrder.Language.equiv_between_cg : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.CG L M →
    FirstOrder.Language.Structure.CG L N →
      ∀ (g : L.FGEquiv M N), L.IsExtensionPair M N → L.IsExtensionPair N M → ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv
-- Mathlib.GroupTheory.Commutator.Basic
/-- Representatives `(g₁, g₂) : G × G` of commutators `⁅g₁, g₂⁆ ∈ G`.  -/
commutatorRepresentatives : (G : Type u_1) → [Group G] → Set (G × G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Const.unitOfList l cmp).size ≤ l.length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).getD fallback
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getKeyGT k t ho he = Std.DTreeMap.Internal.Impl.getKeyGT k_1 t_1 ⋯ ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Functional equation for the odd Hurwitz zeta function (alternative form).  -/
HurwitzZeta.completedSinZeta_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedSinZeta a (1 - s) = HurwitzZeta.completedHurwitzZetaOdd a s
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_eq : ∀ {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] (f : M ≃ₗ[R] P)
  (g : N ≃ₗ[R] Q), TensorProduct.AlgebraTensorModule.congr f g = TensorProduct.congr f g
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_pos : ∀ {x : ℝ}, 0 < ↑x ↔ 0 < x
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_eq_bot_of_nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] {S : Subgroup G} [Group.IsNilpotent ↥S] {n : ℕ},
  Group.nilpotencyClass ↥S ≤ n → S.lowerCentralSeries n = ⊥
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.ext : ∀ {R : Type u_2} {inst : CommRing R} {n : ℕ} {x y : ChevalleyThm.PolynomialC.InductionObj✝ R n},
  ChevalleyThm.PolynomialC.InductionObj.val✝ x = ChevalleyThm.PolynomialC.InductionObj.val✝ y → x = y
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafification_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Functor Cᵒᵖ D), (CategoryTheory.toSheafification J D).app P = CategoryTheory.toSheafify J P
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential.eq_1 : ∀ (E : Type u_1) (F : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (s : ℝ),
  TemperedDistribution.besselPotential E F s =
    TemperedDistribution.fourierMultiplierCLM F fun x => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson.eq_1 : ∀ {R : Type u} [inst : Ring R] (I : Ideal R), I.jacobson = sInf {J | I ≤ J ∧ J.IsMaximal}
-- Mathlib.Analysis.Convex.Segment
segment_eq_image₂ : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), segment 𝕜 x y = (fun p => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
-- Mathlib.Order.Filter.Cofinite
Function.update_eventuallyEq : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (f : α → β) (a : α) (b : β),
  Function.update f a b =ᶠ[Filter.principal {a}ᶜ] f
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
/-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
reinterpret the `lie_smul` law as an `SMulCommClass`.  -/
LieAlgebra.smulCommClass : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  SMulCommClass R (CommutatorRing L) (CommutatorRing L)
-- Mathlib.Data.List.Sigma
List.kerase_cons_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)},
  a ≠ s.fst → List.kerase a (s :: l) = s :: List.kerase a l
-- Mathlib.CategoryTheory.Sites.Point.Comap
/-- Given a continuous functor `F : C ⥤ D` between sites `(C, J)` and `(D, K)`,
and a point `Φ` of `(D, K)`, this is the isomorphism between
`Φ.skyscraperSheafFunctor ⋙ F.sheafPushforwardContinuous A J K` and
`(Φ.comap F hF).skyscraperSheafFunctor`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctorCompSheafPushforwardContinuous : {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] →
        {K : CategoryTheory.GrothendieckTopology D} →
          (Φ : K.Point) →
            (F : CategoryTheory.Functor C D) →
              [inst_2 : CategoryTheory.RepresentablyFlat F] →
                {J : CategoryTheory.GrothendieckTopology C} →
                  (hF : CategoryTheory.CoverPreserving J K F) →
                    [inst_3 : CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] →
                      (A : Type u_3) →
                        [inst_4 : CategoryTheory.Category.{v, u_3} A] →
                          [inst_5 : CategoryTheory.Limits.HasProducts A] →
                            [inst_6 : F.IsContinuous J K] →
                              Φ.skyscraperSheafFunctor.comp (F.sheafPushforwardContinuous A J K) ≅
                                (Φ.comap F hF).skyscraperSheafFunctor
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instInhabitedTacticM : {α : Type} → Inhabited (Lean.Elab.Tactic.TacticM α)
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S)
-- Init.Data.Array.Extract
Array.extract_eq_pop : ∀ {α : Type u_1} {as : Array α} {stop : ℕ}, stop = as.size - 1 → as.extract 0 stop = as.pop
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.trueExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J) {Z : D}
  (h : (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j)
        ⟨(0, j), ⋯⟩)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
        (e.hom.app (Y j)))
      h
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.key : Lean.Meta.SynthInstance.ConsumerNode → Lean.Expr
-- Mathlib.CategoryTheory.Center.Linear
/-- The `R`-linear structure on a preadditive category `C` equipped with
a ring morphism `R →+* CatCenter C`.  -/
CategoryTheory.Linear.ofRingMorphism : {R : Type w} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] → (R →+* CategoryTheory.CatCenter C) → CategoryTheory.Linear R C
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instMul : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalNonAssocSemiring R] → Mul (HahnSeries Γ R)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.Mem.eq_1 : ∀ {α : Type u_1} (v : α) (c : Std.Sat.CNF.Clause α), Std.Sat.CNF.Clause.Mem v c = ((v, false) ∈ c ∨ (v, true) ∈ c)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.fst = AddMonoid.Coprod.lift (AddMonoidHom.id M) 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃)
  (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') {Z : CochainComplex C ℤ}
  (h :
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingConeCompTriangle f' g').obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f' g').mor₃ h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
          (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯))
        h)
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition : {α : Type u} → α → List α → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (Std.ExtDHashMap.Const.get? m a).isSome = true},
  (Std.ExtDHashMap.Const.get? m a).get h = Std.ExtDHashMap.Const.get m a ⋯
-- Mathlib.Data.Semiquot
Semiquot.mem_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (q : Semiquot α) (b : β), b ∈ Semiquot.map f q ↔ ∃ a ∈ q, f a = b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseₘ.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k k_1 : α),
  k = k_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.eraseₘ k t h = Std.DTreeMap.Internal.Impl.eraseₘ k_1 t_1 ⋯
-- Std.Http.Protocol.H1.Config
/-- Maximum length of chunk extension value (default: 256 bytes).
 -/
Std.Http.Protocol.H1.Config.maxChunkExtValueLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Tactic.LinearCombinationPrime
/-- A proof of `a = b`.  -/
Mathlib.Tactic.LinearCombinationPrime.Expanded.proof : Lean.Term → Mathlib.Tactic.LinearCombinationPrime.Expanded
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The coyoneda embedding `coyoneda.obj X : C ⥤ Type v` for `X : Cᵒᵖ` preserves limits.  -/
CategoryTheory.coyoneda_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (CategoryTheory.coyoneda.obj X)
-- Mathlib.Algebra.Group.AddChar
AddChar.sum_apply : ∀ {ι : Type u_1} {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (s : Finset ι)
  (ψ : ι → AddChar A M) (a : A), (∑ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a
-- Mathlib.Util.Export
Lean.Export.Alloc.mk.injEq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] (map : Std.HashMap α ℕ) (next : ℕ) (map_1 : Std.HashMap α ℕ)
  (next_1 : ℕ), ({ map := map, next := next } = { map := map_1, next := next_1 }) = (map = map_1 ∧ next = next_1)
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars_injective : ∀ {L : Type u_2} [inst : Field L] (F : Subfield L), Function.Injective fun E => Subfield.extendScalars ⋯
-- Lean.Compiler.IR.Basic
/-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`.  -/
Lean.IR.Expr.sproj : ℕ → ℕ → Lean.IR.VarId → Lean.IR.Expr
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.sSup_eq_bsup : ∀ {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}), sSup (o.brange f) = o.bsup f
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Comonad C} (f g : T₁ ⟶ T₂),
  f.app = g.app → f = g
-- Mathlib.Algebra.Category.ModuleCat.Basic
LinearEquiv.toModuleIso_inv : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ : Type v} {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁}
  {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂), e.toModuleIso.inv = ModuleCat.ofHom ↑e.symm
-- Init.Data.UInt.Lemmas
UInt64.zero_ne_one : 0 ≠ 1
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.eLpNorm_inner_lt_top : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f g : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.eLpNorm (fun x => inner 𝕜 (↑↑f x) (↑↑g x)) 1 μ < ⊤
-- Mathlib.Order.Bounded
Set.bounded_lt_Icc : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a b : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Icc a b)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_congr_ae : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {f₁ f₂ : V → E},
  f₁ =ᵐ[MeasureTheory.volume] f₂ → ∀ (x : V), FourierTransform.fourier f₁ x = FourierTransform.fourier f₂ x
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isPrimitive_iff_content_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R}, p.IsPrimitive ↔ p.content = 1
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_nsmul_two_le_of_pos : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : AddCommMonoid M] [ExistsAddOfLE M]
  [IsOrderedCancelAddMonoid M], 0 < x → ∃ y, 0 < y ∧ 2 • y ≤ x
-- Mathlib.Analysis.RCLike.Basic
/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are strictly ordered rings.

Note this is only an instance with `open scoped ComplexOrder`.  -/
RCLike.toIsStrictOrderedRing : ∀ {K : Type u_1} [inst : RCLike K], IsStrictOrderedRing K
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.HashMap.Raw.ofList l).isEmpty = l.isEmpty
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_eq_iff_map_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
  Function.Commute f g → Monotone f → StrictMono g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x = g^[n] x ↔ f x = g x)
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.size.eq_2 : ∀ {α : Type u_1} (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  (Batteries.BinomialHeap.Imp.Heap.cons rank val c s).size = 1 <<< rank + s.size
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getD_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_zero : ∀ {α : Type u_1} [inst : DecidableEq α], Multiset.dedup 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.hom_ext : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {f g : M.exteriorPower n ⟶ N},
  ModuleCat.exteriorPower.mk.postcomp f = ModuleCat.exteriorPower.mk.postcomp g → f = g
-- Mathlib.Topology.Irreducible
/-- In a (pre)irreducible space, a nonempty open set is dense.  -/
IsOpen.dense : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [PreirreducibleSpace X], IsOpen s → s.Nonempty → Dense s
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrameCoeff.congr_simp : ∀ {𝕜 : 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 I_1 : ModelWithCorners 𝕜 E H)
  (e_I : I = I_1) {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_9 : (x : M) → AddCommGroup (V x)]
  [inst_10 : (x : M) → Module 𝕜 (V x)] [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V]
  [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7} (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  [inst_14 : MemTrivializationAtlas e] (b b_1 : Module.Basis ι 𝕜 F),
  b = b_1 →
    ∀ [inst_15 : ContMDiffVectorBundle 1 F V I] (i i_1 : ι),
      i = i_1 →
        ∀ (x : M),
          Bundle.Trivialization.localFrameCoeff I e b i x = Bundle.Trivialization.localFrameCoeff I_1 e_1 b_1 i_1 x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    EuclideanGeometry.angle p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.ord_pos : ∀ {c : Cardinal.{u_1}}, c.IsRegular → 0 < c.ord
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.of.injEq : ∀ (carrier : Type u) [str : SeminormedAddCommGroup carrier] (carrier_1 : Type u)
  (str_1 : SeminormedAddCommGroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Analysis.Analytic.IteratedFDeriv
AnalyticOn.domDomCongr_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E},
  AnalyticOn 𝕜 f Set.univ →
    ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)),
      ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x
-- Lean.DocString.Markdown
/-- Applies a uniform prefix to every line. Empty lines receive the trimmed prefix to avoid trailing
whitespace (which denotes a hard line break).
 -/
Lean.Doc.prefixLines : String → Array String → Array String
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.one_def : ∀ (α : Type u) [inst : One α], 1 = FreeAbelianGroup.of 1
-- Init.Data.Rat.Lemmas
mkRat.eq_1 : ∀ (num : ℤ) (den : ℕ),
  mkRat num den =
    if den_nz : den = 0 then { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }
    else Rat.normalize num den den_nz
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_pos : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α}, 0 < |a| ↔ a ≠ 0
-- Aesop.Saturate
Aesop.isForwardOrDestructRuleName : Aesop.RuleName → Bool
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The **Lusin-Souslin theorem**: the range of a continuous injective function defined on a Polish
space is Borel-measurable.  -/
MeasureTheory.measurableSet_range_of_continuous_injective : ∀ {γ : Type u_3} {β : Type u_4} [inst : TopologicalSpace γ] [PolishSpace γ] [inst_2 : TopologicalSpace β] [T2Space β]
  [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β] {f : γ → β},
  Continuous f → Function.Injective f → MeasurableSet (Set.range f)