mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₂_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₂.Rel i₂ (c₂.next i₂) → HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
-- Lean.DocString.Types
Lean.Doc.Inline.linebreak.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (string : String), sizeOf (Lean.Doc.Inline.linebreak string) = 1 + sizeOf string
-- Mathlib.Topology.UniformSpace.Defs
/-- Replace topology in a `UniformSpace` instance with a propositionally (but possibly not
definitionally) equal one.  -/
UniformSpace.replaceTopology : {α : Type u_2} → [i : TopologicalSpace α] → (u : UniformSpace α) → i = u.toTopologicalSpace → UniformSpace α
-- Mathlib.Algebra.RingQuot
RingQuot.mk.injEq : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} (toQuot toQuot_1 : Quot (RingQuot.Rel r)),
  ({ toQuot := toQuot } = { toQuot := toQuot_1 }) = (toQuot = toQuot_1)
-- Mathlib.Order.Max
Subsingleton.isMax : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α] (a : α), IsMax a
-- Mathlib.Logic.Function.Defs
Function.IsFixedPt.decidable : {α : Type u₁} → [h : DecidableEq α] → {f : α → α} → {x : α} → Decidable (Function.IsFixedPt f x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- A commutative additive group object is a commutative additive group object in the
category of additive group objects.  -/
CategoryTheory.AddGrp.instIsCommAddMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X], CategoryTheory.IsCommAddMonObj H
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app : ∀ {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_2, u_2} A']
  [inst_1 : CategoryTheory.Category.{v_3, u_3} B] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'}
  {e' : A' ≌ B'} (X : B), AlgebraicTopology.DoldKan.Compatibility.τ₀.hom.app X = e'.counitIso.hom.app (eB.functor.obj X)
-- Init.Prelude
/-- A numerical name. This kind of name is used, for example, to create hierarchical names for
free variables and metavariables. The identifier `_uniq.231` is represented as
```lean
.num (.str .anonymous "_uniq") 231
```
 -/
Lean.Name.num : Lean.Name → ℕ → Lean.Name
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  [inst_4 : SizeOf N] [inst_5 : SizeOf E] [inst_6 : SizeOf G] [inst_7 : SizeOf E'] (toAddEquiv : E ≃+ E')
  (inl_comm : ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl) (rightHom_comm : ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom),
  sizeOf { toAddEquiv := toAddEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
    1 + sizeOf toAddEquiv + sizeOf inl_comm + sizeOf rightHom_comm
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.hasBasis_nhds_zero : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F],
  (nhds 0).HasBasis (fun SV => Bornology.IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ nhds 0) fun SV => {f | Set.MapsTo (⇑f) SV.1 SV.2}
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist_self : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x : X ⊕ Y), Metric.glueDist Φ Ψ ε x x = 0
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] (m : M),
  Continuous fun x => x + m
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newHyp : Lean.FVarId → Lean.Meta.Grind.Goal → Lean.Meta.Grind.IntroResult✝
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {n : ℕ}
  {m : M}, DividedPowerAlgebra.dp R n (r • m) = r ^ n • DividedPowerAlgebra.dp R n m
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_eq_zero : ∀ {α : Type u_1} {a : FreeMonoid α}, a.length = 0 ↔ a = 1
-- Mathlib.Analysis.Convex.Body
ConvexBody.mk.injEq : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] (carrier : Set V)
  (convex' : Convex ℝ carrier) (isCompact' : IsCompact carrier) (nonempty' : carrier.Nonempty) (carrier_1 : Set V)
  (convex'_1 : Convex ℝ carrier_1) (isCompact'_1 : IsCompact carrier_1) (nonempty'_1 : carrier_1.Nonempty),
  ({ carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' } =
      { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedVAdd.vadd_le_vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : Preorder P] [inst_2 : VAdd G P] [IsOrderedVAdd G P] {a b : G}
  {c d : P}, a ≤ b → c ≤ d → a +ᵥ c ≤ b +ᵥ d
-- Mathlib.Order.SupClosed
isGLB_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α} {a : α}, IsGLB (infClosure s) a ↔ IsGLB s a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_iff_forall_mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.Equiv t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂
-- Mathlib.Algebra.Group.Action.Defs
SemiconjBy.smul_left : ∀ {M : Type u_1} {α : Type u_5} [inst : SMul M α] [inst_1 : Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
  {x a b : α}, SemiconjBy x a b → ∀ (r : M), SemiconjBy (r • x) a b
-- Batteries.Linter.UnnecessarySeqFocus
/-- Enables the 'unnecessary `<;>`' linter. This will warn whenever the `<;>` tactic combinator
is used when `;` would work.

```
example : True := by apply id <;> trivial
```
The `<;>` is unnecessary here because `apply id` only makes one subgoal.
Prefer `apply id; trivial` instead.

In some cases, the `<;>` is syntactically necessary because a single tactic is expected:
```
example : True := by
  cases () with apply id <;> apply id
  | unit => trivial
```
In this case, you should use parentheses, as in `(apply id; apply id)`:
```
example : True := by
  cases () with (apply id; apply id)
  | unit => trivial
```
 -/
Batteries.Linter.linter.unnecessarySeqFocus : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.Normalization
/-- The dominant morphism into the relative normalization.  -/
AlgebraicGeometry.Scheme.Hom.toNormalization : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] → X ⟶ AlgebraicGeometry.Scheme.Hom.normalization f
-- Mathlib.MeasureTheory.Measure.Support
Filter.HasBasis.notMem_measureSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Sort u_2}
  {p : ι → Prop} {s : ι → Set X} {x : X}, (nhds x).HasBasis p s → (x ∉ μ.support ↔ ∃ i, p i ∧ μ (s i) = 0)
-- Mathlib.FieldTheory.KummerExtension
/-- If `L/K` is a cyclic extension of degree `n`, and `K` contains all `n`-th roots of unity,
then `L = K[α]` for some `α ^ n ∈ K`.  -/
exists_root_adjoin_eq_top_of_isCyclic : ∀ (K : Type u) [inst : Field K] (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  (primitiveRoots (Module.finrank K L) K).Nonempty →
    ∀ [IsGalois K L] [IsCyclic Gal(L/K)], ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
spec_cfcₙAux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜), spectrum 𝕜 ((cfcₙAux ⋯ a ha) f) = Set.range ⇑f
-- Lean.Language.Basic
/-- Potentially reusable value.  -/
Lean.Language.SyntaxGuarded.val : {α : Type} → Lean.Language.SyntaxGuarded α → α
-- Batteries.Data.List.Basic
List.takeDTR.go.eq_def : ∀ {α : Type u_1} (dflt : α) (a : ℕ) (a_1 : List α) (a_2 : Array α),
  List.takeDTR.go dflt a a_1 a_2 =
    match a, a_1, a_2 with
    | n.succ, x :: xs, acc => List.takeDTR.go dflt n xs (acc.push x)
    | 0, x, acc => acc.toList
    | n, [], acc => acc.toListAppend (List.replicate n dflt)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.append.eq_def : ∀ {α : Type u_1} (x x_1 : RBTree.RBNode α),
  x.append x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, x => x
    | x, RBTree.RBNode.nil => x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d =>
      match b.append c with
      | RBTree.RBNode.node RBTree.RBColor.red b' z c' =>
        RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b') z
          (RBTree.RBNode.node RBTree.RBColor.red c' y d)
      | bc => RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red bc y d)
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d =>
      match b.append c with
      | RBTree.RBNode.node RBTree.RBColor.red b' z c' =>
        RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a x b') z
          (RBTree.RBNode.node RBTree.RBColor.black c' y d)
      | bc => a.balLeft x (RBTree.RBNode.node RBTree.RBColor.black bc y d)
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      RBTree.RBNode.node RBTree.RBColor.red (a.append b) x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      RBTree.RBNode.node RBTree.RBColor.red a x (b.append c)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_succ : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (n : ℕ),
  S.lowerCentralSeries (n + 1) = ⁅S.lowerCentralSeries n, S⁆
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_add : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c c' : ℕ → 𝕜),
  FormalMultilinearSeries.ofScalars E (c + c') =
    FormalMultilinearSeries.ofScalars E c + FormalMultilinearSeries.ofScalars E c'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app : ∀ (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_union_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  (mem : m₂.contains k = true), (m₁.union m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_ext_iff : ∀ {X Y : AddCommGrpCat} {f g : X ⟶ Y}, f = g ↔ AddCommGrpCat.Hom.hom f = AddCommGrpCat.Hom.hom g
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateLeft.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Tactic.BVDecide.BVUnOp.rotateLeft n) = 1 + sizeOf n
-- Mathlib.Order.Defs.Unbundled
IsEquiv.of_equivalence : ∀ {α : Sort u_1} {lt : α → α → Prop}, Equivalence lt → IsEquiv α lt
-- Mathlib.Data.List.Chain
/-- If `a` and `b` are related by the reflexive transitive closure of `r`, then there is an
`r`-chain starting from `a` and ending on `b`.
 -/
List.exists_isChain_cons_of_relationReflTransGen : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
  Relation.ReflTransGen r a b → ∃ l, List.IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
-- Init.Data.Int.Order
Int.mem_toNat? : ∀ {a : ℤ} {n : ℕ}, a.toNat? = some n ↔ a = ↑n
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Reinterprets `p : Submodule k V` as an `AffineSubspace k V`.  -/
Submodule.toAffineSubspace : {k : Type u_1} →
  {V : Type u_2} →
    [inst : Ring k] → [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → Submodule k V → AffineSubspace k V
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is continuously differentiable up to `n` on `s` if, for any point `x` in `s`, it
admits continuous derivatives up to order `n` on a neighborhood of `x` in `s`.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.

For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
For `n = ω`, we require the function to be analytic within `s` at every point of `s`. The precise
definition we give (all the derivatives should be analytic) is more involved to work around issues
when the space is not complete, but it is equivalent when the space is complete.
 -/
ContDiffOn : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → Set E → Prop
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.congr_preservesColimit : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  {F F' : CategoryTheory.Functor K J} (e : F ≅ F'),
  CategoryTheory.ObjectProperty.preservesColimit F = CategoryTheory.ObjectProperty.preservesColimit F'
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint : ∀ {σ : Type v} {X : AlgebraicGeometry.Scheme} {s : Set σ},
  s.Finite →
    ∀ {U : σ → X.Opens},
      (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (U i)) →
        s.Pairwise (Function.onFun Disjoint U) → AlgebraicGeometry.IsAffineOpen (⨆ i ∈ s, U i)
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.mk.inj : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {m : ℕ} {toEvalsTo : StateTransition.EvalsTo f a b}
  {steps_le_m : toEvalsTo.steps ≤ m} {toEvalsTo_1 : StateTransition.EvalsTo f a b}
  {steps_le_m_1 : toEvalsTo_1.steps ≤ m},
  { toEvalsTo := toEvalsTo, steps_le_m := steps_le_m } = { toEvalsTo := toEvalsTo_1, steps_le_m := steps_le_m_1 } →
    toEvalsTo = toEvalsTo_1
-- Batteries.Data.ByteArray
ByteArray.instDecidableEq_batteries : DecidableEq ByteArray
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instCompleteLattice.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.instCompleteLattice =
    { toSemilatticeSup := (completeLatticeOfInf (AddSubgroup G) ⋯).toSemilatticeSup, inf := fun x1 x2 => x1 ⊓ x2,
      inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯, toSupSet := (completeLatticeOfInf (AddSubgroup G) ⋯).toSupSet,
      isLUB_sSup := ⋯, toInfSet := (completeLatticeOfInf (AddSubgroup G) ⋯).toInfSet, isGLB_sInf := ⋯,
      toTop := AddSubgroup.instTop, le_top := ⋯, toBot := AddSubgroup.instBot, bot_le := ⋯ }
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is upper hemicontinuous at `x` if, whenever `t` is a neighborhood of
`f x`, then `t` is a neighborhood of `f x'` for all `x'` sufficiently close to `x`.  -/
UpperHemicontinuousAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → α → Prop
-- Mathlib.GroupTheory.Complement
Subgroup.not_isComplement_empty_left : ∀ {G : Type u_1} [inst : Group G] {T : Set G}, ¬Subgroup.IsComplement ∅ T
-- Mathlib.Data.Set.Pairwise.Basic
/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
disjoint iff `f` is injective .  -/
Set.pairwiseDisjoint_image_left_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
  (∀ b ∈ t, Function.Injective fun a => f a b) →
    ((t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t))
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.commutes_symm' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : TruncatedWittVector p m (ZMod p)),
  (TruncatedWittVector.zmodEquivTrunc p n).symm ((TruncatedWittVector.truncate hm) x) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))) ((TruncatedWittVector.zmodEquivTrunc p m).symm x)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkGENat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyGE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyGE n], L.IsStrictlyGE n
