mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.mk.injEq : ∀ (self next root congr : Lean.Expr) (target? proof? : Option Lean.Expr) (flipped : Bool) (size : ℕ)
  (interpreted ctor hasLambdas heqProofs : Bool) (idx generation mt : ℕ) (sTerms : Lean.Meta.Grind.SolverTerms)
  (funCC : Bool) (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource) (self_1 next_1 root_1 congr_1 : Lean.Expr)
  (target?_1 proof?_1 : Option Lean.Expr) (flipped_1 : Bool) (size_1 : ℕ)
  (interpreted_1 ctor_1 hasLambdas_1 heqProofs_1 : Bool) (idx_1 generation_1 mt_1 : ℕ)
  (sTerms_1 : Lean.Meta.Grind.SolverTerms) (funCC_1 : Bool) (ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource),
  ({ self := self, next := next, root := root, congr := congr, target? := target?, proof? := proof?, flipped := flipped,
        size := size, interpreted := interpreted, ctor := ctor, hasLambdas := hasLambdas, heqProofs := heqProofs,
        idx := idx, generation := generation, mt := mt, sTerms := sTerms, funCC := funCC,
        ematchDiagSource := ematchDiagSource } =
      { self := self_1, next := next_1, root := root_1, congr := congr_1, target? := target?_1, proof? := proof?_1,
        flipped := flipped_1, size := size_1, interpreted := interpreted_1, ctor := ctor_1, hasLambdas := hasLambdas_1,
        heqProofs := heqProofs_1, idx := idx_1, generation := generation_1, mt := mt_1, sTerms := sTerms_1,
        funCC := funCC_1, ematchDiagSource := ematchDiagSource_1 }) =
    (self = self_1 ∧
      next = next_1 ∧
        root = root_1 ∧
          congr = congr_1 ∧
            target? = target?_1 ∧
              proof? = proof?_1 ∧
                flipped = flipped_1 ∧
                  size = size_1 ∧
                    interpreted = interpreted_1 ∧
                      ctor = ctor_1 ∧
                        hasLambdas = hasLambdas_1 ∧
                          heqProofs = heqProofs_1 ∧
                            idx = idx_1 ∧
                              generation = generation_1 ∧
                                mt = mt_1 ∧ sTerms = sTerms_1 ∧ funCC = funCC_1 ∧ ematchDiagSource = ematchDiagSource_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.tail.reverse = p.reverse.dropLast.copy ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A block diagonal matrix whose components are all equal is Hermitian if
and only if each block is Hermitian.  -/
Matrix.isHermitian_blockDiagonal_iff : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n]
  {M : n → Matrix m m α}, (Matrix.blockDiagonal M).IsHermitian ↔ ∀ (i : n), (M i).IsHermitian
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg_of_neg_of_nonpos`.  -/
Right.add_neg_of_neg_of_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b : α},
  a < 0 → b ≤ 0 → a + b < 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceAnd : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_top_subsingleton : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (a : α) [inst_2 : Decidable (a = ⊥)], (↑⊤.parts).Subsingleton
-- Std.Data.TreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.get : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → (a : α) → a ∈ t → β
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `i`th coefficient is `0` for all `i < n`.  -/
PowerSeries.nat_le_order : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ), (∀ i < n, (PowerSeries.coeff i) φ = 0) → ↑n ≤ φ.order
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.one.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} [inst_1 : SizeOf J],
  sizeOf MonCat.Colimits.Prequotient.one = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_ofList_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.ExtDTreeMap.ofList l cmp).size ≤ l.length
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), (X.kernelSequenceOpcycles f g fg h n).X₁ = X.opcycles f g n
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_zero : ∀ {w : ℕ} {x : BitVec w}, x.sshiftRight 0 = x
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.find?_eq_none_iff : ∀ {ρ : Type} (pat : ρ) {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] [inst_2 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_4 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice}, s.find? pat = none ↔ s.contains pat = false
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.option : Lean.Syntax → Lean.Elab.CompletionInfo
-- Mathlib.Algebra.Group.Subgroup.Ker
MulEquiv.range_eq_top : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G'), (↑e).range = ⊤
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstSMul G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
        (∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g • e = e) →
          IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})
-- Mathlib.Order.Lattice
/-- The partial orders from `SemilatticeSup_mk'` and `SemilatticeInf_mk'` agree
if `sup` and `inf` satisfy the lattice absorption laws `sup_inf_self` (`a ⊔ a ⊓ b = a`)
and `inf_sup_self` (`a ⊓ (a ⊔ b) = a`).  -/
semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder : ∀ {α : Type u_1} [inst : Max α] [inst_1 : Min α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a)
  (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (sup_idem : ∀ (a : α), a ⊔ a = a)
  (inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a) (inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c))
  (inf_idem : ∀ (a : α), a ⊓ a = a),
  (∀ (a b : α), a ⊔ a ⊓ b = a) →
    (∀ (a b : α), a ⊓ (a ⊔ b) = a) →
      (SemilatticeSup.mk' sup_comm sup_assoc sup_idem).toPartialOrder =
        (SemilatticeInf.mk' inf_comm inf_assoc inf_idem).toPartialOrder
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
maximalIdeal_isPrincipal_of_isDedekindDomain : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsDedekindDomain R],
  Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₂).isEmpty = true → (↑(m₁.inter m₂)).isEmpty = true
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_isSymm : ∀ (n : ℕ), (CartanMatrix.D n).IsSymm
-- Mathlib.Algebra.GradedMulAction
SetLike.IsHomogeneousElem.graded_smul : ∀ {ιA : Type u_1} {ιB : Type u_2} {S : Type u_4} {R : Type u_5} {N : Type u_6} {M : Type u_7} [inst : SetLike S R]
  [inst_1 : SetLike N M] [inst_2 : VAdd ιA ιB] [inst_3 : SMul R M] {A : ιA → S} {B : ιB → N} [SetLike.GradedSMul A B]
  {a : R} {b : M}, SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem B b → SetLike.IsHomogeneousElem B (a • b)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.dist_le_of_fixedPoint : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ (x : α) {y : α}, Function.IsFixedPt f y → dist x y ≤ dist x (f x) / (1 - ↑K)
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- A variant of `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver` with the arguments in the
fiber products flipped.  -/
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ComonToMonOpOpObj_mon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), CategoryTheory.MonObj.one = CategoryTheory.ComonObj.counit.op
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.mk.inj : ∀ {type : Lean.Lsp.MessageType} {message : String} {actions? : Option (Array Lean.Lsp.MessageActionItem)}
  {type_1 : Lean.Lsp.MessageType} {message_1 : String} {actions?_1 : Option (Array Lean.Lsp.MessageActionItem)},
  { type := type, message := message, actions? := actions? } =
      { type := type_1, message := message_1, actions? := actions?_1 } →
    type = type_1 ∧ message = message_1 ∧ actions? = actions?_1
-- Std.Http.Protocol.H1
/-- A single body chunk produced by a pull-driven read.
 -/
Std.Http.Protocol.H1.PulledChunk : Type
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight_cons : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V}
  (p : Quiver.Path a b) (e : b ⟶ c),
  Quiver.Path.weight (fun {i j} => w) (p.cons e) = Quiver.Path.weight (fun {i j} => w) p * w e
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type v₂} {X : α → C} {B : C} (π : (a : α) → X a ⟶ B)
  [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] (a b : α), CategoryTheory.Limits.HasPullback (π a) (π b)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.principal_prod : ∀ {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} (sa : Set α),
  lb.HasBasis pb sb → (Filter.principal sa ×ˢ lb).HasBasis pb fun x => sa ×ˢ sb x
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_vcomp : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  (η.vcomp θ).mk = CategoryTheory.CategoryStruct.comp η.mk θ.mk
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Finset α` on `Finset β`.  -/
Finset.mulAction : {α : Type u_2} →
  {β : Type u_3} →
    [DecidableEq β] → [inst : DecidableEq α] → [inst_1 : Monoid α] → [MulAction α β] → MulAction (Finset α) (Finset β)
