mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_list_equiv_foldl : ∀ {α : Type u} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t₁ l)).Equiv
    (List.foldl (fun acc a => Std.DTreeMap.Internal.Impl.insertIfNew! a () acc) t₁ l)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isOpenImmersion_isStableUnderComposition : AlgebraicGeometry.IsOpenImmersion.IsStableUnderComposition
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_natAbs : ∀ {a b : ℤ}, a ∣ ↑b.natAbs ↔ a ∣ b
-- Mathlib.Logic.Equiv.Defs
Equiv.cast_trans : ∀ {α β γ : Sort u_1} (h : α = β) (h2 : β = γ), Equiv.cast ⋯ = (Equiv.cast h).trans (Equiv.cast h2)
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.continuousOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s → ContinuousOn f (f ⁻¹' s)
-- Mathlib.Algebra.Order.Group.Basic
zsmul_lt_zsmul_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α},
  0 < a → m < n → m • a < n • a
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.ofSimplex_le_iff : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (A : X.Subcomplex),
  SSet.Subcomplex.ofSimplex x ≤ A ↔ x ∈ A.obj (Opposite.op { len := n })
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsCyclotomicExtension.aeval_zeta : ∀ (n : ℕ) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n],
  (Polynomial.aeval (IsCyclotomicExtension.zeta n A B)) (Polynomial.cyclotomic n A) = 0
-- Lean.Parser.Extra
Lean.Parser.antiquotExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
cmp_mul_pos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a : R} [PosMulStrictMono R],
  0 < a → ∀ (b c : R), cmp (a * b) (a * c) = cmp b c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {h : k ∈ Std.DTreeMap.filterMap f t},
  Std.DTreeMap.Const.get (Std.DTreeMap.filterMap f t) k h = (f (t.getKey k ⋯) (Std.DTreeMap.Const.get t k ⋯)).get ⋯
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroIntIi : Lean.Grind.ToInt.Zero ℤ Lean.Grind.IntInterval.ii
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The center of a non-unital algebra is the set of elements which commute with every element.
They form a non-unital subalgebra.  -/
NonUnitalSubalgebra.center : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → NonUnitalSubalgebra R A
-- Mathlib.Algebra.Opposites
MulOpposite.op_bijective : ∀ {α : Type u_1}, Function.Bijective MulOpposite.op
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Asymptotics.IsTheta.summable_iff_nat : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F},
  f =Θ[Filter.atTop] g → (Summable f ↔ Summable g)
-- Init.Data.String.Slice
/-- Creates a new slice that contains the first `n` characters \(Unicode code points\) of `s`.

If `n` is greater than the amount of characters in `s`, returns `s`.

Examples:

* `"red green blue".toSlice.take 3 == "red".toSlice`

* `"red green blue".toSlice.take 1 == "r".toSlice`

* `"red green blue".toSlice.take 0 == "".toSlice`

* `"red green blue".toSlice.take 100 == "red green blue".toSlice`
 -/
String.Slice.take : String.Slice → ℕ → String.Slice
-- Mathlib.Data.Set.Prod
Set.offDiag_subset_prod : ∀ {α : Type u_1} (s : Set α), s.offDiag ⊆ s ×ˢ s
-- Lean.Elab.InfoTree.Types
Lean.Elab.setInfoState : {m : Type → Type} → [Lean.Elab.MonadInfoTree m] → Lean.Elab.InfoState → m Unit
-- Mathlib.Order.Filter.Prod
Filter.mem_prod_principal : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : Filter α} {s : Set (α × β)},
  s ∈ f ×ˢ Filter.principal t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f