-- Mathlib.Order.Completion
DedekindCut.principal_sSup_left : ∀ {α : Type u_1} [inst : CompleteLattice α] (A : DedekindCut α), DedekindCut.principal (sSup A.left) = A
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.map₂_coe_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{u_1, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ]
  (pkg'' : AbstractCompletion.{vγ, uγ} γ) (a : α) (b : β) (f : α → β → γ),
  UniformContinuous₂ f → pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)
-- Mathlib.RingTheory.Binomial
Ring.multichoose_neg_self : ∀ (n : ℕ), Ring.multichoose (-↑n) n = (-1) ^ n
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_neg : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f : ρ.IntertwiningMap σ), Rep.ofHom (-f) = -Rep.ofHom f
-- Lean.Meta.Tactic.ElimInfo
/-- Information about an eliminator as used by `induction` or `cases`.

Created from an expression by `getElimInfo`. This typically contains level metavariables that
are instantiated as we go (e.g. in `addImplicitTargets`), so this is single use.
 -/
Lean.Meta.ElimInfo : Type
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_pos_iff_mem_support : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (p : PrimeSpectrum R), 0 < Module.rankAtStalk M p ↔ p ∈ Module.support R M
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_mul_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : AddCommMonoid α] [inst_3 : Mul α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α)
  (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p), M.submatrix e₁ ⇑e₂ * N.submatrix (⇑e₂) e₃ = (M * N).submatrix e₁ e₃
