mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f : α →Co β}, f.toFun = ⇑f
-- Mathlib.Data.List.Sym
List.Nodup.sym2 : ∀ {α : Type u_1} {xs : List α}, xs.Nodup → xs.sym2.Nodup
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k k' : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKey! k' =
    if (k == k') = true then if (f (Std.DHashMap.Const.get? m k)).isSome = true then k else default else m.getKey! k'
-- Lean.Compiler.IR.Basic
/-- If `some <blame>`, then declaration depends on `<blame>` which uses a `sorry` axiom.  -/
Lean.IR.DeclInfo.sorryDep? : Lean.IR.DeclInfo → Option Lean.Name
-- Mathlib.Order.Category.Frm
Frm.hom_ofHom : ∀ {X Y : Type u} [inst : Order.Frame X] [inst_1 : Order.Frame Y] (f : FrameHom X Y), Frm.Hom.hom (Frm.ofHom f) = f
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles
-- Mathlib.Order.Lattice
le_sup_of_le_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ b
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.mono : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa μa' : MeasureTheory.Measure α}
  {μb μb' : MeasureTheory.Measure β} {f : α → β},
  μa'.AbsolutelyContinuous μa →
    μb.AbsolutelyContinuous μb' →
      MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb'
-- Mathlib.Data.Tree.Basic
BinaryTree.traverse.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β),
  BinaryTree.traverse f BinaryTree.nil = pure BinaryTree.nil
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The left adjoint of a 1-morphism.  -/
CategoryTheory.Bicategory.leftAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (f : b ⟶ a) → [CategoryTheory.Bicategory.IsRightAdjoint f] → a ⟶ b
-- Init.Data.SInt.Lemmas
Int8.ofIntClamp_toInt : ∀ (x : Int8), Int8.ofIntClamp x.toInt = x
-- Mathlib.Data.Stream.Defs
/-- Proposition saying that all elements of a stream satisfy a predicate.  -/
Stream'.All : {α : Type u} → (α → Prop) → Stream' α → Prop
-- Mathlib.Data.Bundle
/-- The pullback of a bundle `E` over a base `B` under a map `f : B' → B`, denoted by
`Bundle.Pullback f E` or `f *ᵖ E`, is the bundle over `B'` whose fiber over `b'` is `E (f b')`.  -/
Bundle.Pullback : {B : Type u_1} → {B' : Type u_4} → (B' → B) → (B → Type u_5) → B' → Type u_5
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.Finite.not_linearIndependent_of_infinite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M]
  [StrongRankCondition R] {ι : Type u_1} [Infinite ι] (v : ι → M), ¬LinearIndependent R v
