mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_comap : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : AddGroup N]
  [inst_3 : TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f),
  ↑(OpenAddSubgroup.comap f hf H) = AddSubgroup.comap f ↑H
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, a ∉ m → m.getKey! a = default
-- Mathlib.Data.Fin.Tuple.Basic
/-- Define a function on `Fin (n + 1)` from a value on `i : Fin (n + 1)` and values on each
`Fin.succAbove i j`, `j : Fin n`. This version is elaborated as eliminator and works for
propositions, see also `Fin.insertNth` for a version without an `@[elab_as_elim]`
attribute.  -/
Fin.succAboveCases : {n : ℕ} →
  {α : Fin (n + 1) → Sort u} → (i : Fin (n + 1)) → α i → ((j : Fin n) → α (i.succAbove j)) → (j : Fin (n + 1)) → α j
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- Rotating triangles three times identifies with the shift by `1`.  -/
CategoryTheory.Pretriangulated.rotateRotateRotateIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        (CategoryTheory.Pretriangulated.rotate C).comp
            ((CategoryTheory.Pretriangulated.rotate C).comp (CategoryTheory.Pretriangulated.rotate C)) ≅
          CategoryTheory.Pretriangulated.Triangle.shiftFunctor C 1
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A σ-compact space is a space that is the union of a countable collection of compact subspaces.
Note that a locally compact separable T₂ space need not be σ-compact.
The sequence can be extracted using `compactCovering`.  -/
SigmaCompactSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Mathlib.Logic.Function.Defs
Function.map_comp_diag : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ), Prod.map f g ∘ Function.diag = Function.prod f g
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ}
  (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯)))
  (j : Fin (n + 1)),
  (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).incl.app j =
    F.map ((Fin.isTerminalLast n).from j)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_lt_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m : ι}, ∀ i ≤ m, MeasureTheory.hittingBtwn u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
-- Lean.Data.Lsp.Internal
/-- Information about a single import statement.  -/
Lean.Lsp.ImportInfo : Type
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the next element in the equivalence class of `e`.  -/
Lean.Meta.Grind.Goal.getNext : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.Basic
IsAddUnit.mem_addSubmonoid_iff : ∀ {M : Type u_4} [inst : AddMonoid M] (a : M), a ∈ IsAddUnit.addSubmonoid M ↔ IsAddUnit a
-- Std.Data.ExtTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtTreeMap.getKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α → α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_eq_insertMany!_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h : t₁.Balanced),
  ↑(t₁.insertMany t₂ h) = ↑(t₁.insertMany! t₂)
-- Mathlib.NumberTheory.ModularForms.Identities
SlashInvariantForm.T_zpow_width_invariant : ∀ (N : ℕ) (k n : ℤ)
  (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)
  (z : UpperHalfPlane), f (ModularGroup.T ^ (↑N * n) • z) = f z
-- Init.PropLemmas
and_exists_self : ∀ (P : Prop) (Q : P → Prop), (P ∧ ∃ (p : P), Q p) ↔ ∃ (p : P), Q p
-- Mathlib.FieldTheory.Separable
Polynomial.separable_or : ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F},
  Irreducible f → f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (Polynomial.expand F p) g = f
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C)
  [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D)
  (g : (⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B),
  (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B) g =
    CategoryTheory.CategoryStruct.comp (⊥_ CategoryTheory.StructuredArrow A G).hom (G.map g)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If an affine subspace is nonempty and contained in another with the same direction, they are
equal.  -/
AffineSubspace.eq_of_direction_eq_of_nonempty_of_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁.direction = s₂.direction → (↑s₁).Nonempty → s₁ ≤ s₂ → s₁ = s₂
-- Init.Data.Vector.Lemmas
Vector.map_const_fun : ∀ {β : Type u_1} {n : ℕ} {α : Type u_2} {x : β}, Vector.map (Function.const α x) = fun x_1 => Vector.replicate n x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_keysArray_eq : ∀ {α : Type u} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keysArray = t₂.keysArray)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.SubsheafClosure.below.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))}
  {motive : (Z : C) → (a : F.obj (Opposite.op Z)) → K.SubsheafClosure 𝒮 Z a → Prop} {Z : C} {a : F.obj (Opposite.op Z)}
  (a_1 : a ∈ 𝒮 Z), CategoryTheory.Precoverage.SubsheafClosure.below ⋯
