mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.DateTime
_private.Std.Time.DateTime.0.Std.Time.DateTime.mk.injEq : ∀ (date : Thunk Std.Time.PlainDateTime) (timestamp : Std.Time.Timestamp) (rules : Std.Time.TimeZone.ZoneRules)
  (timezone : Std.Time.TimeZone) (date_1 : Thunk Std.Time.PlainDateTime) (timestamp_1 : Std.Time.Timestamp)
  (rules_1 : Std.Time.TimeZone.ZoneRules) (timezone_1 : Std.Time.TimeZone),
  ({ date := date, timestamp := timestamp, rules := rules, timezone := timezone } =
      { date := date_1, timestamp := timestamp_1, rules := rules_1, timezone := timezone_1 }) =
    (date = date_1 ∧ timestamp = timestamp_1 ∧ rules = rules_1 ∧ timezone = timezone_1)
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.mk_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {S : AddSubgroup G} (g : G) (hg : g ∈ S)
  (a : α), ⟨g, hg⟩ +ᵥ a = g +ᵥ a
-- Mathlib.Order.Filter.CardinalInter
/-- Supremum of two `CardinalInterFilter`s is a `CardinalInterFilter`.  -/
Filter.cardinalInterFilter_sup_eq : ∀ {α : Type u} {c : Cardinal.{u}} (l₁ l₂ : Filter α) [CardinalInterFilter l₁ c] [CardinalInterFilter l₂ c],
  CardinalInterFilter (l₁ ⊔ l₂) c
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural projection
ordered homomorphism from the lexicographic M ×ₗ N to M.  -/
OrderAddMonoidHom.fstₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] →
      [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → Lex (α × β) →+o α
-- Mathlib.CategoryTheory.Conj
/-- An isomorphism between two objects defines a monoid isomorphism between their
monoid of endomorphisms.  -/
CategoryTheory.Iso.conj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.End X ≃* CategoryTheory.End Y
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)), AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint (T.SpecTensorTo p) = T
-- Mathlib.Control.Basic
seq_bind_eq : ∀ {α β γ : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (x : m α) {g : β → m γ} {f : α → β},
  f <$> x >>= g = x >>= g ∘ f
-- Mathlib.Topology.Constructions.SumProd
Topology.IsEmbedding.inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsEmbedding Sum.inl
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instNormedAddCommGroup : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] → [hp : Fact (1 ≤ p)] → NormedAddCommGroup ↥(MeasureTheory.Lp E p μ)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points, whose `vectorSpan` is finite-dimensional, is coplanar if and only if their
`vectorSpan` has dimension at most `2`.  -/
coplanar_iff_finrank_le_two : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [FiniteDimensional k ↥(vectorSpan k s)],
  Coplanar k s ↔ Module.finrank k ↥(vectorSpan k s) ≤ 2
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` on which a normal subgroup `S ≤ G` acts trivially, the short
complex `H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A)` is exact.  -/
groupHomology.H1CoresCoinfOfTrivial_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)], (groupHomology.H1CoresCoinfOfTrivial A S).Exact
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDocumentFilter.toJson : Lean.Lsp.DocumentFilter → Lean.Json
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.denote_input_vec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} {assign : α → Bool} {idx : ℕ} {hidx : idx < len}
  (s : Std.Sat.AIG.RefVecEntry α len) {input : β s.aig len} {hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size},
  ⟦assign, { aig := (f s.aig input).aig, ref := (s.vec.get idx hidx).cast hcast }⟧ =
    ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.of_left_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (v : V),
  LinearMap.transvection 0 v = LinearMap.id
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_map_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  (F : CategoryTheory.Functor G C) {X Y : G} (f : X ⟶ Y),
  ((CategoryTheory.Core.functorToCore F).map f).iso.hom = F.map f
-- Mathlib.Order.Category.BddLat
/-- The underlying lattice of a bounded lattice.  -/
BddLat.toLat : BddLat → Lat
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) [inst_1 : Inhabited (β a)], m.get! a = m_1.get! a
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedSymExtensionState : Inhabited Lean.Meta.Sym.SymExtensionState
-- Lean.LocalContext
/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes.  -/
Lean.LocalContext.sanitizeNames : Lean.LocalContext → StateM Lean.NameSanitizerState Lean.LocalContext
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableDiv₂` if `uncurry (· / ·)` is a measurable function.
For a typeclass assuming measurability of `(c / ·)` and `(· / c)` see `MeasurableDiv`.  -/
MeasurableDiv₂ : (G₀ : Type u_2) → [MeasurableSpace G₀] → [Div G₀] → Prop
-- Mathlib.Order.Lattice.Nat
Nat.iInf_lt_succ' : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨅ k, ⨅ (_ : k < n + 1), u k = u 0 ⊓ ⨅ k, ⨅ (_ : k < n), u (k + 1)
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `absorbs_iInter`. -/
Absorbs.iInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {ι : Sort u_3} [Finite ι] {s : ι → Set α}, (∀ (i : ι), Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i, s i) t
-- Mathlib.Order.Disjoint
Complementeds.instInhabited : {α : Type u_1} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → Inhabited (Complementeds α)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ici_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ici a)), Subtype.val '' Set.Iic b = Set.Icc a ↑b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_ne_nil_iff : ∀ {m n : ℕ}, (m...=n).toList ≠ [] ↔ m ≤ n
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The type of morphisms in the category `F.DescentData' sq sq₃`.  -/
CategoryTheory.Pseudofunctor.DescentData'.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  F.DescentData' sq sq₃ → F.DescentData' sq sq₃ → Type (max t v')
-- Mathlib.Order.Circular
CircularOrder.toCircularPartialOrder : {α : Type u_1} → [self : CircularOrder α] → CircularPartialOrder α
-- Mathlib.Geometry.Manifold.Immersion
/-- Every `ModelWithCorners 𝕜 E H` is an immersion when viewed as a map `H → E`.  -/
ModelWithCorners.isImmersion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ},
  Manifold.IsImmersion I (modelWithCornersSelf 𝕜 E) ↑n ↑I
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientQuotientEquivQuotientAux_mk : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M)
  (x : G ⧸ N), (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) x
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- `HasWeakLimit F` represents the mere existence of a weak limit for `F`.  -/
CategoryTheory.Limits.HasWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} → [inst_1 : CategoryTheory.Category.{v_3, u_3} C] → CategoryTheory.Functor J C → Prop
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiable_mul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I 1 G] {a : G},
  MDiff fun x => x * a