-- Lean.Util.Diff
_private.Lean.Util.Diff.0.Lean.Diff.matchPrefix.go.eq_def : ∀ {α : Type u_1} [inst : BEq α] (left right : Subarray α) (pref : Array α),
  Lean.Diff.matchPrefix.go✝ left right pref =
    let i := pref.size;
    if x : i < Std.Slice.size left ∧ i < Std.Slice.size right then
      if (left[i] == right[i]) = true then Lean.Diff.matchPrefix.go✝ left right (pref.push left[i])
      else (pref, left.drop pref.size, right.drop pref.size)
    else (pref, left.drop pref.size, right.drop pref.size)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_coeff_mul_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  [inst_3 : Add A] [inst_4 : Add B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
    ∀ (f g : AddMonoidAlgebra R A), (f * g).coeff.support.sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instPartialOrder : {R : Type u} → {M : Type v} → [inst : SMul R M] → PartialOrder (SubMulAction R M)
-- Init.Data.Int.Order
Int.instIdempotentOpMax : Std.IdempotentOp max
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termα_mod_G : Lean.ParserDescr
-- Mathlib.Data.PNat.Xgcd
/-- `w = wp + 1`  -/
PNat.XgcdType.w : PNat.XgcdType → ℕ+
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- A linear map on weight space.  -/
RootPairing.Hom.weightMap : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} → {Q : RootPairing ι₂ R M₂ N₂} → P.Hom Q → M →ₗ[R] M₂
-- Mathlib.Analysis.Convex.Basic
MonotoneOn.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ici_add_one_eq_Ioi_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderTop α] [inst_3 : Add α]
  [SuccAddOrder α] {a : α}, ¬IsMax a → Finset.Ici (a + 1) = Finset.Ioi a
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.mk.inj : ∀ {expr exprType exprInit exprResult proof : Lean.Expr} {modified : Bool}
  {expr_1 exprType_1 exprInit_1 exprResult_1 proof_1 : Lean.Expr} {modified_1 : Bool},
  { expr := expr, exprType := exprType, exprInit := exprInit, exprResult := exprResult, proof := proof,
        modified := modified } =
      { expr := expr_1, exprType := exprType_1, exprInit := exprInit_1, exprResult := exprResult_1, proof := proof_1,
        modified := modified_1 } →
    expr = expr_1 ∧
      exprType = exprType_1 ∧
        exprInit = exprInit_1 ∧ exprResult = exprResult_1 ∧ proof = proof_1 ∧ modified = modified_1
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'_single : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (M : Matrix n m N₂) (i : n) (j : m), (((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) (Pi.single i 1)) (Pi.single j 1) = M i j
-- Init.Data.List.Basic
/-- `[]` is the smallest element in the lexicographic order.  -/
List.Lex.nil : ∀ {α : Type u} {r : α → α → Prop} {a : α} {l : List α}, List.Lex r [] (a :: l)
-- Init.Prelude
instMonadEvalT : (m : Type u_1 → Type u_2) → MonadEvalT m m
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintKind : Lean.FromJson Lean.Lsp.InlayHintKind
-- Mathlib.Data.Set.BoolIndicator
Set.boolIndicator.eq_1 : ∀ {α : Type u_1} (s : Set α) (x : α), s.boolIndicator x = if x ∈ s then true else false
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.ext_iff : ∀ {α α₂ β : Type w} {m : Type w → Type u_1} {x y : Std.Iterators.Types.Flatten α α₂ β m},
  x = y ↔ x.it₁ = y.it₁ ∧ x.it₂ = y.it₂
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inr_triangleδ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) {Z : CochainComplex C ℤ}
  (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).mor₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_inverse_map : ∀ {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete J × CategoryTheory.Discrete K} (x : X ⟶ Y),
  CategoryTheory.Discrete.productEquiv.inverse.map x =
    match x with
    | (f₁, f₂) => CategoryTheory.eqToHom ⋯
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceFrom_next : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).endPos},
  String.Slice.Pos.ofSliceFrom (p.next h) = (String.Slice.Pos.ofSliceFrom p).next ⋯
-- Mathlib.Probability.Process.Stopping
MeasureTheory.integrable_stoppedValue : ∀ {Ω : Type u_1} (ι : Type u_3) {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [inst_1 : PartialOrder ι] {ℱ : MeasureTheory.Filtration ι m}
  [inst_2 : NormedAddCommGroup E] [LocallyFiniteOrderBot ι],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ {N : ι}, (∀ (ω : Ω), τ ω ≤ ↑N) → MeasureTheory.Integrable (MeasureTheory.stoppedValue u τ) μ
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_image_le_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [AddLeftMono N] {g : ι → ι'} {f : ι' → N},
  (∀ u ∈ Finset.image g s, 0 ≤ f u) → ∑ u ∈ Finset.image g s, f u ≤ ∑ u ∈ s, f (g u)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomologicalComplex.homologyπ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  K.homologyπ i = (K.sc i).homologyπ
-- Mathlib.Data.Finsupp.Fin
Finsupp.tail_update_succ : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] (y : M) (t : Fin (n + 1) →₀ M),
  (t.update i.succ y).tail = t.tail.update i y
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.rightUnitor'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (i : I),
  K.rightUnitor'.inv i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (K.X i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (K.X i)
          (HomologicalComplex.singleObjXSelf c 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
        (K.ιTensorObj (HomologicalComplex.tensorUnit C c) i 0 i ⋯))
-- Mathlib.Data.Set.Sups
Set.image_subset_sups_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α} {b : α}, b ∈ t → (fun a => a ⊔ b) '' s ⊆ s ⊻ t
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- For any symplectic matrix `fromBlocks A B C D` over a local ring `R`, we can construct
a symmetric `X` s.t. `A + X * C` is invertible.

Introducing local ring hypothesis enables us to transport the construction of `X`
(from the previous lemma, which works only over fields) back to `R` while keeping
`A + X * C` invertible.  -/
_private.Mathlib.LinearAlgebra.SymplecticGroup.0.SymplecticGroup.exists_symmetric_X_isUnit_det_add_mul_of_symplectic : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A B C D : Matrix l l R} [IsLocalRing R],
  Matrix.fromBlocks A B C D ∈ Matrix.symplecticGroup l R → ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {inst_2 : CategoryTheory.Category.{v_3, u_3} C₃}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} C₄} {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {x y : CategoryTheory.CatCommSq T L R B},
  x = y ↔ CategoryTheory.CatCommSq.iso T L R B = CategoryTheory.CatCommSq.iso T L R B
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_iff_of_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} {f₃ : F₁ ⟶ F₃},
  CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃ →
    ∀ [CategoryTheory.Presheaf.IsLocallySurjective J f₁],
      CategoryTheory.Presheaf.IsLocallySurjective J f₃ ↔ CategoryTheory.Presheaf.IsLocallySurjective J f₂
