mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {i : X ⟶ Y} {r : Y ⟶ X}
  {retract :
    autoParam (CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Retract.retract._autoParam}
  {i_1 : X ⟶ Y} {r_1 : Y ⟶ X}
  {retract_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 r_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Retract.retract._autoParam},
  { i := i, r := r, retract := retract } = { i := i_1, r := r_1, retract := retract_1 } → i = i_1 ∧ r = r_1
-- Init.Data.Vector.Algebra
Vector.zero_hmul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} [inst : Zero α] [Zero β] [inst_2 : Zero γ] [inst_3 : HMul α β γ],
  (∀ (c : β), 0 * c = 0) → ∀ (c : Vector β n), 0 * c = 0
-- Lean.Data.Json.Basic
Lean.Json.arr.sizeOf_spec : ∀ (elems : Array Lean.Json), sizeOf (Lean.Json.arr elems) = 1 + sizeOf elems
-- Batteries.Lean.EStateM
EStateM.run_seqLeft : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ),
  (x <* y).run s =
    match x.run s with
    | EStateM.Result.ok v s => EStateM.Result.map (fun x => v) (y.run s)
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_fun_def : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE), slope f = fun a b => (b - a)⁻¹ • (f b -ᵥ f a)
-- Lean.Widget.UserWidget
/-- An ESmodule that exports a react component to render.  -/
Lean.Widget.UserWidgetDefinition.javascript : Lean.Widget.UserWidgetDefinition → String
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f ≠ ∅ →
    ∀ {fallback : α},
      (Std.ExtDTreeMap.Const.alter t k f).minKeyD fallback = k ↔
        (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (s : S)
  (f : AdicCompletion I M), ↑(s • f) = s • ↑f
-- Init.PropLemmas
exists_and_left : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, b ∧ p x) ↔ b ∧ ∃ x, p x
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_univ : ∀ {α : Type u_1}, Nat.card ↑Set.univ = Nat.card α
-- Mathlib.Computability.TuringMachine.Computable
/-- the initial state of the machine  -/
Turing.FinTM2.initialState : (self : Turing.FinTM2) → self.σ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictFDerivAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.Normal.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] {φ : H ⟶ G},
  autoParam (CategoryTheory.Mono φ) CategoryTheory.IsAddMonHom.Normal.mono._autoParam →
    autoParam (CategoryTheory.IsAddMonHom φ) CategoryTheory.IsAddMonHom.Normal.isAddMonHom._autoParam →
      (∃ ψ,
          CategoryTheory.CategoryStruct.comp ψ φ =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
              (CategoryTheory.AddGrpObj.addConj G)) →
        CategoryTheory.IsAddMonHom.Normal φ
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.exists_isOpenCover_presentation : ∀ {X : AlgebraicGeometry.Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M],
  ∃ ι U x, TopologicalSpace.IsOpenCover U ∧ ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)
