mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M} {x : M},
  (∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) →
    ChartedSpace.LiftPropAt P g x → ChartedSpace.LiftPropWithinAt P g s x
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.IsOpen.inter : ∀ (α : Type u) [inst : OmegaCompletePartialOrder α] (s t : Set α),
  Scott.IsOpen α s → Scott.IsOpen α t → Scott.IsOpen α (s ∩ t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Concyclic.mk : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P},
  EuclideanGeometry.Cospherical ps → Coplanar ℝ ps → EuclideanGeometry.Concyclic ps
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.Raw.ofList l cmp).get? k' = some (cast ⋯ v)
-- Mathlib.Data.Fin.Fin2
Fin2.fs.injEq : ∀ {n : ℕ} (a a_1 : Fin2 n), (a.fs = a_1.fs) = (a = a_1)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.apply_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : Y),
  e (e.symm x) = x
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Vertical composition of modifications.  -/
CategoryTheory.Lax.LaxTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Lax.LaxTrans.Modification η θ →
              CategoryTheory.Lax.LaxTrans.Modification θ ι → CategoryTheory.Lax.LaxTrans.Modification η ι
-- Mathlib.Data.Finset.Lattice.Basic
Finset.right_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s = t ∪ s ↔ t ⊆ s
-- Init.Data.Vector.Lemmas
Vector.prod_toList : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] [inst_1 : One α] {xs : Vector α n}, xs.toList.prod = xs.prod
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.bidirectionalRec.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) → ((a : α) → motive [a]) → ((a b : α) → (l : List α) → motive (a :: b :: l)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_inf : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V} (v : V), (G₁ ⊓ G₂).neighborSet v = G₁.neighborSet v ∩ G₂.neighborSet v
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ^ (k - s + 1) ≠ 2`. See the next lemmas
for similar results.  -/
IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two : ∀ {p : ℕ} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k s : ℕ},
  IsPrimitiveRoot ζ (p ^ (k + 1)) →
    ∀ [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L],
      Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
        s ≤ k → p ^ (k - s + 1) ≠ 2 → (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.Order.LiminfLimsup
Filter.liminfReparam.eq_1 : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) (s : ι' → Set ι)
  (p : ι' → Prop) [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)] (j : Subtype p),
  Filter.liminfReparam f s p j = if j ∈ {j | BddBelow (Set.range fun i => f ↑i)} then j else ⋯.choose (Nat.find ⋯)
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_X_pow : ∀ {F : Type u} [inst : Field F] {n : ℕ}, (Polynomial.X ^ n).natSepDegree = if n = 0 then 0 else 1
-- Mathlib.Order.Filter.Map
Filter.eventuallyLE_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} [inst : LE γ] {f₁ f₂ : β → γ},
  f₁ ≤ᶠ[Filter.map m f] f₂ ↔ f₁ ∘ m ≤ᶠ[f] f₂ ∘ m
-- Batteries.Data.Fin.Coding
Fin.decodePi.eq_1 : ∀ (x_2 : Fin 0 → ℕ) (x_3 : Fin (Fin.prod x_2)), Fin.decodePi x_2 x_3 = fun x => nomatch x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.subsingleton_of_empty_left : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty m], Subsingleton (Matrix m n α)
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The change-of-basis matrix between two orthonormal bases with the same orientation has
determinant 1.  -/
OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
  e.toBasis.orientation = f.toBasis.orientation → e.toBasis.det ⇑f = 1
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
MonomialOrder.degLex_single_le_iff : ∀ {σ : Type u_2} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {a b : σ},
  ((MonomialOrder.degLex.toSyn fun₀ | a => 1) ≤ MonomialOrder.degLex.toSyn fun₀ | b => 1) ↔ b ≤ a
-- Mathlib.Algebra.BigOperators.Fin
/-- This is a classic "telescoping sum" lemma. It says:
`r₀ - (r₀ + r₁) + (r₁ + r₂) - (r₂+ r₃) + ⋯ ± (rₙ₋₁ + rₙ) ∓ rₙ = 0`.

The chosen spelling, which gives definitional power over `d`, is influenced by downstream
applications such as `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`.  -/
Fin.sum_neg_one_pow_eq_zero : ∀ {α : Type u_3} [inst : AddCommGroup α] {n : ℕ} (d : Fin (n + 2) → α) (r : Fin (n + 1) → α),
  d 0 = r 0 →
    (∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ) →
      d (Fin.last (n + 1)) = r (Fin.last n) → ∑ i, (-1) ^ ↑i • d i = 0
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : Preorder β]
  [inst_3 : BoundedOrder β] [inst_4 : Preorder γ] [inst_5 : BoundedOrder γ] (g : BoundedOrderHom βᵒᵈ γᵒᵈ)
  (f : BoundedOrderHom αᵒᵈ βᵒᵈ),
  BoundedOrderHom.dual.symm (g.comp f) = (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation_add_coe : ∀ (L : PeriodPair) (x : ℂ) (l : ↥L.lattice), PeriodPair.relation✝ L (x + ↑l) = PeriodPair.relation✝ L x
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_self : ∀ (n : ℕ), n.stirlingSecond n = 1
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortExact_shortComplexObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).ShortExact
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.Hom.injective`. -/
CategoryTheory.CardinalFilteredPoset.Hom.injective : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J₁ J₂ : CategoryTheory.CardinalDirectedPoset κ} (f : J₁ ⟶ J₂),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.Cert.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {subject : Q(«$α»)}
  {result : Mathlib.Tactic.Determinant.CertResult rα subject} {isZero : Bool} {subject_1 : Q(«$α»)}
  {result_1 : Mathlib.Tactic.Determinant.CertResult rα subject_1} {isZero_1 : Bool},
  { subject := subject, result := result, isZero := isZero } =
      { subject := subject_1, result := result_1, isZero := isZero_1 } →
    subject = subject_1 ∧ result ≍ result_1 ∧ isZero = isZero_1
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_ext : ∀ {X Y : BddDistLat} {f g : X ⟶ Y}, BddDistLat.Hom.hom f = BddDistLat.Hom.hom g → f = g
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The continuous function from the basic open set `D(f)` in `Proj`
to the corresponding basic open set in `Spec A⁰_f`.  -/
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace ⟶
                  ↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                        (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.trimmed_iff_seq_trimmed : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)), ms.Trimmed ↔ ms.seq.Trimmed
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The equivalence setoid for a projective point representative on a Weierstrass curve.  -/
WeierstrassCurve.Projective.instSetoidForallFinOfNatNat : {R : Type r} → [CommRing R] → Setoid (Fin 3 → R)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map_id : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  FundamentalGroupoid.map (ContinuousMap.id X) = CategoryTheory.Functor.id (FundamentalGroupoid X)
-- Lean.Elab.ConfigEval.Types
/-- The configuration value. Usually this is a `Term`, but user-defined configuration items
can use arbitrary syntax. For `+`/`-` booleans, this syntax is synthetic.  -/
Lean.Elab.ConfigEval.ConfigItem.value : Lean.Elab.ConfigEval.ConfigItem → Lean.Syntax
-- Mathlib.CategoryTheory.Abelian.Yoneda
CategoryTheory.preadditiveYonedaMap.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v, u₁} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (X : C), CategoryTheory.preadditiveYonedaMap F X = CategoryTheory.preadditiveYonedaMap F X
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitIsoSwapCompLim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.limitIsoSwapCompLim G).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).hom
      (CategoryTheory.Limits.limMap (G.flipIsoCurrySwapUncurry.hom.app X))
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex.X₂ = (X₂ ⊞ X₃)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Set`. See note [pointwise nat action].  -/
Set.ZSMul : {α : Type u_2} → [Zero α] → [Add α] → [Neg α] → SMul ℤ (Set α)
-- Lean.DocString.Syntax
Lean.Doc.Syntax.linebreak : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.irrational_of_isRoot_T_real : ∀ {n : ℕ} {x : ℝ}, (Polynomial.Chebyshev.T ℝ ↑n).IsRoot x → x ≠ 0 → Irrational x
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
CommGrpTypeEquivalenceCommGrp.inverse_obj_inv : ∀ {A : CommGrpCat} {x : (fun X => X) (CommGrpTypeEquivalenceCommGrp.inverse.obj A).X},
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.GrpObj.inv) x = x⁻¹
-- Init.Data.UInt.Lemmas
UInt64.lt_of_le_of_ne : ∀ {a b : UInt64}, a ≤ b → a ≠ b → a < b
-- Mathlib.RepresentationTheory.Basic
Representation.single_smul : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (t : k) (g : G) (v : ρ.asModule),
  MonoidAlgebra.single g t • v = t • (ρ g) (ρ.asModuleEquiv v)
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_apply_assoc : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y : C₁} (G : CategoryTheory.Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G)
  (f : L₁.obj X ⟶ L₁.obj Y) {Z : D₂} (h : L₂.obj (Φ.functor.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) h =
    CategoryTheory.CategoryStruct.comp (e.hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (e.inv.app Y) h))
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.eq_1 : ∀ {α : Type u_1} (l : List α) (le : α → α → Bool),
  List.MergeSort.Internal.mergeSortTR₂ l le = List.MergeSort.Internal.mergeSortTR₂.run✝ le ⟨l, ⋯⟩
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_false_left : ∀ {b c : Bool}, false.atLeastTwo b c = (b && c)
-- Init.Data.List.Nat.Pairwise
/-- The list `List.finRange n` is strictly increasing.  -/
List.pairwise_lt_finRange : ∀ (n : ℕ), List.Pairwise (fun x1 x2 => x1 < x2) (List.finRange n)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_two : ∀ {α : Type u_1} {G : SimpleGraph α}, G.CliqueFree 2 ↔ G = ⊥
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a constant function is `⊤` if the constant is zero and `0` otherwise.
 -/
meromorphicOrderAt_const_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (z₀ : 𝕜) (n : ℤ) [inst_3 : Decidable (↑n = 0)],
  meromorphicOrderAt (↑n) z₀ = if ↑n = 0 then ⊤ else 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- An equivalent expression of `IsLinearSet` in terms of `Finset` instead of `Set.Finite`.  -/
isLinearSet_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsLinearSet s ↔ ∃ a t, s = a +ᵥ ↑(AddSubmonoid.closure ↑t)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_neg_iff_of_nonpos : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M] {f : ι → M}, f ≤ 0 → (∑ i, f i < 0 ↔ f < 0)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.eval.eq_4 : Std.Tactic.BVDecide.Gate.or.eval = fun x1 x2 => x1 || x2
-- Init.Data.Array.Find
Array.findSome?_eq_none_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {p : α → Option α_1} {xs : Array α},
  Array.findSome? p xs = none ↔ ∀ x ∈ xs, p x = none
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C)
  (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
      CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m),
  (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).truth = truth
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.sub b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_8 a b
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.addTermOpId : Lean.Expr → Lean.Meta.Grind.AC.ACM Unit
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instBraidedCategoryScheme : CategoryTheory.BraidedCategory AlgebraicGeometry.Scheme
-- Mathlib.Analysis.Calculus.ContDiff.Operations
hasFTaylorSeriesUpToOn_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
  {P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)} {n : WithTop ℕ∞},
  HasFTaylorSeriesUpToOn n Φ P' s ↔
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k (Std.Internal.List.modifyKey k f l) =
      Option.map f (Std.Internal.List.getValueCast? k l)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- **Alias** of `Submodule.adjoint_orthogonalProjectionOnto`. -/
Submodule.adjoint_orthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (U : Submodule 𝕜 E) [inst_4 : CompleteSpace ↥U],
  ContinuousLinearMap.adjoint U.orthogonalProjectionOnto = U.subtypeL
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.preservesFiniteColimits_tateComplexFunctor : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G],
  CategoryTheory.Limits.PreservesFiniteColimits (tateComplexFunctor R G)
-- Init.Data.Vector.Algebra
Vector.instSub : {α : Type u_1} → {n : ℕ} → [Sub α] → Sub (Vector α n)
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.coe_of_map_div : ∀ {G : Type u_5} [inst : Group G] {H : Type u_8} [inst_1 : Group H] (f : G → H)
  (hf : ∀ (x y : G), f (x / y) = f x / f y), ⇑(MonoidHom.ofMapDiv f hf) = f
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH.eq_1 : ∀ {X : Type u_2} [inst : EMetricSpace X] (s : Set X),
  dimH s = ⨆ d, ⨆ (_ : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤), ↑d
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_5 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (g : Std.Tactic.BVDecide.Gate) (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs) cache =
    match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig lhs cache with
    | { result := ⟨{ aig := aig_1, ref := lhsRef }, lextend⟩, cache := cache } =>
      match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_1 rhs cache with
      | { result := ⟨{ aig := aig_2, ref := rhsRef }, rextend⟩, cache := cache } =>
        let lhsRef_1 := lhsRef.cast rextend;
        let input := { lhs := lhsRef_1, rhs := rhsRef };
        match g with
        | Std.Tactic.BVDecide.Gate.and =>
          let ret := aig_2.mkAndCached input;
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨ret, this⟩, cache := cache }
        | Std.Tactic.BVDecide.Gate.xor =>
          let ret := aig_2.mkXorCached input;
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨ret, this⟩, cache := cache }
        | Std.Tactic.BVDecide.Gate.beq =>
          let ret := aig_2.mkBEqCached input;
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨ret, this⟩, cache := cache }
        | Std.Tactic.BVDecide.Gate.or =>
          let ret := aig_2.mkOrCached input;
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨ret, this⟩, cache := cache }
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    Q ≠ 0 → Filter.Tendsto (fun x => |Polynomial.eval x P / Polynomial.eval x Q|) Filter.atTop Filter.atTop
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.SumEval.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.GoodProducts.SumEval C ho =
    Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l
-- Mathlib.Algebra.Group.Submonoid.Defs
OneMemClass.coe_one : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] (S' : A), ↑1 = 1