-- Mathlib.Computability.Language
Language.ext : ∀ {α : Type u_1} {l m : Language α}, (∀ (x : List α), x ∈ l ↔ x ∈ m) → l = m
-- Mathlib.Order.Filter.Pointwise
Filter.smul_le_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g₁ g₂ : Filter β}, g₁ ≤ g₂ → f • g₁ ≤ f • g₂
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.getUnfoldFor? : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) (x y : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F H).app (x, y))
      (ℌ.ev_app.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.MonoidalClosed.uncurry (ℌ.π y x)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The identity continuous intertwining map.  -/
ContIntertwiningMap.id : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] →
                [inst_5 : Module R V] → {π₁ : ContRepresentation R G V} → ContIntertwiningMap π₁ π₁
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_of_le' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  (l : Filter α), (∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) → Asymptotics.IsBigOWith c l f g
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- The canonical isomorphism between the codomains of two co-Cartesian morphisms
lying over the same object.  -/
CategoryTheory.Functor.IsCocartesian.codomainUniqueUpToIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} →
            {a b : 𝒳} →
              (f : R ⟶ S) →
                (φ : a ⟶ b) → [p.IsCocartesian f φ] → {b' : 𝒳} → (φ' : a ⟶ b') → [p.IsCocartesian f φ'] → b ≅ b'
-- Init.Data.String.PosRaw
String.Pos.Raw.ext : ∀ {x y : String.Pos.Raw}, x.byteIdx = y.byteIdx → x = y
-- Batteries.CodeAction.Attr
/-- This attribute marks a code action, which is used to suggest new tactics or replace existing ones.

* `@[tactic_code_action]`: This is a code action which applies to the spaces between tactics,
to suggest a new tactic to change the goal state.

* `@[tactic_code_action kind]`: This is a code action which applies to applications of the tactic
`kind` (a tactic syntax kind), which can replace the tactic or insert things before or after it.

* `@[tactic_code_action kind₁ kind₂]`: shorthand for
`@[tactic_code_action kind₁, tactic_code_action kind₂]`.

* `@[tactic_code_action *]`: This is a tactic code action that applies to all tactics.
Use sparingly.
 -/
Batteries.CodeAction.tactic_code_action : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charmatrix_apply_natDegree : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R}
  [Nontrivial R] (i j : n), (M.charmatrix i j).natDegree = if i = j then 1 else 0
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν),
  g.compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (↑g ∘ f) ⋯
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The Kronecker product of two Hadamard matrices is Hadamard.  -/
Matrix.IsHadamard.kronecker : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : Semiring R] [inst_5 : StarRing R] {A : Matrix m m R} {B : Matrix n n R},
  A.IsHadamard → B.IsHadamard → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).IsHadamard
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_6.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} (t : List (Lean.Doc.Block i b))
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_6 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_7 t (Lean.Doc.Block.brecOn_6.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- `J` commutes with any positively-oriented isometric automorphism.  -/
Orientation.linearIsometryEquiv_comp_rightAngleRotation' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
  0 < LinearMap.det ↑φ.toLinearEquiv → o.rightAngleRotation.trans φ = φ.trans o.rightAngleRotation
-- Aesop.Util.UnionFind
/-- Cluster the `as` according to which `bs` are associated to them by `f`. Two
members `a₁, a₂` of `as` are put in the same cluster iff `f a₁ ∩ f a₂ ≠ ∅`.  -/
Aesop.cluster : {α : Type (max u_1 u_2)} →
  {β : Type u_2} → [BEq α] → [Hashable α] → [BEq β] → [Hashable β] → (α → Array β) → Array α → Array (Array α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.instTensorUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.GrpObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Data.Finset.Sym
Finset.sym2_eq_image : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.sym2 = Finset.image (Function.uncurry Sym2.mk) (s ×ˢ s)
-- Mathlib.Probability.ProbabilityMassFunction.Integrals
PMF.integral_eq_sum : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] [inst_5 : Fintype α] (p : PMF α) (f : α → E),
  ∫ (a : α), f a ∂p.toMeasure = ∑ a, (p a).toReal • f a
-- Mathlib.Data.Vector.Mem
List.Vector.mem_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (b : β) (v : List.Vector α n) (f : α → β),
  b ∈ (List.Vector.map f v).toList ↔ ∃ a ∈ v.toList, f a = b
-- Mathlib.Data.PNat.Prime
PNat.fact_prime_five : Fact (PNat.Prime 5)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonHighlightMatchesOptions.fromJson : Lean.Json → Except String Lean.Lsp.HighlightMatchesOptions
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiff.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {n : WithTop ℕ∞},
  ContDiff ℂ n f → ContDiff ℂ n fun x => Complex.cosh (f x)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The class group of principal ideal domain is finite (in fact a singleton).

See `ClassGroup.fintypeOfAdmissibleOfFinite` for a finiteness proof that works for rings of integers
of global fields.
 -/
instFintypeClassGroupOfIsPrincipalIdealRing : {R : Type u_1} → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsPrincipalIdealRing R] → Fintype (ClassGroup R)
-- Mathlib.Algebra.Star.Basic
TrivialStar.mk : ∀ {R : Type u} [inst : Star R], (∀ (r : R), star r = r) → TrivialStar R
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.rTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) (x : TensorProduct 𝕜 E G),
  (LinearIsometryEquiv.rTensor G f) x = (LinearEquiv.rTensor G f.toLinearEquiv) x