-- Init.Data.Vector.Lemmas
Vector.replace_append_left : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n m : ℕ} {a b : α} {xs : Vector α n} {ys : Vector α m},
  a ∈ xs → (xs ++ ys).replace a b = xs.replace a b ++ ys
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_le_inj : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₁ a₂ : α} {g : κ → α} (e : ι → κ),
  Function.Injective e → (∀ c ∉ Set.range e, 0 ≤ g c) → (∀ (i : ι), f i ≤ g (e i)) → HasSum f a₁ → HasSum g a₂ → a₁ ≤ a₂
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i : E.saturate.I₀),
  E.fromSaturateOfHasPullbacks.h₀ i = CategoryTheory.CategoryStruct.id (E.saturate.X i)
-- Mathlib.Tactic.NormNum.Result
/-- Helper function to synthesize a typed `Ring α` expression.  -/
Mathlib.Meta.NormNum.inferRing : {u : Lean.Level} → (α : Q(Type u)) → Lean.MetaM Q(Ring «$α»)
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.DoOpsRefPointed : NonemptyType
-- Mathlib.Order.Heyting.Basic
toDual_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), OrderDual.toDual (￢a) = (OrderDual.toDual a)ᶜ
-- Mathlib.Order.SuccPred.Basic
Order.le_iff_eq_or_le_pred : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α}, b ≤ a ↔ b = a ∨ b ≤ Order.pred a
-- Mathlib.Algebra.Lie.Ideal
LieHom.isIdealMorphism_iff : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'),
  f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofHasPullback_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_3 : CategoryTheory.Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)],
  (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G f₁ f₃).pt =
    CategoryTheory.Limits.pullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.halt.sizeOf_spec : sizeOf Turing.PartrecToTM2.Cont'.halt = 1