-- Mathlib.Data.Num.ZNum
ZNum.ofInt'.eq_1 : ∀ (n : ℕ), ZNum.ofInt' (Int.ofNat n) = (Num.ofNat' n).toZNum
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_smul_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {V : (x : M') → TangentSpace I' x} {g : M' → 𝕜},
  VectorField.mpullbackWithin I I' f (g • V) s x = g (f x) • VectorField.mpullbackWithin I I' f V s x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.comap_mulValuation_eq_int_padicValuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Valuation.comap (Int.castRingHom ℚ_[p]) Padic.mulValuation = Int.padicValuation p
-- Batteries.Lean.Meta.Basic
/-- Obtain all unassigned metavariables. If `includeDelayed` is `true`,
delayed-assigned metavariables are considered unassigned.
 -/
Lean.Meta.getUnassignedExprMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → optParam Bool false → m (Array Lean.MVarId)
-- Init.Data.Ord.Basic
Ordering.isEq_eq_false : ∀ {o : Ordering}, o.isEq = false ↔ ¬o = Ordering.eq
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.comp_ofBijective_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (hf : Function.Bijective ⇑f), f.comp ↑(RingEquiv.ofBijective f hf).symm = NonUnitalRingHom.id S
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isSubInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.CatCenter.localization 0 L W = 0
-- Mathlib.GroupTheory.PGroup
IsPGroup.map : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
  IsPGroup p ↥H → ∀ {K : Type u_2} [inst_1 : Group K] (ϕ : G →* K), IsPGroup p ↥(Subgroup.map ϕ H)
-- Mathlib.Probability.Kernel.Composition.CompNotation
MeasureTheory.Measure.comp_apply_univ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsMarkovKernel κ], (μ.bind ⇑κ) Set.univ = μ Set.univ
-- Std.Time.DateTime
/-- Subtract `Year.Offset` from a `DateTime`, clipping to the last valid day.
 -/
Std.Time.DateTime.subYearsClip : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.kernel_hull : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α},
  PrimitiveSpectrum.OrderGenerates T → ∀ (a : α), PrimitiveSpectrum.kernel (PrimitiveSpectrum.hull T a) = a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.toList_sorted : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBTree.RBMap α β cmp},
  List.Pairwise (RBTree.RBNode.cmpLT fun x1 x2 => cmp x1.1 x2.1) t.toList
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.impImpSimp.inj : ∀ {x : Lean.Name} {p : Mathlib.Tactic.ITauto.Proof} {x_1 : Lean.Name} {p_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.impImpSimp x p = Mathlib.Tactic.ITauto.Proof.impImpSimp x_1 p_1 → x = x_1 ∧ p = p_1
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
/-- Let `A` be an `R`-algebra. If `A ⧸ I` is finite free over `R`,
then the image of `Z(I) ∩ D(f) ⊆ Spec S` in `Spec R` is compact open.  -/
PrimeSpectrum.exists_image_comap_of_finite_of_free : ∀ {R : Type u_2} {A : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (f : A) (s : Set A)
  [Module.Finite R (A ⧸ Ideal.span s)] [Module.Free R (A ⧸ Ideal.span s)],
  ∃ t,
    PrimeSpectrum.comap (algebraMap R A) '' (PrimeSpectrum.zeroLocus s \ PrimeSpectrum.zeroLocus {f}) =
      (PrimeSpectrum.zeroLocus ↑t)ᶜ
-- Mathlib.Order.Category.BddOrd
BddOrd.dualEquiv_functor : BddOrd.dualEquiv.functor = BddOrd.dual
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.contains k t = true ↔ k ∈ t
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.endsWith pat = true
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instOrderTop.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instOrderTop = { toTop := OpenAddSubgroup.instTop, le_top := ⋯ }
-- Init.Data.Vector.MapIdx
Vector.mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n} {k : ℕ}, x ∈ xs.zipIdx k ↔ k ≤ x.2 ∧ xs[x.2 - k]? = some x.1
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.ofHom_eq : ∀ {X Y : Type u} (f : X ⟶ Y), TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f) = f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_toList : ∀ {M : Type u_7} [inst : AddCommMonoid M] (s : Finset M), s.toList.sum = ∑ x ∈ s, x
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instNegOffset : Neg Std.Time.Hour.Offset
-- Mathlib.RingTheory.Adjoin.Dimension
/-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are
free `R`-algebras, then the `Module.finrank` of the rank of the subalgebra generated by `A` and `B`
over `R` is less than or equal to the product of that of `A` and `B`.  -/
Subalgebra.finrank_sup_le_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [StrongRankCondition R] [inst_2 : CommRing S] [inst_3 : Algebra R S]
  (A B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B],
  Module.finrank R ↥(A ⊔ B) ≤ Module.finrank R ↥A * Module.finrank R ↥B
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getElem!_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getElem!_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  [inst_3 : Inhabited γ] {f : α → β → Option γ} {k : α},
  m.WF → (Std.HashMap.Raw.filterMap f m)[k]! = (m[k]?.bind (f k)).get!
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSigmaEquiv.eq_1 : ∀ {α : Type u_9} (p : α → Type v) (q : α → Prop),
  Equiv.subtypeSigmaEquiv p q =
    { toFun := fun x => ⟨⟨(↑x).fst, ⋯⟩, (↑x).snd⟩, invFun := fun x => ⟨⟨↑x.fst, x.snd⟩, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.CategoryTheory.Action.Monoidal
Action.β_inv_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] [inst_3 : CategoryTheory.BraidedCategory V] {X Y : Action V G},
  (β_ X Y).inv.hom = (β_ X.V Y.V).inv
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instReprOrdinal : Repr Std.Time.Minute.Ordinal
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (toFun : α → β) (injective : Function.Injective toFun)
  (succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a))
  (succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a))
  (toFun_1 : α → β) (injective_1 : Function.Injective toFun_1)
  (succ?_toFun_1 : ∀ (a : α), Std.PRange.succ? (toFun_1 a) = Option.map toFun_1 (Std.PRange.succ? a))
  (succMany?_toFun_1 :
    ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun_1 a) = Option.map toFun_1 (Std.PRange.succMany? n a)),
  ({ toFun := toFun, injective := injective, succ?_toFun := succ?_toFun, succMany?_toFun := succMany?_toFun } =
      { toFun := toFun_1, injective := injective_1, succ?_toFun := succ?_toFun_1,
        succMany?_toFun := succMany?_toFun_1 }) =
    (toFun = toFun_1)
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.isToken : String.Pos.Raw → String.Pos.Raw → Option Lean.Parser.Token → Bool
-- Init.Data.Array.Int
Array.prod_eq_foldl_int : ∀ {xs : Array ℤ}, xs.prod = Array.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x x_1 : C) (x_2 : D),
  (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D) x
            x_1).unmop.app
      x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2).inv