-- Mathlib.InformationTheory.Hamming
Hamming.instPseudoMetricSpace : {ι : Type u_2} → {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → PseudoMetricSpace (Hamming β)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureForallPureForall : ∀ {α : Sort u_1} (σs : List (Type u_2)) (P : α → Prop), Std.Do.SPred.Tactic.IsPure spred(∀ x, ⌜P x⌝) (∀ (x : α), P x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).getKey! k = default
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), ↑S.toSubmodule = ↑S
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A surjective linear map `f` with finite-dimensional codomain is an open map.  -/
LinearMap.isOpenMap_of_finiteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F]
  [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜]
  [T2Space E] [FiniteDimensional 𝕜 E] (f : F →ₗ[𝕜] E), Function.Surjective ⇑f → IsOpenMap ⇑f
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_pi : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : Fintype ι] [Module.Free R M] [Module.Finite R M] (f : ι → M →ₗ[R] M),
  LinearMap.det (LinearMap.pi fun i => f i ∘ₗ LinearMap.proj i) = ∏ i, LinearMap.det (f i)
-- Lean.AuxRecursor
Lean.auxRecExt : Lean.TagDeclarationExtension
-- Lean.Declaration
Lean.OpaqueVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (isUnsafe : Bool) (all : List Lean.Name)
  (toConstantVal_1 : Lean.ConstantVal) (value_1 : Lean.Expr) (isUnsafe_1 : Bool) (all_1 : List Lean.Name),
  ({ toConstantVal := toConstantVal, value := value, isUnsafe := isUnsafe, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, isUnsafe := isUnsafe_1, all := all_1 }) =
    (toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ isUnsafe = isUnsafe_1 ∧ all = all_1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Nonzero divisors have valuation greater than zero.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : ↥(nonZeroDivisors R)), 0 < v.intValuation ↑x
