mathlib-initiative/mathlib-types huggingface dataset:
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshToken.state : ProofWidgets.RefreshToken → IO.Ref ProofWidgets.RefreshComponent.RefreshState
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.one : (α : Type u) → [One α] → One (FreeAbelianGroup α)
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.snd_compProd_prodMkLeft : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} (κ : ProbabilityTheory.Kernel X Y) (η : ProbabilityTheory.Kernel Y Z)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η],
  (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft X η)).snd = η.comp κ
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAdjointPair.sub : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} {B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂} {f f' : M → M₁} {g g' : M₁ → M},
  B.IsAdjointPair B' f g → B.IsAdjointPair B' f' g' → B.IsAdjointPair B' (f - f') (g - g')
-- Init.Grind.ToInt
/-- The infinite interval `(-∞, ∞)`.  -/
Lean.Grind.IntInterval.ii : Lean.Grind.IntInterval
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Interpret a functor to the categorical pullback as a `CatCommSqOver`.  -/
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Functor (CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G))
                      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
-- Init.Data.String.PosRaw
String.instLTRaw : LT String.Pos.Raw
-- Mathlib.Algebra.Group.Semiconj.Defs
addSemiconjBy_iff_eq : ∀ {M : Type u_2} [inst : AddCancelCommMonoid M] {a x y : M}, AddSemiconjBy a x y ↔ x = y
-- ProofWidgets.Data.Html
ProofWidgets.LayoutKind.noConfusionType : Sort v✝ → ProofWidgets.LayoutKind → ProofWidgets.LayoutKind → Sort v✝
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_v_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      ((CochainComplex.mappingCocone.snd φ).v p₂ p₃ h₂₃) =
    β.v p₁ p₃ ⋯
-- Mathlib.Tactic.Linter.AuxLemma
/-- Returns `true` if any component of the name is an auto-generated auxiliary name.  -/
_private.Mathlib.Tactic.Linter.AuxLemma.0.Mathlib.Linter.AuxLemma.nameRefersToAuxLemma : Lean.Name → Bool
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.leftCancelSemigroup : {α : Type u} → [AddLeftCancelSemigroup α] → LeftCancelSemigroup (Multiplicative α)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDualFlip_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (m₁ m₂ : M), (b.toDualFlip m₁) m₂ = (b.toDual m₂) m₁
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ici' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atBot → Set.Iic (f a) ⊆ f '' Set.Ici a
-- Init.Data.Prod
Prod.swap_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α × β), x.swap.swap = x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (L.iCycles i) =
    CategoryTheory.CategoryStruct.comp (K.iCycles i) (φ.f i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_le_maxKey!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k},
        (compare (Std.Internal.List.maxKey! l)
              (Std.Internal.List.maxKey! (Std.Internal.List.insertEntryIfNew k v l))).isLE =
          true
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.measurable_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β]
  (hf : MeasureTheory.AEStronglyMeasurable f μ), Measurable (MeasureTheory.AEStronglyMeasurable.mk f hf)
-- Std.Data.ExtHashMap.Lemmas
/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
obligation in the statement of `getElem_insertIfNew`.  -/
Std.ExtHashMap.contains_of_contains_insertIfNew' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Option.isSome.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none) (val : α),
  x = some val →
    (match x with
      | some val => h_1 val
      | none => h_2 ()) ≍
      h_1 val
-- Init.Tactics
/-- `mvcgen` will break down a Hoare triple proof goal like `⦃P⦄ prog ⦃Q⦄` into verification conditions,
provided that all functions used in `prog` have specifications registered with `@[spec]`.

### Verification Conditions and specifications

A verification condition is an entailment in the stateful logic of `Std.Do.SPred`
in which the original program `prog` no longer occurs.
Verification conditions are introduced by the `mspec` tactic; see the `mspec` tactic for what they
look like.
When there's no applicable `mspec` spec, `mvcgen` will try and rewrite an application
`prog = f a b c` with the simp set registered via `@[spec]`.

### Features

When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` will additionally

* add a Hoare triple specification `foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄` to `spec` set for a
  function `foo` occurring in `prog`,
* unfold a definition `def bar_def ... := ...` in `prog`,
* unfold any method of the `instBEqFloat : BEq Float` instance in `prog`.
* it will no longer substitute away `let`-expressions that occur at most once in `P`, `Q` or `prog`.

### Config options

`+noLetElim` is just one config option of many. Check out `Lean.Elab.Tactic.Do.VCGen.Config` for all
options. Of particular note is `stepLimit = some 42`, which is useful for bisecting bugs in
`mvcgen` and tracing its execution.

### Extended syntax

Often, `mvcgen` will be used like this:
```
mvcgen [...]
case inv1 => exact I1
case inv2 => exact I2
all_goals (mleave; try grind)
```
There is special syntax for this:
```
mvcgen [...] invariants
· I1
· I2
with grind
```
When `I1` and `I2` need to refer to inaccessibles (`mvcgen` will introduce a lot of them for program
variables), you can use case label syntax:
```
mvcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2
with grind
```
This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.

### Invariant suggestions

`mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
```
mvcgen [...] invariants?
```
This is useful if you do not recall the exact syntax to construct invariants.
Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and
this must hold at the end of the loop" by looking at the corresponding VCs.
Although the suggested invariant is a good starting point, it is too strong and requires users to
interpolate it such that the inductive step can be proved. Example:
```
def mySum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for x in l do
    acc := acc + x
  return acc

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen invariants?
  all_goals admit
```
 -/