-- Init.Meta.Defs
Lean.getGithash : Unit → String
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_add_self : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {a b : α}, a ≤ b + a
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearMap_comp : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} {R₂ : Type u_6} {R₃ : Type u_7}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] [inst_7 : AddCommMonoid P] [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : N →ₛₗ[σ₂₃] P) (f₂ : M →ₛₗ[σ₁₂] N),
  Finsupp.mapRange.linearMap (f ∘ₛₗ f₂) = Finsupp.mapRange.linearMap f ∘ₛₗ Finsupp.mapRange.linearMap f₂
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Yoneda.obj_map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Opposite.op X ⟶ Opposite.op Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.obj X).map f)) (CategoryTheory.CategoryStruct.id X) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.map f.unop).app (Opposite.op Y)))
      (CategoryTheory.CategoryStruct.id Y)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.mk.injEq : ∀ (dynamicRegistration? : Option Bool) (resolveSupport? : Option Lean.Lsp.ResolveSupport)
  (dynamicRegistration?_1 : Option Bool) (resolveSupport?_1 : Option Lean.Lsp.ResolveSupport),
  ({ dynamicRegistration? := dynamicRegistration?, resolveSupport? := resolveSupport? } =
      { dynamicRegistration? := dynamicRegistration?_1, resolveSupport? := resolveSupport?_1 }) =
    (dynamicRegistration? = dynamicRegistration?_1 ∧ resolveSupport? = resolveSupport?_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.quasicoherentData_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat}
  [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation)
  (a : C), P.quasicoherentData.X a = id a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_simple_adjoin_simple : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E),
  IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯
-- Init.Data.Vector.Lemmas
/-- Variant of `all_eq_false` in terms of membership rather than an array index.  -/
Vector.all_eq_false' : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = false ↔ ∃ x ∈ xs, ¬p x = true
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [inst_4 : q.IsPrime],
  q.ramificationIdx R =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) p)).toNat
-- Batteries.Data.List.Basic
/-- Computes the "bag intersection" of `l₁` and `l₂`, that is,
the collection of elements of `l₁` which are also in `l₂`. As each element
is identified, it is removed from `l₂`, so elements are counted with multiplicity.
 -/
List.bagInter : {α : Type u_1} → [BEq α] → List α → List α → List α
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux2.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (x : Equiv.Perm α), Equiv.Perm.signAux2 [] x = 1
-- Init.Data.Int.Order
Int.add_lt_of_lt_sub_left : ∀ {a b c : ℤ}, b < c - a → a + b < c
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_10 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.arithShiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_10 w n lhs rhs
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_liftAt : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n n' m : ℕ} {t : L.Term (α ⊕ Fin n)}
  {v : α ⊕ Fin (n + n') → M},
  FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.liftAt n' m t) =
    FirstOrder.Language.Term.realize (v ∘ Sum.map id fun i => if ↑i < m then Fin.castAdd n' i else i.addNat n') t
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.X_pow_order_dvd : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, PowerSeries.X ^ φ.order.toNat ∣ φ
-- Init.System.IOError
IO.Error.inappropriateType.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.inappropriateType filename osCode details = IO.Error.inappropriateType filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Algebra.Module.Projective
Module.projective_def' : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
  Module.Projective R P ↔ ∃ s, Finsupp.linearCombination R id ∘ₗ s = LinearMap.id
-- Mathlib.Analysis.Normed.Module.Basic
SubalgebraClass.toNormedAlgebra : {S : Type u_6} →
  {𝕜 : Type u_7} →
    {E : Type u_8} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedRing E] →
          [inst_2 : NormedAlgebra 𝕜 E] →
            [inst_3 : SetLike S E] → [inst_4 : SubringClass S E] → [SMulMemClass S 𝕜 E] → (s : S) → NormedAlgebra 𝕜 ↥s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.η_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.MonObj X],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointLieSubalgebraEquiv_symm_apply : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : N ≃ₗ[R] M)
  (f : ↥(skewAdjointLieSubalgebra B)), ↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj ↑f