-- Mathlib.Geometry.Manifold.Notation
/-- Check if an expression `e` is a `ContinuousLinearMap` over an identity ring homomorphism where
the coefficient rings of the domain and codomain are reducibly definitionally equal. If so, we
return `(k, E, F)`, where `k` is the coefficient ring, `E` is the domain, and `F` is the codomain
of the continuous linear maps. Otherwise, we error.
Assumes that `e` is already in `whnf` and has had metavariables instantiated.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.isCLMReduciblyDefeqCoefficients : Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.div` -/
TendstoUniformlyOnFilter.fun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' →
      TendstoUniformlyOnFilter (fun i i_1 => f i i_1 / f' i i_1) (fun i => g i / g' i) l l'
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.sInter_of_countable : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {s : Set (Set α)},
  Order.cof α ≠ Cardinal.aleph0 → s.Countable → (∀ x ∈ s, IsClub x) → IsClub (⋂₀ s)
-- Mathlib.NumberTheory.Dioph
/-- A predicate asserting that a function is a multivariate integer polynomial.
(We are being a bit lazy here by allowing many representations for multiplication,
rather than only allowing monomials and addition, but the definition is equivalent
and this is easier to use.)  -/
IsPoly : {α : Type u_1} → ((α → ℕ) → ℤ) → Prop
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Ioi : ∀ (a : ℝ), UniqueDiffOn ℝ (Set.Ioi a)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_nnratCast : ∀ (q : ℚ≥0), ↑↑q = ↑q
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mk : {R : Type u} →
  [inst : Ring R] →
    [toAddGroupFilterBasis : AddGroupFilterBasis R] →
      (∀ {U : Set R}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V * V ⊆ U) →
        (∀ (x₀ : R) {U : Set R},
            U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ * x) ⁻¹' U) →
          (∀ (x₀ : R) {U : Set R},
              U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x * x₀) ⁻¹' U) →
            RingFilterBasis R
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instSubfieldClass : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  SubfieldClass (IntermediateField K L) L
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.add_bind : ∀ {α β : Type u} (f : α → FreeAddGroup β) (x y : FreeAddGroup α), x + y >>= f = (x >>= f) + (y >>= f)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Lax.LaxTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.truncation_zero : ∀ {α : Type u_1} (f : α → ℝ), ProbabilityTheory.truncation f 0 = 0
-- Lean.Declaration
Lean.InductiveVal.numTypeFormers : Lean.InductiveVal → ℕ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_comp_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y X X' B A : C} (p : X ⟶ Y) (p' : X' ⟶ X) (i : A ⟶ B)
  [CategoryTheory.HasLiftingProperty i p] [CategoryTheory.HasLiftingProperty i p'],
  CategoryTheory.HasLiftingProperty i (CategoryTheory.CategoryStruct.comp p' p)
-- Mathlib.Order.Filter.Prod
Filter.eventually_prod_principal_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {p : α × β → Prop} {s : Set β},
  (∀ᶠ (x : α × β) in f ×ˢ Filter.principal s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
-- Mathlib.Analysis.Complex.RealDeriv
/-- If a complex function `e` is differentiable at a real point, then the function `ℝ → ℝ` given by
the real part of `e` is also differentiable at this point, with a derivative equal to the real part
of the complex derivative.  -/
HasDerivAt.real_of_complex : ∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun x => (e ↑x).re) e'.re z
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_eq_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support = p.support.dropLast.concat v
-- Mathlib.RingTheory.Artinian.Module
/-- A reduced commutative Artinian ring is isomorphic to a finite product of fields,
namely the quotients by the maximal ideals.  -/
IsArtinianRing.equivPi : (R : Type u_1) →
  [inst : CommRing R] → [IsArtinianRing R] → [IsReduced R] → R ≃ₐ[R] (I : MaximalSpectrum R) → R ⧸ I.asIdeal
-- Mathlib.Data.Fintype.Basic
/-- Short-circuit instance to decrease search for `Unique.fintype`,
since that relies on a subsingleton elimination for `Unique`.  -/
Fintype.subtypeEq : {α : Type u_1} → (y : α) → Fintype { x // x = y }
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.setGoals : List Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Compactness.Compact
Function.compactSpace : ∀ {Y : Type v} {ι : Type u_1} [inst : TopologicalSpace Y] [CompactSpace Y], CompactSpace (ι → Y)
-- Std.Http.Protocol.H1.Writer
/-- All the data produced by the writer, ready to be sent to the socket.
 -/
Std.Http.Protocol.H1.Writer.outputData : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Internal.ChunkedBuffer
-- Mathlib.Data.FinEnum
FinEnum.card_Int16 : FinEnum.card Int16 = 2 ^ 16
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter m₂ ⋯) k fallback = fallback
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.im_neg : ∀ (z : Complex.UnitClosedDisc), (-z).im = -z.im
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J),
  c.toCostructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Opens.compl_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Opens α), s.compl.compl = s
-- Mathlib.Data.Set.Basic
Set.inter_isAssoc : ∀ {α : Type u}, Std.Associative fun x1 x2 => x1 ∩ x2
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pairwiseDisjoint_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [IsLeftCancelVAdd α β] {s : Set α} {t : Set β},
  (s.PairwiseDisjoint fun x => x +ᵥ t) ↔ Set.InjOn (fun p => p.1 +ᵥ p.2) (s ×ˢ t)
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.mk.inj : ∀ {year : Std.Time.Year.Offset} {month : Std.Time.Month.Ordinal} {day : Std.Time.Day.Ordinal}
  {valid : year.Valid month day} {year_1 : Std.Time.Year.Offset} {month_1 : Std.Time.Month.Ordinal}
  {day_1 : Std.Time.Day.Ordinal} {valid_1 : year_1.Valid month_1 day_1},
  { year := year, month := month, day := day, valid := valid } =
      { year := year_1, month := month_1, day := day_1, valid := valid_1 } →
    year = year_1 ∧ month = month_1 ∧ day = day_1
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_id : ∀ {α : Type u_1} (i : ℕ) (l : List α), l.modifyTailIdx i id = l
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The non-trivial symmetric braiding, sending $a \otimes b$ to
$(-1)^{\deg a' \deg b} (b \otimes a)$.  -/
GradedTensorProduct.comm : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] →
                                GradedTensorProduct R 𝒜 ℬ ≃ₐ[R] GradedTensorProduct R ℬ 𝒜
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_sup : ∀ {G : Type u_2} [inst : Group G] (S T : Submonoid G), (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_4 : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.l_hom x) =
    id
      (CategoryTheory.Discrete.natTrans fun x_1 =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.MonoidalCategoryStruct.tensorObj
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C))
                  x).normalizeObj'.obj
            x_1))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Morphisms for `WalkingMulticospan`.  -/
CategoryTheory.Limits.WalkingMulticospan.Hom : {J : CategoryTheory.Limits.MulticospanShape} →
  CategoryTheory.Limits.WalkingMulticospan J → CategoryTheory.Limits.WalkingMulticospan J → Type (max w w')
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.initGrindNorm : Lean.Parser.Parser
-- Mathlib.Computability.Encoding
Computability.inclusionBoolΓ'_injective : Function.Injective Computability.inclusionBoolΓ'
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [LocallyCompactSpace M], LocallyCompactSpace Mᵐᵒᵖ
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.resolveSimpIdTheorem? : Lean.Term → Lean.Elab.TermElabM Lean.Elab.Tactic.ResolveSimpIdResult
-- Mathlib.AlgebraicGeometry.Limits
/-- `Spec 0` is the initial object in the category of schemes.  -/
AlgebraicGeometry.specPUnitIsInitial : CategoryTheory.Limits.IsInitial (AlgebraicGeometry.Spec (CommRingCat.of PUnit.{u + 1}))
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_add : ∀ {p q : DyckWord}, (p + q).semilength = p.semilength + q.semilength
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.mk.inj : ∀ {nextIdx : ℕ} {lmap : Std.HashMap Lean.LMVarId Lean.Level} {emap : Std.HashMap Lean.MVarId Lean.Expr}
  {mctx : Lean.MetavarContext} {nextIdx_1 : ℕ} {lmap_1 : Std.HashMap Lean.LMVarId Lean.Level}
  {emap_1 : Std.HashMap Lean.MVarId Lean.Expr} {mctx_1 : Lean.MetavarContext},
  { nextIdx := nextIdx, lmap := lmap, emap := emap, mctx := mctx } =
      { nextIdx := nextIdx_1, lmap := lmap_1, emap := emap_1, mctx := mctx_1 } →
    nextIdx = nextIdx_1 ∧ lmap = lmap_1 ∧ emap = emap_1 ∧ mctx = mctx_1
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Any.eq_def : ∀ {α : Type u_1} (p : α → Prop) (x : RBTree.RBNode α),
  RBTree.RBNode.Any p x =
    match x with
    | RBTree.RBNode.nil => False
    | RBTree.RBNode.node c l v r => p v ∨ RBTree.RBNode.Any p l ∨ RBTree.RBNode.Any p r
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.instSmallCategoryI : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (P : CategoryTheory.Limits.IndObjectPresentation A) → CategoryTheory.SmallCategory P.I
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findM?_eq_findSomeM? : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [Std.Iterators.Finite α Id] {it : Std.Iter β} {f : β → m (ULift.{w, 0} Bool)},
  it.findM? f =
    it.findSomeM? fun x => do
      let __do_lift ← f x
      pure (if __do_lift.down = true then some x else none)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ f x * r` tends to infinity along a filter `l`
if and only if `f` tends to negative infinity along `l`.  -/
Filter.tendsto_mul_const_atTop_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (S : L.Substructure P) (g : L.Hom N P) (f : L.Hom M N),
  FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.comap g S) =
    FirstOrder.Language.Substructure.comap (g.comp f) S
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.inverseImage_trW_isInverted : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  {D : Type u_2} [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : CategoryTheory.Limits.HasZeroObject D] [inst_9 : CategoryTheory.HasShift D ℤ]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [inst_12 : F.CommShift ℤ] [F.IsTriangulated]
  [P.IsClosedUnderIsomorphisms] {E : Type u_4} [inst_15 : CategoryTheory.Category.{u_5, u_4} E]
  (L : CategoryTheory.Functor C E) [L.IsLocalization P.trW], (P.inverseImage F).trW.IsInvertedBy (F.comp L)
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_a_eq : ∀ (a b : ℕ+), a = a.gcdA' b * a.gcd b