-- Mathlib.Data.Set.Image
/-- If the preimage of a set under a surjective map is a subsingleton,
the set is a subsingleton.  -/
Set.subsingleton_of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → ∀ (s : Set β), (f ⁻¹' s).Subsingleton → s.Subsingleton
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.subtypeVal.match_1.eq_2 : ∀ (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → x_1.Arrow (TypeVec.repeat x Prop) → Fin2 x → Sort u_2) (n : ℕ)
  (x : TypeVec.{u_1} n.succ) (x_1 : x.Arrow (TypeVec.repeat n.succ Prop))
  (h_1 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (x_2 : x.Arrow (TypeVec.repeat n.succ Prop)) → (i : Fin2 n) → motive n.succ x x_2 i.fs)
  (h_2 :
    (n : ℕ) → (x : TypeVec.{u_1} n.succ) → (x_2 : x.Arrow (TypeVec.repeat n.succ Prop)) → motive n.succ x x_2 Fin2.fz),
  (match n.succ, x, x_1, Fin2.fz with
    | n.succ, x, x_2, i.fs => h_1 n x x_2 i
    | n.succ, x, x_2, Fin2.fz => h_2 n x x_2) =
    h_2 n x x_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F]
  (a : A),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a)
      ((G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) =
    G.map ((L.leftKanExtensionUnit F).app a)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Weierstrass `℘` function with the `l₀`-term missing.
This is mainly a tool for calculations where one would want to omit a diverging term.
This has the notation `℘[L - l₀]` in the namespace `PeriodPairs`.  -/
PeriodPair.«term℘[_-_]» : Lean.ParserDescr
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.isConstant.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (x : Std.Sat.AIG.Decl α)
  (h_1 : Unit → motive Std.Sat.AIG.Decl.false) (h_2 : (x : Std.Sat.AIG.Decl α) → motive x),
  (x = Std.Sat.AIG.Decl.false → False) →
    (match x with
      | Std.Sat.AIG.Decl.false => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Init.Data.BitVec.Lemmas
BitVec.lt_add_one : ∀ {w : ℕ} {b : BitVec w}, b ≠ BitVec.allOnes w → b < b + 1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_eq_of_lt_right : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v x < v y → v (x - y) = v y
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.toRingEquiv_uniqueAlgEquiv : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [inst_4 : Unique M],
  ↑(AddMonoidAlgebra.uniqueAlgEquiv R M) = AddMonoidAlgebra.uniqueRingEquiv M
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods : Type
-- Mathlib.RingTheory.Smooth.Basic
/-- Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] A`
with kernel `I` (typically a presentation `R[X] → A`),
`A` is formally smooth iff the `P`-linear map `I/I² → A ⊗[P] Ω[P⁄R]` is split injective.
Also see `Algebra.Extension.formallySmooth_iff_split_injection`
for the version in terms of `Extension`.
 -/
Algebra.FormallySmooth.iff_split_injection : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {P : Type u_2}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] [Algebra.FormallySmooth R P] [inst_6 : Algebra P A]
  [IsScalarTower R P A],
  Function.Surjective ⇑(algebraMap P A) →
    (Algebra.FormallySmooth R A ↔ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P A = LinearMap.id)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.card_le_iff : ∀ {o : Ordinal.{u_1}} {c : Cardinal.{u_1}}, o.card ≤ c ↔ o < (Order.succ c).ord
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_const_left : ∀ {w a b : ℕ} {c : BitVec w},
  BitVec.ofNat w a &&& (BitVec.ofNat w b &&& c) = BitVec.ofNat w a &&& BitVec.ofNat w b &&& c
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.repr_isUnitSMul : ∀ {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : CommSemiring R₂]
  [inst_2 : Module R₂ M] {v : Module.Basis ι R₂ M} {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)) (x : M) (i : ι),
  ((v.isUnitSMul hw).repr x) i = ⋯.unit⁻¹ • (v.repr x) i
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M},
  y ∈ f.source →
    s ⊆ f.source → Filter.map (↑(f.extend I)) (nhdsWithin y s) = nhdsWithin (↑(f.extend I) y) (↑(f.extend I) '' s)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x) ∈
      NumberField.mixedEmbedding.fundamentalCone K ↔
    x ∈ NumberField.mixedEmbedding.fundamentalCone K
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_v_comp_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) (G.d q q') =
    CategoryTheory.CategoryStruct.comp (φ.f p) (G.d p q')
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A function on `ℍ` which is invariant under `SL(2, ℤ)`, and is `O ((im τ) ^ t)` at `I∞` for
some `0 ≤ t`, is bounded on `ℍ` by a constant multiple of `(max (im τ) (1 / im τ)) ^ t`.

This will be applied to `f τ * (im τ) ^ (k / 2)` for `f` a modular form of weight `k`, taking
`t = 0` if `f` is cuspidal, and `t = k / 2` otherwise.  -/
ModularGroup.exists_bound_of_invariant_of_isBigO : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ},
      0 ≤ t →
        (f =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) →
          (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), f (g • τ) = f τ) →
            ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
-- Mathlib.Analysis.Convex.Star
/-- The translation of a star-convex set is also star-convex.  -/
StarConvex.preimage_add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x z : E} {s : Set E}, StarConvex 𝕜 (z + x) s → StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], r.toList = [] ↔ ¬Std.PRange.UpwardEnumerable.least < r.upper
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousOn.eval : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] [inst_5 : TopologicalSpace Z]
  {f : Z → F} {g : Z → X} {s : Set Z}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun z => (f z) (g z)) s
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback an `Order.Frame.MinimalAxioms` along an injection.  -/
Function.frameMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  Order.Frame.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) → Order.Frame.MinimalAxioms α
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size)
  (h_1 :
    (size : ℕ) →
      (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
        (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
          motive ⟨{ size := size, buckets := buckets }, hm⟩),
  (match ⟨{ size := size, buckets := buckets }, hm⟩ with
    | ⟨{ size := size, buckets := buckets }, hm⟩ => h_1 size buckets hm) =
    h_1 size buckets hm
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.bind₁_onePoly_wittPolynomial : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), (MvPolynomial.bind₁ WittVector.onePoly) (wittPolynomial p ℤ n) = 1
-- Mathlib.Data.FinEnum
/-- `FinEnum.Equiv` states that type `α` is in bijection with `Fin card`,
the size of the `FinEnum`  -/
FinEnum.equiv : {α : Sort u_1} → [self : FinEnum α] → α ≃ Fin (FinEnum.card α)
-- Mathlib.Algebra.Group.Basic
add_sub_sub_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a + b - (a - c) = b + c
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.mk : Lean.Expr → Option Lean.Name → Option Lean.Name → Lean.Meta.GeneralizeArg
-- Init.Core
/-- An equivalence relation is reflexive: `r x x`  -/
Equivalence.refl : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ (x : α), r x x