-- Mathlib.Data.List.Chain
List.IsChain.tail : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l → List.IsChain R l.tail
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.mk'_edge : ∀ {X : SSet.Truncated 2} (s : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })),
  (SSet.Truncated.Edge.mk' s).edge = s
-- Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.MkIff.Shape.mk.inj : ∀ {variablesKept : List Bool} {neqs : Option ℕ} {variablesKept_1 : List Bool} {neqs_1 : Option ℕ},
  { variablesKept := variablesKept, neqs := neqs } = { variablesKept := variablesKept_1, neqs := neqs_1 } →
    variablesKept = variablesKept_1 ∧ neqs = neqs_1
-- Batteries.Util.Panic
Batteries.panicWith_eq : ∀ {α : Sort u_1} (v : α) (msg : String), Batteries.panicWith v msg = v
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
  (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃)
  (fst : T.obj₂ ⟶ T.obj₁)
  (total :
    CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr =
      CategoryTheory.CategoryStruct.id T.obj₂),
  (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inl = T.mor₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {l : List (α × β)},
  Std.DTreeMap.Raw.Const.ofList l cmp = Std.DTreeMap.Raw.Const.insertMany ∅ l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.foldr_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : α → β → δ → δ} {init : δ}, t₁.Equiv t₂ → Std.TreeMap.foldr f init t₁ = Std.TreeMap.foldr f init t₂
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} (n : ℕ),
  MvPowerSeries.constantCoeff f = 0 → ↑n ≤ (f ^ n).order
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.pow_eq_on_of_mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  (∀ x ∈ f.support ∩ g.support, f x = g x) → ∀ (k : ℕ), ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setLctxInitIndices : Lean.Meta.Simp.Context → Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- The **Cauchy product formula** for the product of two infinite sums indexed by `ℕ`, expressed
by summing on `Finset.range`.

See also `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm` if `f` and `g` are absolutely summable.
 -/
Summable.tsum_mul_tsum_eq_tsum_sum_range : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α]
  [IsTopologicalSemiring α],
  Summable f →
    Summable g →
      (Summable fun x => f x.1 * g x.2) →
        (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse : ∀ (X : SSet.Truncated 2) {Y Y' : SSet.Truncated 2} (g : Y ⟶ Y'),
  ((CategoryTheory.Functor.id X.HomotopyCategory).prod (SSet.Truncated.mapHomotopyCategory g)).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y') =
    (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (↑n) (↑n + 1))
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.varMap : Lean.Meta.Simp.Arith.Int.ToLinear.State → Lean.Meta.KExprMap ℕ
-- Mathlib.RingTheory.HopfAlgebra.Convolution
AlgHom.convGroup : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Bialgebra R C] → [inst_4 : HopfAlgebra R A] → Group (WithConv (A →ₐ[R] C))
-- Mathlib.Algebra.Group.End
Equiv.Perm.instOne : {α : Type u_4} → One (Equiv.Perm α)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.WF.modify : ∀ {α : Type u_1} {cut : α → Ordering} {cmp : α → α → Ordering} {f : α → α} {t : RBTree.RBNode α},
  RBTree.RBNode.OnRoot (fun x => RBTree.RBNode.cmpEq cmp (f x) x) (RBTree.RBNode.zoom cut t).1 →
    RBTree.RBNode.WF cmp t → RBTree.RBNode.WF cmp (RBTree.RBNode.modify cut f t)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.mk : {α : Type u} → (α → Option α) → (ℕ → α → Option α) → Std.PRange.UpwardEnumerable α