-- Mathlib.Data.Complex.Basic
Complex.ofReal_inv : ∀ (r : ℝ), ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.Data.Fintype.EquivFin
/-- A constructive embedding of a fintype `α` in another fintype `β` when `card α ≤ card β`.  -/
Function.Embedding.truncOfCardLE : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] → [DecidableEq α] → [DecidableEq β] → Fintype.card α ≤ Fintype.card β → Trunc (α ↪ β)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- The partial application of a constant to a covariant operator is monotone.  -/
Covariant.monotone_of_const : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} [inst : Preorder N] [CovariantClass M N μ fun x1 x2 => x1 ≤ x2] (m : M),
  Monotone (μ m)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : N ≃+ P}
  {j : P ≃+ Q},
  (f.ofAddEquivOfLocalizations (k.trans j)).toAddMonoidHom =
    j.toAddMonoidHom.comp (f.ofAddEquivOfLocalizations k).toAddMonoidHom
-- Mathlib.RingTheory.PowerSeries.GaussNorm
/-- We say `f` HasGaussNorm if the values `v (coeff t f) * c ^ t` is bounded above, that is
`gaussNormC f` is finite.  -/
PowerSeries.HasGaussNorm : {R : Type u_1} → [Semiring R] → (R → ℝ) → ℝ → PowerSeries R → Prop
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resIndAdjunction_homEquiv_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S)
  {B : Rep.{max w u v, u, v} k G} (f : Rep.res S.subtype B ⟶ A),
  ((Rep.resIndAdjunction k S).homEquiv B A) f =
    CategoryTheory.CategoryStruct.comp ((Rep.resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f) A.indCoindIso.inv
-- Mathlib.Analysis.Convex.Cone.Basic
_private.Mathlib.Analysis.Convex.Cone.Basic.0.ConvexCone.isOpen_hull : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : AddCommMonoid E] →
      [inst_1 : TopologicalSpace E] →
        [inst_2 : Semifield 𝕜] →
          [inst_3 : LinearOrder 𝕜] →
            [inst_4 : Module 𝕜 E] → {s : Set E} → IsOpen s → ProofWanted (IsOpen ↑(ConvexCone.hull 𝕜 s))
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root element in the equivalence class of `e` IF `e` has been internalized.  -/
Lean.Meta.Grind.getRoot? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Lean.Meta.Tactic.Grind.Action
/-- If tracing is enabled and continuation produced `.closed [t₁, ..., tₙ]`,
returns the singleton sequence `[t]` where `t` is
```
· t₁
  ...
  tₙ
```
 -/
Lean.Meta.Grind.Action.group : Lean.Meta.Grind.Action
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.State.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)), sizeOf { map := map } = 1 + sizeOf map