-- Init.SimpLemmas
Bool.or_true : ∀ (b : Bool), (b || true) = true
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_def : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithBot α),
  a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (fun x1 x2 => x1 * x2) a b
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasLimit K₁]
  [inst_7 : CategoryTheory.Limits.HasLimit K₂] (j : J₁ × J₂) {Z : C} (h : (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom
      (CategoryTheory.CategoryStruct.comp
        ((G.map (CategoryTheory.Limits.limit.π K₁ j.1)).app (CategoryTheory.Limits.limit K₂))
        (CategoryTheory.CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (CategoryTheory.Limits.limit.π K₂ j.2)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
      h
-- Batteries.Lean.PersistentHashSet
/-- Returns `true` if `f` returns `true` for all elements of the set.
 -/
Lean.PersistentHashSet.allM : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → {m : Type → Type u_2} → [Monad m] → Lean.PersistentHashSet α → (α → m Bool) → m Bool
-- Mathlib.Computability.Reduce
OneOneReducible.to_many_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  p ≤₁ q → p ≤₀ q
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.liftAlgHom.congr_simp : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [inst_1 : CommRing R]
  [inst_2 : CommRing A] [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f f_1 : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n)
  (e_f : f = f_1) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m),
  AdicCompletion.liftAlgHom I f hf = AdicCompletion.liftAlgHom I f_1 ⋯
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.nat_le_ofENat : ∀ {m : ℕ} {n : ℕ∞}, ↑m ≤ ↑n ↔ ↑m ≤ n
-- Mathlib.Order.Cofinal
GaloisConnection.isCofinal_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {g : α → β},
  GaloisConnection f g → IsCofinal (Set.range g)
-- Mathlib.Data.Set.Pointwise.Support
mulSupport_comp_inv_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : GroupWithZero α] [inst_1 : MulAction α β] [inst_2 : One γ]
  {c : α}, c ≠ 0 → ∀ (f : β → γ), (Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_zero : Cardinal.lift.{u_2, u_1} 0 = 0
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.continuation : String
-- Init.Data.List.Perm
List.Perm.filter : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Perm l₂ → (List.filter p l₁).Perm (List.filter p l₂)
-- Mathlib.Order.WellFoundedSet
Finset.partiallyWellOrderedOn_bUnion : ∀ {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : Finset ι) {f : ι → Set α},
  (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ_σ₀Iter'_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (m + j = n) SimplexCategory.δ_σ₀Iter'._auto_1),
  autoParam (j < ↑i) SimplexCategory.δ_σ₀Iter'._auto_3 →
    autoParam (↑i = ↑i' + j) SimplexCategory.δ_σ₀Iter'._auto_5 →
      ∀ {Z : SimplexCategory} (h_1 : { len := m + 1 } ⟶ Z),
        CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
            (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter j ⋯) h_1) =
          CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter j ⋯)
            (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i') h_1)
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.of_subsingleton_left : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Subsingleton α], Filter.EventuallyConst f l
-- Mathlib.Topology.Maps.Basic
IsClosedMap.isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → Continuous f → Function.Surjective f → Topology.IsQuotientMap f
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (g : β → α)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformly f g = TendstoLocallyUniformly (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.RingTheory.Idempotents
eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute : ∀ {R : Type u_1} [inst : Ring R] {e₁ e₂ : R},
  IsIdempotentElem e₁ → IsIdempotentElem e₂ → IsNilpotent (e₁ - e₂) → Commute e₁ e₂ → e₁ = e₂
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toNormedGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedCommGroup E],
  NormedCommGroup.toNormedGroup =
    { toNorm := inst.toNorm, toGroup := inst.toGroup, toMetricSpace := inst.toMetricSpace, dist_eq := ⋯ }
-- Lean.Exception
/-- Throw a "maximum recursion depth has been reached" exception using the given reference syntax.
 -/
Lean.throwMaxRecDepthAt : {m : Type → Type} → {α : Type} → [Lean.MonadError m] → Lean.Syntax → m α
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- All `x ∈ 𝓞[K]` can be written as `n / d` with `n : R` and `d ∈ v.asIdealᶜ`.  -/
IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1 → ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.targetAffineLocally_affineAnd_le : ∀ {Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f) →
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ≤
      AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => W)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β} {a : α},
  a ∈ s -ᵥ t ↔ ∃ b ∈ s, ∃ c ∈ t, b -ᵥ c = a
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.skyscraperPresheafHomEquiv.symm g) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.Limits.Pi.π (fun t => M) x)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.rangeS_le : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  (algebraMap R A).rangeS ≤ S.toSubsemiring
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- The `(n+1)`th convergent of `ξ` is the `n`th convergent of `1/(fract ξ)`.  -/
Real.convergent_succ : ∀ (ξ : ℝ) (n : ℕ), ξ.convergent (n + 1) = ↑⌊ξ⌋ + ((Int.fract ξ)⁻¹.convergent n)⁻¹
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.preimageMkEquivSubgroupProdSet.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (t : Set (α ⧸ s)),
  QuotientGroup.preimageMkEquivSubgroupProdSet s t =
    { toFun := fun a => (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩), invFun := fun a => ⟨Quotient.out ↑a.2 * ↑a.1, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Fintype.Quotient
Quotient.finChoice_eq : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (a : (i : ι) → α i), (Quotient.finChoice fun x => ⟦a x⟧) = ⟦a⟧
-- Mathlib.Algebra.Field.Defs
Semifield.mk : {K : Type u_2} →
  [toCommSemiring : CommSemiring K] →
    [toInv : Inv K] →
      [toDiv : Div K] →
        [toZPow : ZPow K] →
          autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : K), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial K] →
                    0⁻¹ = 0 →
                      (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                        [toNNRatCast : NNRatCast K] →
                          autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionSemiring.nnratCast_def._autoParam →
                            (nnqsmul : ℚ≥0 → K → K) →
                              autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                  DivisionSemiring.nnqsmul_def._autoParam →
                                Semifield K
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.match_1.eq_1 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C →
      (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C → Sort u_2)
  (a : C) (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
  (h_1 :
    (a : C) →
      (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X a : CategoryTheory.FreeMonoidalCategory C) →
      (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        motive (X.tensor a) n),
  (match CategoryTheory.FreeMonoidalCategory.of a, x with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor a, n => h_3 X a n) =
    h_1 a x
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for nonempty finite sums in additive
commutative groups with an ultrametric norm.  -/
IsUltrametricDist.norm_sum_le_of_forall_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι},
  s.Nonempty → ∀ {f : ι → M} {C : ℝ}, (∀ i ∈ s, ‖f i‖ ≤ C) → ‖∑ i ∈ s, f i‖ ≤ C
-- Mathlib.Logic.Equiv.Sum
Equiv.sumSumSumComm_symm : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12),
  (Equiv.sumSumSumComm α β γ δ).symm = Equiv.sumSumSumComm α γ β δ
-- Lean.Elab.DefView
Lean.Elab.DefParsed.mk.injEq : ∀ (fullHeaderRef : Lean.Syntax)
  (headerProcessedSnap : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot))
  (fullHeaderRef_1 : Lean.Syntax)
  (headerProcessedSnap_1 : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)),
  ({ fullHeaderRef := fullHeaderRef, headerProcessedSnap := headerProcessedSnap } =
      { fullHeaderRef := fullHeaderRef_1, headerProcessedSnap := headerProcessedSnap_1 }) =
    (fullHeaderRef = fullHeaderRef_1 ∧ headerProcessedSnap = headerProcessedSnap_1)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instBEqGCongrKey : BEq Mathlib.Tactic.GCongr.GCongrKey