-- Mathlib.Topology.NhdsSet
/-- This inequality cannot be improved to an equality. For instance,
if `X` has two elements and the coarse topology and `s` and `t` are distinct singletons then
`𝓝ˢ (s ∩ t) = ⊥` while `𝓝ˢ s ⊓ 𝓝ˢ t = ⊤` and those are different.  -/
nhdsSet_inter_le : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s t : Set X), nhdsSet (s ∩ t) ≤ nhdsSet s ⊓ nhdsSet t
-- Init.Core
/-- Auxiliary definition for `Quot.rec`.  -/
Quot.indep : {α : Sort u} → {r : α → α → Prop} → {motive : Quot r → Sort v} → ((a : α) → motive (Quot.mk r a)) → α → PSigma motive
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instFunLike : {A : Type u_2} →
  {B : Type u_3} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → FunLike (A →ₜ+ B) A B
-- Mathlib.Algebra.BigOperators.Finprod
finprod_true : ∀ {M : Type u_2} [inst : CommMonoid M] (f : True → M), ∏ᶠ (i : True), f i = f trivial
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α}
  {g : k ∈ Std.TreeMap.Raw.filterMap f t} (h : t.WF), (Std.TreeMap.Raw.filterMap f t)[k] = (f k t[k]).get ⋯
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- The induced linear map on the quotients mod `I • ⊤`.  -/
LinearMap.reduceModIdeal : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_3} →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (M →ₗ[R] N) → M ⧸ I • ⊤ →ₗ[R ⧸ I] N ⧸ I • ⊤
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddGroup A] →
          [inst_3 : StarAddMonoid A] → [inst_4 : SMul R A] → [StarModule R A] → SMul R ↥(selfAdjoint A)
-- Mathlib.Algebra.Field.Defs
Field.toCommRing : {K : Type u} → [self : Field K] → CommRing K
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (fallback : β k),
  Std.DTreeMap.Internal.Impl.leaf.getD k fallback = fallback
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsAddApply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsAddApply (TestFunction Ω F n) E F
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given a type `M` with a multiplication, a congruence relation `c` on `M`, and elements of `M`
`x, y`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`.  -/
Con.instMembershipProd : {M : Type u_1} → [inst : Mul M] → Membership (M × M) (Con M)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instNormal : ∀ {G : Type u_1} [inst : Group G] (H : FiniteIndexNormalSubgroup G), H.Normal
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams : Type
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the forward direction of `sbtw_comm`. -/
Sbtw.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Sbtw R x y z → Sbtw R z y x
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsSupportedOutside.exactAt : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'}, K.IsSupportedOutside e → ∀ (i : ι), K.ExactAt (e.f i)
-- Mathlib.Data.Finset.Defs
Finset.mem_def : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ s ↔ a ∈ s.val
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq : ∀ (v : (r : ℕ) × ↑(EisensteinSeries.gammaSet 1 r 0)), EisensteinSeries.gammaSetDivGcdSigmaEquiv.symm v = ↑v.snd
-- Lean.Meta.AppBuilder
/-- Similar to `mkEqTrans`, but arguments can be `none`.
`none` is treated as a reflexivity proof.
 -/
Lean.Meta.mkEqTrans? : Option Lean.Expr → Option Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.coe_fract_self : ∀ {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : FloorRing K] [inst_4 : Fintype ι] [inst_5 : Unique ι] (k : K),
  ZSpan.fract (Module.Basis.singleton ι K) k = Int.fract k
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.one_lt_rpow : ∀ {x : NNReal} {z : ℝ}, 1 < x → 0 < z → 1 < x ^ z
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Icc_atTop_atTop : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Icc Filter.atTop Filter.atTop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux : Type → Type
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Monad for the definitional simplifier, layered on top of `SymM`.  -/
Lean.Meta.Sym.DSimp.DSimpM : Type → Type
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- If a space is locally path-connected, the topology of its path components is discrete.  -/
instDiscreteTopologyZerothHomotopy : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X], DiscreteTopology (ZerothHomotopy X)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.ofRaw.injEq : ∀ (val val_1 : ℕ), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- `F(S) / F` is an algebraic extension if and only if all elements of `S` are
algebraic elements.  -/
IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  Algebra.IsAlgebraic F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_injective_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Function.Injective (Polynomial.map f) ↔ Function.Injective ⇑f