Lean.Parser.Tactic.mvcgenMacro : Lean.ParserDescr
-- Lean.Util.CollectFVars
Lean.collectFVars : Lean.CollectFVars.State → Lean.Expr → Lean.CollectFVars.State
-- Mathlib.CategoryTheory.Equivalence
/-- If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence.  -/
CategoryTheory.Functor.isEquivalence_of_comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).IsEquivalence], G.IsEquivalence
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_coe : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  ↑f.range = Set.range ⇑f
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.size_node : ∀ {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α), (Ordnode.node sz l x r).size = sz
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (h : α) (s : Stream'.Seq (GenContFract.Pair α)),
  sizeOf { h := h, s := s } = 1 + sizeOf h + sizeOf s
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.GrothendieckTopology.closureOperator_isClosed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) (X : C)
  (S : CategoryTheory.Sieve X), (J₁.closureOperator X).IsClosed S = J₁.IsClosed S
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- If `X : Truncated 2` has a unique `0`-simplex and (at most) one `1`-simplex,
then `X.HomotopyCategory` is a terminal object in `Cat`.  -/
SSet.Truncated.HomotopyCategory.isTerminal : (X : SSet.Truncated 2) →
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))] →
    [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 }))] →
      CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of X.HomotopyCategory)
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.instInhabitedCommandCodeActionEntry.default : Lean.CodeAction.CommandCodeActionEntry
-- Mathlib.Analysis.Fourier.Inversion
/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
space is integrable, and its Fourier transform `𝓕 f` is also integrable, then `𝓕 (𝓕⁻ f) = f` at
continuity points of `f`.  -/
MeasureTheory.Integrable.fourier_fourierInv_eq : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
      ∀ {v : V}, ContinuousAt f v → FourierTransform.fourier (FourierTransformInv.fourierInv f) v = f v
-- Batteries.Data.List.Lemmas
List.countPBefore.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (xs : List α) (i s : ℕ),
  List.countPBefore.go p xs i s =
    match xs, i, s with
    | head :: tail, 0, s => s
    | a :: xs, i.succ, s => bif p a then List.countPBefore.go p xs i (s + 1) else List.countPBefore.go p xs i s
    | [], x, s => s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.revAll_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → s.revAll pat = t.revAll pat
-- Mathlib.Data.Real.Basic
Real.instAddSemigroup : AddSemigroup ℝ
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  {F G : CategoryTheory.Functor (↑(Set.Iic x)) C} {i₁ i₂ i₃ : K} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ x},
  CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G i₁ i₂ h₁₂ ⋯ →
    CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G i₂ i₃ h₂₃ h₃ →
      CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G i₁ i₃ ⋯ h₃
-- Mathlib.Logic.Equiv.Defs
/-- If `α` is an empty type, then it is equivalent to the `Empty` type.  -/
Equiv.equivEmpty : (α : Sort u) → [IsEmpty α] → α ≃ Empty
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Module ℝ A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A},
  0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
