mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.Data
Aesop.GoalData.parent : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → IO.Ref MVarCluster
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_isOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : AlgebraicGeometry.PresheafedSpace C}
  (Y : AlgebraicGeometry.SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion
    (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.topIso_inv_ι_assoc : ∀ (X : SSet) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.topIso X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.ι ⊤) h) =
    h
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_eq_compl_inter`. -/
Set.diff_eq_compl_inter : ∀ {α : Type u_1} {s t : Set α}, s \ t = tᶜ ∩ s
-- Mathlib.Algebra.Divisibility.Units
IsUnit.dvd_mul_right : ∀ {α : Type u_1} [inst : Monoid α] {a b u : α}, IsUnit u → (a ∣ b * u ↔ a ∣ b)
-- Init.Data.Vector.Lemmas
Vector.all_push : ∀ {α : Type u_1} {n : ℕ} {as : Vector α n} {a : α} {p : α → Bool}, (as.push a).all p = (as.all p && p a)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.image_eq_preimage_symm : ∀ {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₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M),
  ⇑e '' s = ⇑e.symm ⁻¹' s
-- Init.Data.Dyadic.Basic
Dyadic.not_lt : ∀ {x y : Dyadic}, ¬x ≤ y ↔ y < x
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E}
  {s : Set 𝕜} {t : Set E} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              ↑i ≤ n →
                iteratedDerivWithin i (g ∘ f) s x =
                  ∑ c, (iteratedFDerivWithin 𝕜 c.length g t (f x)) fun j => iteratedDerivWithin (c.partSize j) f s x
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MkAtom₁.mk : {m : Type → Type} → (Lean.Expr → m Mathlib.Tactic.BicategoryLike.Atom₁) → Mathlib.Tactic.BicategoryLike.MkAtom₁ m
-- Lean.Server.Requests
Lean.Server.RequestHandler : Type
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT0Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T0Space M], T0Space Mᵈᵃᵃ
-- Batteries.Data.List.Basic
/-- Get the head and tail of a list, if it is nonempty.  -/
List.next? : {α : Type u_1} → List α → Option (α × List α)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.cycles
-- Mathlib.RingTheory.Ideal.Int
Ideal.ringChar_quot : ∀ {S : Type u_2} [inst : CommRing S] (I : Ideal S), ringChar (S ⧸ I) = Ideal.absNorm (Ideal.under ℤ I)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {fallback : (a : α) × β a}, (k == a) = true → Std.Internal.List.getEntryD a fallback (⟨k, v⟩ :: l) = ⟨k, v⟩
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- A multiplicative action is isometric if each map `x ↦ c • x` is an isometry.  -/
IsIsometricSMul : (M : Type u) → (X : Type w) → [PseudoEMetricSpace X] → [SMul M X] → Prop
-- Mathlib.Data.Matrix.Basic
Matrix.piAlgEquiv_symm_apply : ∀ {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (R : Type u_16) [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (β i)] [inst_2 : (i : ι) → Algebra R (β i)] [inst_3 : Fintype n] [inst_4 : DecidableEq n]
  (f : (i : ι) → Matrix n n (β i)), (Matrix.piAlgEquiv R).symm f = Matrix.of fun j k i => f i j k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.insertMany t l) k' = some v
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.read.inj : ∀ {f f_1 : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.read f = Turing.PartrecToTM2.Λ'.read f_1 → f = f_1
-- Mathlib.Data.Int.ModEq
Int.gcd_a_modEq : ∀ (a b : ℕ), ↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSeq.ord_cof : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → o.cof.ord = a
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the third row  -/
CategoryTheory.ShortComplex.SnakeInput.L₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.Data.Nat.Log
Nat.log_antitone_left : ∀ {n : ℕ}, AntitoneOn (fun b => Nat.log b n) (Set.Ioi 1)
-- Mathlib.Topology.Baire.Lemmas
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with a union over a countable set in any type.  -/
IsGδ.dense_biUnion_interior_of_closed : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [BaireSpace X] {t : Set α} {s : Set X},
  IsGδ s →
    Dense s →
      t.Countable → ∀ {f : α → Set X}, (∀ i ∈ t, IsClosed (f i)) → s ⊆ ⋃ i ∈ t, f i → Dense (⋃ i ∈ t, interior (f i))
-- Lean.Meta.PProdN
/-- Strips top-level `PProd` and `And` projections  -/
Lean.Meta.PProdN.stripProjs : Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_finitary : ∀ {α : Type u_1} {β : Type u_2} (N : Matroid β) [N.Finitary] (f : α → β), (N.comap f).Finitary
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_apply_basis : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂)
  (M : Matrix n m N₂) (i : n) (j : m), (((Matrix.toLinearMap₂ b₁ b₂) M) (b₁ i)) (b₂ j) = M i j
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_zero : ∀ {R : Type u_1} [inst : Semiring R], ↑0 = 0
-- Mathlib.Order.Heyting.Basic
Codisjoint.himp_inf_cancel_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇨ a ⊓ b = b
-- Init.Data.UInt.Lemmas
UInt64.ofNat_one : UInt64.ofNat 1 = 1
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.coe_compMultilinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂), ⇑(g.compMultilinearMap f) = ⇑g ∘ ⇑f
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μα : MeasureTheory.Measure α} [h : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)] {t : Set Ω},
  ProbabilityTheory.Kernel.IndepSet t t κ μα → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Mathlib.Algebra.Order.Interval.Basic
instInvNonemptyInterval : {α : Type u_2} → [inst : CommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedMonoid α] → Inv (NonemptyInterval α)
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p q : Seminorm 𝕜 E) (e : E) (r : ℝ), (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from additive monoids to types preserves all limits.  -/
AddMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)
-- Mathlib.Analysis.Calculus.MeanValue
Convex.isLittleO_pow_succ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {x₀ : E}
  {n : ℕ},
  Convex ℝ s →
    x₀ ∈ s →
      (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
        (f' =o[nhdsWithin x₀ s] fun x => ‖x - x₀‖ ^ n) →
          (fun x => f x - f x₀) =o[nhdsWithin x₀ s] fun x => ‖x - x₀‖ ^ (n + 1)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqCongrKey : {enodeMap : Lean.Meta.Grind.ENodeMap} → BEq (Lean.Meta.Grind.CongrKey enodeMap)
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a], ⅟a * (a * b) = b
-- Lean.Data.PrefixTree
Lean.PrefixTree.foldM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      {p : α → α → Ordering} → {σ : Type u_1} → [Monad m] → Lean.PrefixTree α β p → σ → (β → σ → m σ) → m σ
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When `S.g = 0`, this is the canonical isomorphism `S.cycles ≅ S.X₂` induced by `S.iCycles`.  -/
CategoryTheory.ShortComplex.cyclesIsoX₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.g = 0 → (S.cycles ≅ S.X₂)
-- Mathlib.Order.Filter.IsBounded
isBoundedUnder_ge_finset_inf : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] [inst_1 : OrderTop β] {f : Filter α}
  {F : ι → α → β} {s : Finset ι},
  (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f (F i)) →
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f fun a => s.inf fun i => F i a
-- Aesop.Options.Public
/-- The search strategy used by Aesop.
 -/
Aesop.Options.strategy : Aesop.Options → Aesop.Strategy
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `le_of_isLUB_Iio`. -/
lub_Iio_le : ∀ {α : Type u_1} [inst : Preorder α] {b : α} (a : α), IsLUB (Set.Iio a) b → b ≤ a
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Auxiliary lemma for `lift_d_comp_eq_zero_iff`.  -/
HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' : ι'} (hj' : e.f j = j'),
  c.prev j = i →
    c'.prev j' = i' →
      ∀ (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) ⦃W : C⦄
        (f' : K.X i ⟶ cone.pt),
        CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.Fork.ι cone) = K.d i j →
          ∀ (f'' : (K.extend e).X i' ⟶ cone.pt),
            CategoryTheory.CategoryStruct.comp f''
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cone) (K.extendXIso e hj').inv) =
                (K.extend e).d i' j' →
              ∀ (φ : cone.pt ⟶ W),
                CategoryTheory.CategoryStruct.comp f' φ = 0 ↔ CategoryTheory.CategoryStruct.comp f'' φ = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a))
      (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
        (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv)
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctor_obj_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)),
  (SimplicialObject.opFunctor.obj X).δ i =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.hom
      (CategoryTheory.CategoryStruct.comp (X.δ i.rev) SimplicialObject.opObjIso.inv)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_eq_top_of_algebra : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  Algebra.adjoin F S = ⊤ → IntermediateField.adjoin F S = ⊤
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
not_isCyclic_prod_of_infinite_nontrivial : ∀ (M : Type u_4) (N : Type u_5) [inst : Group M] [inst_1 : Group N] [Infinite M] [Nontrivial N], ¬IsCyclic (M × N)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.ext_adjoin_singleton : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B]
  [inst_7 : StarRing B] [inst_8 : StarModule R A] {a : A} [inst_9 : FunLike F (↥(StarAlgebra.adjoin R {a})) B]
  [AlgHomClass F R (↥(StarAlgebra.adjoin R {a})) B] [StarHomClass F (↥(StarAlgebra.adjoin R {a})) B] {f g : F},
  f ⟨a, ⋯⟩ = g ⟨a, ⋯⟩ → f = g
-- Mathlib.Dynamics.Transitive
MulAction.IsTopologicallyTransitive.exists_smul_inter : ∀ {M : Type u_1} {α : Type u_2} {inst : Monoid M} {inst_1 : TopologicalSpace α} {inst_2 : MulAction M α}
  [self : MulAction.IsTopologicallyTransitive M α] {U V : Set α},
  IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (m • U ∩ V).Nonempty
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
/-- When `C` is braided and `tensorRight c` preserves a colimit, then so does `tensorLeft k`.
We are not making this an instance to avoid an instance loop with
`preservesColimit_of_braided_and_preservesColimit_tensor_left`.  -/
CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.BraidedCategory C] (c : C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.tensorRight c)],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.tensorLeft c)
-- Init.Data.Vector.Attach
Vector.attachWith_push : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x},
  (xs.push a).attachWith P H = (xs.attachWith P ⋯).push ⟨a, ⋯⟩
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_zero`. -/
LinearOrderedField.inducedMap_zero : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedMap α β 0 = 0
-- Init.Data.UInt.Lemmas
USize.ne_iff_toBitVec_ne : ∀ {a b : USize}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instLT : (ι : Type u_1) → LT (PreAbstractSimplicialComplex ι)
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamilyₗ_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommSemiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.dfinsuppFamilyₗ f = MultilinearMap.dfinsuppFamily f
-- Init.Data.BitVec.Lemmas
/-- If a number `w * n ≤ i < w * (n + 1)`, then `i - w * n` equals `i % w`.
This is true by subtracting `w * n` from the inequality, giving
`0 ≤ i - w * n < w`, which uniquely identifies `i % w`.
 -/