-- Aesop.Nanos
Aesop.instOrdNanos.ord : Aesop.Nanos → Aesop.Nanos → Ordering
-- Init.Data.Array.Lex.Lemmas
Array.not_lt_iff_ge : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, ¬xs < ys ↔ ys ≤ xs
-- Mathlib.Algebra.Group.TypeTags.Basic
isRightRegular_toMul : ∀ {α : Type u} [inst : Monoid α] {a : Additive α}, IsRightRegular (Additive.toMul a) ↔ IsAddRightRegular a
-- Mathlib.Algebra.Order.Archimedean.Basic
OrderDual.instAddArchimedean : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] [Archimedean G],
  Archimedean Gᵒᵈ
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- Euler's Criterion: A unit `x` of `ZMod p` is a square if and only if `x ^ (p / 2) = 1`.  -/
ZMod.euler_criterion_units : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (x : (ZMod p)ˣ), (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toMonoidWithZeroHom : α →*₀ β)
  (monotone' : Monotone (↑toMonoidWithZeroHom).toFun),
  sizeOf { toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } = 1 + sizeOf toMonoidWithZeroHom
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_self_pos_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s : Finset α}, 0 < s.addEnergy s ↔ s.Nonempty
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The explicit coproduct cofan for `F : discrete ι ⥤ LocallyRingedSpace`.  -/
AlgebraicGeometry.LocallyRingedSpace.coproductCofan : {ι : Type v} →
  [Small.{u, v} ι] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace) →
      CategoryTheory.Limits.Cocone F
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∈ m → m.getKey? k = some k
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The embeddings of different blocks of a composition are disjoint.  -/
Composition.disjoint_range : ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
  i₁ ≠ i₂ → Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