-- Mathlib.RingTheory.Ideal.Defs
Ideal.ext_iff : ∀ {α : Type u} [inst : Semiring α] {I J : Ideal α}, I = J ↔ ∀ (x : α), x ∈ I ↔ x ∈ J
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.eq_or_ssubset`.

---

Set notation form of `LE.le.eq_or_lt` -/
HasSubset.Subset.eq_or_ssubset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a = b ∨ a ⊂ b
-- Mathlib.Topology.FiberBundle.Constructions
instTopologicalSpacePullback : {B : Type u} →
  (E : B → Type w₁) →
    {B' : Type w₂} → (f : B' → B) → [(x : B) → TopologicalSpace (E x)] → (x : B') → TopologicalSpace ((f *ᵖ E) x)
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.sub_right : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α β : u ⟶ v),
  CategoryTheory.Arrow.Hom.right (α - β) = CategoryTheory.Arrow.Hom.right α - CategoryTheory.Arrow.Hom.right β
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instSMulCommClass'' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M N (Lex α)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_eq_left : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊢ₛ Q ↔ P ⊣⊢ₛ P ∧ Q
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.eraseExtAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Unit
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- If `x` is a unit, then the multiset of normalized factors of `x` is nil.
The converse is true with a nonzero assumption, see `normalizedFactors_eq_zero_iff`.
 -/
UniqueFactorizationMonoid.normalizedFactors_of_isUnit : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x : α}, IsUnit x → UniqueFactorizationMonoid.normalizedFactors x = 0
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- A linear equiv induces a linear equiv on adic completions.  -/
AdicCompletion.congr : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_3} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → (M ≃ₗ[R] N) → AdicCompletion I M ≃ₗ[AdicCompletion I R] AdicCompletion I N
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} (h' : a ∈ t), t.get? a = some (t.get a h')
-- Init.Data.Array.Lemmas
Array.empty_eq_flatten_iff : ∀ {α : Type u_1} {xss : Array (Array α)}, #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[]
-- Mathlib.Logic.Relation
Relation.ReflGen.single : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r a b → Relation.ReflGen r a b
-- Init.Data.Iterators.Basic
Std.IterStep.skip.sizeOf_spec : ∀ {α : Sort u_1} {β : Sort u_2} [inst : SizeOf α] [inst_1 : SizeOf β] (it : α),
  sizeOf (Std.IterStep.skip it) = 1 + sizeOf it
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_iff_of_dvd_of_pos : ∀ {a b c d : ℤ}, 0 < b → 0 < d → b ∣ a → d ∣ c → (a / b < c / d ↔ d * a < c * b)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedResponseError : {a : Type u_1} → Inhabited (Lean.JsonRpc.ResponseError a)
-- Init.Data.UInt.Lemmas
UInt64.eq_of_toBitVec_eq : ∀ {a b : UInt64}, a.toBitVec = b.toBitVec → a = b
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  (e e_1 : (i : ι) → D₁.obj i ≅ D₂.obj i) (e_e : e = e_1)
  (comm :
    ∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
          ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) =
        CategoryTheory.CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂)),
  CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk e comm =
    CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk e_1 ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.ge : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → g ≤ᶠ[l] f
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.isUniformEmbedding_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α], IsUniformEmbedding CauchyFilter.pureCauchy
-- Mathlib.Topology.Algebra.Module.Star
/-- If `A` is a topological module over a commutative `R` with compatible actions,
then `star` is a continuous semilinear equivalence.  -/
starL : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : AddCommMonoid A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Module R A] → [StarModule R A] → [inst_6 : TopologicalSpace A] → [ContinuousStar A] → A ≃L⋆[R] A
-- Std.Http.Data.Request
Std.Http.Request.instToStringHead : ToString Std.Http.Request.Head
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_erase_eq_of_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).max? = t.max?
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.M.run : {α : Type} → Lean.Meta.Grind.EMatch.M α → Lean.Meta.Grind.GoalM (α × Lean.Meta.Grind.EMatch.SearchState)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e)
      (AlgebraicGeometry.Scheme.Hom.appIso f V).inv =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Init.Data.ByteArray.Bootstrap
Array.push.eq_1 : ∀ {α : Type u} (a : Array α) (v : α), a.push v = { toList := a.toList.concat v }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.toScheme_carrier : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), ↥↑U = ↑↑U
-- Mathlib.Order.Restriction
/-- If a function `f` indexed by `α` is restricted to elements `≤ b`, and `a ≤ b`,
this is the restriction to elements `≤ b`. Intervals are seen as finite sets.  -/
Preorder.frestrictLe₂ : {α : Type u_1} →
  [inst : Preorder α] →
    {π : α → Type u_2} →
      [inst_1 : LocallyFiniteOrderBot α] →
        {a b : α} → a ≤ b → ((i : ↥(Finset.Iic b)) → π ↑i) → (i : ↥(Finset.Iic a)) → π ↑i
-- Init.Data.SInt.Lemmas
Int16.toInt_one : Int16.toInt 1 = 1
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.instEquivLike : {R : Type u_1} →
  {S : Type u_6} →
    {M : Type u_7} →
      {M₂ : Type u_9} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {modM : Module R M} →
                  {modM₂ : Module S M₂} →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        [inst_4 : RingHomInvPair σ σ'] → [inst_5 : RingHomInvPair σ' σ] → EquivLike (M ≃ₛₗ[σ] M₂) M M₂
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_comp_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : A}
  (h : CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀
        (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f)
        h)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the chain map sending `x : Hⁿ → A` to `(g : Gⁿ) ↦ φ (x (f ∘ g))`.  -/
groupCohomology.cochainsMap : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k H} →
          {B : Rep.{u, u, u} k G} →
            (f : G →* H) →
              (Rep.res f A ⟶ B) → (groupCohomology.inhomogeneousCochains A ⟶ groupCohomology.inhomogeneousCochains B)
-- Mathlib.Order.Filter.IsBounded
Filter.isCobounded_le_of_bot : ∀ {α : Type u_1} [inst : LE α] [OrderBot α] {f : Filter α}, Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.Algebra.Group.Defs
CommSemigroup.ext : ∀ {G : Type u} {x y : CommSemigroup G}, Mul.mul = Mul.mul → x = y
-- Init.Data.Nat.Gcd
Nat.gcd_sub_self_left : ∀ {m n : ℕ}, m ≤ n → (n - m).gcd m = n.gcd m