_private.Init.Data.BitVec.Lemmas.0.BitVec.Nat.sub_mul_eq_mod_of_lt_of_le : ∀ {w n i : ℕ}, w * n ≤ i → i < w * (n + 1) → i - w * n = i % w
-- Init.Data.SInt.Bitwise
ISize.toInt16_xor : ∀ (a b : ISize), (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
-- Init.Data.Iterators.Basic
/-- The step function of an iterator in `Iter (α := α) β` or `IterM (α := α) m β`.

In order to allow intrinsic termination proofs when iterating with the `step` function, the
step object is bundled with a proof that it is a "plausible" step for the given current iterator.
 -/
Std.Iterator : Type w → (Type w → Type w') → outParam (Type w) → Type (max w w')
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- The unique point in a single-point space is the simplest example of an affine basis.  -/
AffineBasis.instInhabitedPUnit : {k : Type u_5} → [inst : Ring k] → Inhabited (AffineBasis PUnit.{u_8 + 1} k PUnit.{u_8 + 1})
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.skipRight : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)} {out₁ : { out // ∃ it, it.IsPlausibleOutput out }},
  it.internalState.memoizedLeft = some out₁ →
    ∀ {it₂' : Std.IterM m β₂},
      it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂') →
        Std.Iterators.Types.Zip.PlausibleStep it
          (Std.IterStep.skip
            { internalState := { left := it.internalState.left, memoizedLeft := some out₁, right := it₂' } })
-- Lean.Attributes
Lean.instInhabitedAttributeImplCore.default : Lean.AttributeImplCore
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- If a path `p` is Hamiltonian then the graph has finitely many vertices.  -/
SimpleGraph.Walk.IsHamiltonian.fintype : {α : Type u_1} →
  [inst : DecidableEq α] → {G : SimpleGraph α} → {a b : α} → {p : G.Walk a b} → p.IsHamiltonian → Fintype α
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.ProjectiveResolution X} {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) {Z : CochainComplex C ℤ} (h : (CochainComplex.singleFunctor C 0).obj X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ.hom' (CategoryTheory.CategoryStruct.comp R'.π' h) =
    CategoryTheory.CategoryStruct.comp R.π'
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) h)
-- Mathlib.Order.Basic
LinearOrder.toPartialOrder_injective_iff : ∀ {α : Type u_2} {a₁ a₂ : LinearOrder α}, a₁ = a₂ ↔ a₁.toPartialOrder = a₂.toPartialOrder
-- Mathlib.Topology.Separation.GDelta
Topology.IsInducing.perfectlyNormalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PerfectlyNormalSpace Y]
  {e : X → Y}, Topology.IsInducing e → PerfectlyNormalSpace X
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.Intermediate.dropWhile_eq_dropWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [Std.Iterator α m β] {it : Std.IterM m β}
  {P : β → Bool} {dropping : Bool},
  Std.IterM.Intermediate.dropWhile P dropping it =
    Std.IterM.Intermediate.dropWhileWithPostcondition (pure ∘ ULift.up ∘ P) dropping it
-- Init.Prelude
Nat.le.below.step : ∀ {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {m : ℕ} (a : n.le m), Nat.le.below a → motive m a → Nat.le.below ⋯
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_ne_last : ∀ {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)}, a ≠ Fin.last (n + 1) → b ≠ Fin.last n → a.succAbove b ≠ Fin.last (n + 1)
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.PlausibleStep.skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it') →
    Std.Iterators.Types.TakeWhile.PlausibleStep it (Std.IterStep.skip (Std.IterM.takeWhileWithPostcondition P it'))
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_probChar : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_7} {W : Type u_8}
  {x : MeasurableSpace V} [inst_2 : AddCommGroup V] [inst_3 : Module ℝ V] [inst_4 : AddCommGroup W]
  [inst_5 : Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : MeasureTheory.Measure V) (f : V → E) (w : W),
  VectorFourier.fourierIntegral Real.probChar μ L f w = ∫ (v : V), Complex.exp (-↑((L v) w) * Complex.I) • f v ∂μ
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.allDiffAux.eq_def : ∀ {α : Type u} [inst : BEq α] (as : Array α) (i : ℕ),
  Array.allDiffAux✝ as i =
    if h : i < as.size then Array.allDiffAuxAux✝ as as[i] i h && Array.allDiffAux✝ as (i + 1) else true
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.pushAtomStrLit : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Filter.Basic
/-- An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g.,
`Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`).  -/
Filter.coext : ∀ {α : Type u} {f g : Filter α}, (∀ (s : Set α), sᶜ ∈ f ↔ sᶜ ∈ g) → f = g
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.sc'Map_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
  (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'Map._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'Map._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'Map._auto_5),
  (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₂ = φ.app ⟨j, ⋯⟩
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.mk : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : R},
  m ≠ 0 → ⁅h, m⁆ = μ • m → ⁅e, m⁆ = 0 → t.HasPrimitiveVectorWith m μ
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.ker_prodMap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {G' : Type u_8} {N' : Type u_9}
  [inst_2 : AddGroup G'] [inst_3 : AddGroup N'] (f : G →+ N) (g : G' →+ N'), (f.prodMap g).ker = f.ker.prod g.ker