-- Mathlib.Data.EReal.Inv
EReal.sign_coe : ∀ (x : ℝ), SignType.sign ↑x = SignType.sign x
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.continuousSMul : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] (s : Subsemiring R) (X : Type u_2)
  [inst_2 : TopologicalSpace X] [inst_3 : MulAction R X] [ContinuousSMul R X], ContinuousSMul (↥s) X
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termB' : Lean.ParserDescr
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_zero : nhds 0 = ⨅ a, ⨅ (_ : a ≠ 0), Filter.principal (Set.Iio a)
-- Mathlib.Order.Filter.Bases.Basic
/-- `IsBasis p s` means the image of `s` bounded by `p` is a filter basis.  -/
Filter.IsBasis : {α : Type u_1} → {ι : Sort u_4} → (ι → Prop) → (ι → Set α) → Prop
-- Mathlib.NumberTheory.NumberField.DedekindZeta
/-- The value of the residue at `s = 1` of the Dedekind zeta function, see
`NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT`.
 -/
NumberField.dedekindZeta_residue : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℝ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.not_subset_of_mem : ∀ {x y : ZFSet.{u_1}}, x ∈ y → ¬y ⊆ x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLeftReflectLT : ∀ {α : Type u} [inst : Add α] [inst_1 : LT α] [AddLeftReflectLT α], AddLeftReflectLT (WithBot α)
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.one_le_dist_of_ne : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] {i j : ι},
  i ≠ j → ∀ (x : E i) (y : E j), 1 ≤ dist ⟨i, x⟩ ⟨j, y⟩
-- Init.Data.Option.Lemmas
Option.beq_none : ∀ {α : Type u_1} [inst : BEq α] {o : Option α}, (o == none) = o.isNone
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_add_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)] (w : ι → ℝ)
  (f₁ f₂ g : (i : ι) → E i), ⟪f₁ + f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + ⟪f₂, g⟫_[𝕜, w]
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.isNatEquiv_piEquivSucc : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [inst_1 : SuccOrder ι]
  {equiv : (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j} {e : F (Order.succ i) ≃ F i × X i} (hi : ¬IsMax i)
  [InverseSystem f],
  (∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x) →
    InverseSystem.IsNatEquiv f equiv → InverseSystem.IsNatEquiv f (InverseSystem.piEquivSucc equiv e hi)