-- Mathlib.Topology.Order
Continuous.coinduced_le : ∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β},
  Continuous f → TopologicalSpace.coinduced f t ≤ t'
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- `p` is in the image of `Spec S → Spec R` if and only if `p` extended to `S` and
restricted back to `R` is `p`.  -/
PrimeSpectrum.mem_range_comap_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {p : PrimeSpectrum R},
  p ∈ Set.range (PrimeSpectrum.comap f) ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankRel.equivalence : ∀ (Γ : Type u_1) [inst : Inhabited Γ], Equivalence Turing.BlankRel
-- Mathlib.Control.Bitraversable.Instances
instLawfulBitraversableBicomplOfLawfulTraversable : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] (F G : Type u → Type u) [inst_1 : Traversable F]
  [inst_2 : Traversable G] [LawfulTraversable F] [LawfulTraversable G] [LawfulBitraversable t],
  LawfulBitraversable (Function.bicompl t F G)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (rank : ↑P.II → α)
  (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank x < rank y) (rank_1 : ↑P.II → α)
  (lt_1 : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank_1 x < rank_1 y),
  ({ rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 }) = (rank = rank_1)
-- Mathlib.Algebra.Star.Basic
Units.coe_star : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (u : Rˣ), ↑(star u) = star ↑u
-- Lean.Elab.Tactic.Omega.Core
/-- If the problem is impossible, then `proveFalse?` will contain a proof of `False`.  -/
Lean.Elab.Tactic.Omega.Problem.proveFalse? : Lean.Elab.Tactic.Omega.Problem → Option Lean.Elab.Tactic.Omega.Proof
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.toHasBasis : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasAntitoneBasis s → l.HasBasis (fun x => True) s
-- Lean.Meta.SynthInstance
/-- Auxiliary function for converting the `AbstractMVarsResult` returned by `SynthInstance.main` into an `Expr`.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.applyAbstractResult? : Lean.Expr → Option Lean.Meta.AbstractMVarsResult → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Abelian.Subcategory
CategoryTheory.ObjectProperty.instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels],
  CategoryTheory.IsNormalMonoCategory P.FullSubcategory
-- Mathlib.RingTheory.Localization.BaseChange
/-- The localization of an `R`-module `M` at a submonoid `S` is isomorphic to `S⁻¹R ⊗[R] M` as
an `S⁻¹R`-module.  -/
LocalizedModule.equivTensorProduct : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (M : Type u_3) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → LocalizedModule S M ≃ₗ[Localization S] TensorProduct R (Localization S) M
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsLocallyFiniteMeasure μ
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier_single : ∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (z : d → AddCircle 1) (i : d),
  (UnitAddTorus.mFourier (Pi.single i 1)) z = (fourier 1) (z i)
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousOn.isBigOWith_principal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace α] {s : Set α} {f : α → E} {c : F}
  [inst_1 : SeminormedAddGroup E] [inst_2 : Norm F],
  ContinuousOn f s →
    IsCompact s → ‖c‖ ≠ 0 → Asymptotics.IsBigOWith (sSup (norm '' f '' s) / ‖c‖) (Filter.principal s) f fun x => c
-- Mathlib.Order.Monotone.Monovary
antivary_id_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Antivary f id ↔ Antitone f
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_addEquiv_refl : ∀ (R : Type u_4) [inst : Mul R] [inst_1 : Add R], ↑(RingEquiv.refl R) = AddEquiv.refl R
-- Std.Time.Zoned
/-- Get the current date, in the local timezone.
 -/
Std.Time.PlainDate.now : IO Std.Time.PlainDate
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- The yoneda embedding of `AddMon C` into presheaves of additive monoids.  -/
CategoryTheory.yonedaAddMon : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.AddMon C) (CategoryTheory.Functor Cᵒᵖ AddMonCat)